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 omega-regular properties using lattice-valued automata are thoroughly studied. Since the law of non-contradiction (i.e., a boolean AND -a = 0) and the law of excluded-middle (i.e., a boolean OR -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 satisfies P for a model TS and a linear-time property P, which proceeds by directly checking the inclusion Traces(TS) subset of P instead of Traces(TS) boolean AND -P = phi. 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. (C) 2016 Elsevier Inc. All rights reserved.