Parameterised Model Checking for Alternating-Time Temporal Logic
Parameterised Model Checking for Alternating-Time Temporal Logic
复制标题
交替时间时序逻辑的参数化模型检查
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
A. Lomuscio
中科院分区：
文献类型：
--
作者：
Panagiotis Kouvaros;A. Lomuscio
我们研究了以交替时间时序逻辑表示的规范的参数化模型检查问题。我们引入参数化的并发游戏结构，代表具有不同数量代理的无限多个游戏。我们引入了 ATL 的参数变体来表达系统的属性，而与系统中存在的代理数量无关。虽然参数化模型检查问题是不可判定的，但我们定义了一类特殊的系统，在其上开发了健全且完整的反抽象技术。我们说明了这里针对列车门控制器的优先版本设计的方法。
We investigate the parameterised model checking problem for specifications expressed in alternating-time temporal logic. We introduce parameterised concurrent game structures representing infinitely many games with different number of agents. We introduce a parametric variant of ATL to express properties of the system irrespectively of the number of agents present in the system. While the parameterised model checking problem is undecidable, we define a special class of systems on which we develop a sound and complete counter abstraction technique. We illustrate the methodology here devised on the prioritised version of the train-gate-controller.