Verification of Qualitative ![]()
rc="http://springerlink.lib.tsinghua.edu.cn/media/images/contributions/5/1/8/G/518GUF8UT3PNBLWV_html/MediaObjects/InlineFigure1.png" alt="MediaObjects/Inl
详细信息 查看全文
- 作者：Sté ; phane Demri ; Ré ; gis Gascon
- 刊名：Lecture Notes in Computer Science
- 出版年：2005
- 出版时间：2005
- 年：2005
- 卷：3653
- 期：1
- 页码：p.518
- 全文大小：532 KB
- 刊物类别：Computer Science
- 刊物主题：Artificial Intelligence and Robotics
- 出版者：Springer Berlin / Heidelberg
- ISSN：1611-3349
文摘
We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in ![]()
rc="http://springerlink.lib.tsinghua.edu.cn/media/images/contributions/5/1/8/G/518GUF8UT3PNBLWV_html/MediaObjects/InlineFigure2.png" alt="MediaObjects/InlineFigure2.png" align="middle">. The constraint language includes periodicity constraints, comparison constraints of the form x = y and x < y, it is closed under Boolean operations and it admits a restricted form of existential quantification. This is the largest set of qualitative constraints over ![]()
rc="http://springerlink.lib.tsinghua.edu.cn/media/images/contributions/5/1/8/G/518GUF8UT3PNBLWV_html/MediaObjects/InlineFigure3.png" alt="MediaObjects/InlineFigure3.png" align="middle"> known so far, shown to admit a decidable LTL extension. Such constraints are those used for instance in calendar formalisms or in abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. As a by-product, LTL model-checking over integral relational automata is proved complete for polynomial space which contrasts with the known undecidability of its CTL counterpart.