下推式定时自动机：二进制可达性描述和安全验证
摘要：推动堆积时间自动机（PTA）是使用堆栈增强的时间自动机（具有密集时钟）。PTA的配置包括控制状态、密集时钟值和堆栈字。通过使用模式技术，我们给出了PTA的二进制可达性（即可以达到另一个的所有配置对的集合）的可判定特征。由于时态自动机可以被视为没有堆栈的PTA，我们可以证明时态自动机的二进制可达性可以用加法理论来定义实数和整数。这些结果可用于验证一类包含对密集变量和无界离散变量的线性关系的属性。之前这些属性无法通过经典区域技术进行验证，也不能由定时自动机的定时时态逻辑或用于堆叠系统的CTL$^*$表达。结果还扩展到了定时自动机的其他一般化形式。
作者：Zhe Dang
论文ID：cs/0110010
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23