Modal Transition Systems: Composition and LTL Model Checking
Modal Transition Systems: Composition and LTL Model Checking
复制标题
模态转换系统：组合和 LTL 模型检查
DOI：
10.1007/978-3-642-24372-1_17
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Jan Křetínský
中科院分区：
文献类型：
--
作者：
Nikola Benes;I. Cerná;Jan Křetínský
模态转换系统（MTS）是一种用于规范和抽象解释的成熟的形式主义。我们认为它的析取扩展（DMTS），我们提供的算法表明，DMTS的细化问题并不比MTS的情况下更难。本文主要有两个结果。首先，我们发现了一个错误，在以前的尝试在MTS的LTL模型检测和MTS和DMTS的LTL模型检测算法。此外，我们将展示如何将此结果应用于成分验证和规避MTS组合物的一般不完整性。其次，对常见的实现和合取组合问题给出了一个解决方案，将复杂度从EXPTIME降低到PTIME。
Modal transition systems (MTS) is a well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify an error in a previous attempt at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME.