Lattice-valued Quantitative Verification Of State Transition Systems

Formal method is proving or disproving the correctness of software and hardware systems using formal methods of mathematics. Classic formal description and verification methods have been extensively studied based on two-valued logic. Increasing attention has recently been de-voted to multi-valued description and verification. The quantitative description and verifica-tion theory, including the numerical and non-numerical quantitative description and verification methods, has been formed gradually. In this paper, combining with complete residuated lattice and formal methods, we provide a a general framework for allowing imprecise or incomplete specifications to be expressed and satisfying the need of quantitative verification, resulted in a new theory of non-numerical(lattice-valued) quantitative verification. The main content of this paper is as follows:(1) In Section3, based on complete residuated lattice, we define lattice-valued doubly labeled transition systems (for short, LLDTS) as a general framework for allowing imprecise or incomplete specifications to be expressed and satisfying the need of quantitative veri-fication. Lattice-valued labeled transition systems and lattice-valued Kripke structures are two special cases of LLDTSs. We introduce lattice-valued bisimulation and simula-tion relation between LLDTSs that measure the degree of closeness of two systems as an element of residuated lattice, in contrast to the traditional boolean yes/no to bisimu-lation and simulation. Also, we establish a logical characterization of our bisimulation, given by a lattice-valued extension of μ-calculus. Furthermore, one important applica-tion, lattice-valued model checking, are presented as evidence of the suitability of LDTS and lattice-valued bisimulation as a foundation for lattice-valued analyzes.(2) In Section4, we show how the traditional trace inclusion and equivalence between Kripke structures, can be lifted to a setting of quantitative between lattice-valued Kripke struc-tures, where their interpretation is given as elements of complete residuated lattices. We introduce three distinct quantitative versions of the relations. We study the properties of these relations, as well as the relationships among them. We also present logical charac-terizations of our notions, given by a lattice-valued extension of LTL.(3) In Section5,we explore the relationship between lattice-valued Kripke structure and lattice-valued labeled transition system. By introducing the translation methods between two kinds of models, this paper shows that lattice-valued bisimulation equivalence rela-tion in lattice-valued Kripke structure coincides with lattice-valued bisimulation equiva-lence relation in lattice-valued labeled transition system. It also prove that model check-ing lattice-valued HML defined over lattice-valued labeled transition system can be re-duced to model checking lattice-valued modal logic defined over lattice-valued Kripke structure, and vice versa. The basic properties of the lattice-valued computation tree logic, such as the model checking lattice-valued computation tree logic, are discussed in this section.(4) In Section6, a lattice-valued timed automaton, an extension to the well-studied specifi-cation formalism of real-time systems, is presented for the specification and verification of real-time systems when designing and analyzing the ones in the context of incom-plete or inconsistent setting. Several important results for lattice-valued timed automata are discussed. First, we give the operational semantics of lattice-valued timed automata defined over a derivative of LLDTSs and discuss the decidability of reachablity prob-lem. Secondly, to express the properties of lattice-valued timed automata, we introduce a real-time temporal logic, LACTLWc. Thirdly, We develop a model checking method for such model against LATCTLc. We also present a notion of D-bisimulation to compare the behavior of two states in a lattice-valued timed automaton, and show that LATCTLc logically characterizes the D-bisimulation.