Model checking of linear-time properties in multi-valued systems

详细信息    查看全文

• 作者：Yongming Li ; ^a ; ^{liyongm@snnu.edu.cn" class="auth_mail" title="E-mail the corresponding author} ; Manfred Droste^b ; ^{droste@informatik.uni-leipzig.de" class="auth_mail" title="E-mail the corresponding author} ; Lihui Lei^a ; ^{leilihui@snnu.edu.cn" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Model checking ; Multi-valued transition system ; Invariant ; Safety ; Liveness ; Lattice-valued finite automaton
• 刊名：Information Sciences
• 出版年：2017
• 出版时间：20 January 2017
• 年：2017
• 卷：377
• 期：Complete
• 页码：51-74
• 全文大小：1087 K

文摘

In this paper, we study the model-checking problem of linear-time properties in multi-valued systems. Safety properties, invariant properties, liveness properties, persistence and dual-persistence properties in multi-valued logic systems are introduced. Some algorithms related to the above multi-valued linear-time properties are discussed. The verification of multi-valued regular safety properties and multi-valued ω  -regular properties using lattice-valued automata are thoroughly studied. Since the law of non-contradiction (i.e., b=MathURL&_method=retrieve&_eid=1-s2.0-S0020025516313548&_mathId=si3.gif&_user=111111111&_pii=S0020025516313548&_rdoc=1&_issn=00200255&md5=175b712979ae5b1b249ce6e71e7261cd" title="Click to view the MathML source">a∧¬a=0$a\wedge \neg a=0$) and the law of excluded-middle (i.e., b=MathURL&_method=retrieve&_eid=1-s2.0-S0020025516313548&_mathId=si4.gif&_user=111111111&_pii=S0020025516313548&_rdoc=1&_issn=00200255&md5=a310c0b811b4fdb4d492bb5a7c733aa2" title="Click to view the MathML source">a∨¬a=1$a\vee \neg a=1$) do not hold in multi-valued logic, the linear-time properties introduced in this paper have new forms compared to those in classical logic. Compared to those classical model-checking methods, our methods to multi-valued model checking are accordingly more direct: We give an algorithm for showing TS⊧P for a model TS and a linear-time property P, which proceeds by directly checking the inclusion Traces(TS) ⊆ P   instead of b=MathURL&_method=retrieve&_eid=1-s2.0-S0020025516313548&_mathId=si5.gif&_user=111111111&_pii=S0020025516313548&_rdoc=1&_issn=00200255&md5=891ec1d503acffa672800f4f53b29ca7" title="Click to view the MathML source">Traces(TS)∩¬P=∅$Traces\left(TS\right)\cap \neg P=\varnothing$. A new form of multi-valued model checking with membership degree is also introduced. In particular, we show that multi-valued model checking can be reduced to classical model checking. The related verification algorithms are also presented. Some illustrative examples and a case study are also provided.