论文标题
定时下降自动机的可及性关系
Reachability relations of timed pushdown automata
论文作者
论文摘要
定时下降自动机（TPDA）是一种表现力的形式主义，将递归与广泛的时序约束逻辑相结合。我们证明，TPDA的可达性关系在线性算术中是可以表达的，这是一种丰富的逻辑概括性的爆发前算术和理性算术。主要的技术成分是时钟约束的新量化剂消除结果（用于简化TPDA过渡的语法），使用时钟差关系来表达分数时钟值的可及性关系以及Parikh定理的应用来重建积分时钟值。
Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax of TPDA transitions), the use of clock difference relations to express reachability relations of the fractional clock values, and an application of Parikh's theorem to reconstruct the integral clock values.
