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

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., a∧¬a=0) and the law of excluded-middle (i.e., a∨¬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 Traces(TS)∩¬P=∅. 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.