一句话：给出时间自动机二元可达关系可在线性算术中定义的新简化证明，并用于参数化 TCTL 可达片段的模型检测与复杂度下界。
时间自动机配置间的二元可达关系可用整数与实数上的线性算术定义，是实时验证中的基本结论。本文基于差分约束矩阵（DBM）的可达性分析，给出该结论一个更简单的新证明。利用该证明，作者为参数化 TCTL 的可达片段设计了指数空间模型检测过程；同时证明该模型检测问题是 NEXPTIME-难的，从而刻画了其复杂度上界与下界。结果深化了对时间自动机可达性及参数化时序逻辑验证复杂度的理解。
We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.