参数化时序自动机中不变量表达能力的探讨
摘要
对兼具硬时序约束与并发性的系统进行验证具有挑战性。当某些时序常数缺失或未知时，这一挑战变得更加困难。参数化时序形式体系，如参数化时序自动机（PTAs），致力于综合使某性质成立的此类时序常数（视为参数）。这类形式体系具有高度表达力，但也是不可判定的，仅有少数可判定子类被提出。我们在此提出一种对 PTAs 的语法限制：移除守卫（转移上的约束），仅保留不变量（位置上的约束）。尽管该限制保持了 PTAs 的表达力（因而其不可判定性），但对约束类型的额外限制不仅可证明可判定性，还能精确综合满足可达性的参数赋值。该形式体系初看似乎平凡，因其享有比时序自动机（TAs）更优复杂度的可达性问题的可判定性；但它受制于整个 TCTL 逻辑的不可判定性，而 TAs 恰恰享有该逻辑的可判定性。我们认为我们的形式体系在可判定性与实际表达力之间提供了有趣的权衡，因而具有前景。我们在一个小型案例研究中展示了其适用性。
引用
@article{arxiv.1908.06633,
title = {On the expressive power of invariants in parametric timed automata},
author = {Étienne André and Didier Lime and Mathias Ramparison},
journal= {arXiv preprint arXiv:1908.06633},
year = {2019}
}
备注
This is the author version of the manuscript of the same name published in the proceedings of the 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019). This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST