Model-Checking of Linear-Time Properties in Multi-Valued Systems

TL;DR

This paper extends model-checking techniques to multi-valued systems, introducing new properties and algorithms that account for the nuances of multi-valued logic, including lattice-valued automata and degrees of membership.

Contribution

It introduces novel multi-valued linear-time properties, algorithms for their verification, and reduces multi-valued model checking to classical methods, addressing non-classical logic laws.

Findings

Multi-valued model checking can be reduced to classical model checking.

New forms of properties due to absence of law of non-contradiction and excluded middle.

Algorithms for verifying multi-valued safety and ω-regular properties are developed.

Abstract

In this paper, we study model-checking of linear-time properties in multi-valued systems. Safety property, invariant property, liveness property, 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 $\omega$-regular properties using lattice-valued automata are thoroughly studied. Since the law of non-contradiction (i.e., $a\wedge \neg a=0$) and the law of excluded-middle (i.e., $a\vee \neg a=1$) do not hold in multi-valued logic, the linear-time properties introduced in this paper have the new forms compared to those in classical logic. Compared to those classical model checking methods, our methods to multi-valued model checking are more directly accordingly. 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 the classical model checking. The related verification algorithms are also presented. Some illustrative examples and case study are also provided.