可更新时序自动机可达性计算的加速与增效
计算机科学中的逻辑
2020-09-29 v1 形式语言与自动机理论
摘要
可更新时序自动机（UTA）是经典时序自动机的扩展，允许在转移上对时钟变量进行特殊更新，如 x:= x - 1、x := y + 2 等。UTA 的可达性在一般情形下是不可判定的。人们已研究过多种具有可判定可达性的子类。UTA 可达性的一般方法包含两阶段：首先，对自动机进行静态分析以计算每个状态下的一组时钟约束；第二阶段枚举可达的配置集合，称为区域。本文中，我们改进了静态分析算法。与已有算法相比，我们的方法计算出更小的约束集合，并对更多 UTA 保证终止，使可达性计算更快且更有效。作为主要应用，我们得到了有界减法时序自动机（一类广泛用于建模调度问题的 UTA）可判定性的另一种证明及更高效的算法。我们已在工具 TChecker 中实现了我们的过程，并进行了实验以验证我们所提方法的益处。
引用
@article{arxiv.2009.13260,
title = {Reachability for Updatable Timed Automata made faster and more effective},
author = {Paul Gastin and Sayan Mukherjee and B Srivathsan},
journal= {arXiv preprint arXiv:2009.13260},
year = {2020}
}
备注
Shorter version of this article is accepted at FSTTCS 2020