时间自动机中循环的快速检测
计算机科学中的逻辑
2014-10-17 v1 形式语言与自动机理论
摘要
我们提出了一种新的高效算法，用于检测时间自动机中的循环是否可以被无限次迭代。现有解决该问题的方法其复杂度关于时钟数量呈指数级增长。我们的方法是多项式时间的：它本质上执行了对数次数量的区（zone）规范化。该方法可被整合到用于验证时间自动机上 B"uchi 性质的算法中。我们报告了一些实验，表明当使用我们的可迭代性测试时，搜索空间显著减少。
引用
@article{arxiv.1410.4509,
title = {Fast detection of cycles in timed automata},
author = {Aakash Deshpande and Frédéric Herbreteau and B. Srivathsan and Thanh-Tung Tran and Igor Walukiewicz},
journal= {arXiv preprint arXiv:1410.4509},
year = {2014}
}