Reasoning And Symbolic Model Checking Of Extended Temporal Logics

With the never-ending increase of the complexity of software and hardware,correctness of design and implementation becomes more and more di?cult to guar-antee. Therefore, verification technologies are urgently required in such fields. Themodel checking approach, presented in the 80s last century, has been proven anapplicable technique in verifying the correctness of software and hardware systems.Verification algorithms is highly sensitive to the type of specification language.Temporal logics under linear framework, such as LTL, benefit from several aspectssuch as (relative) stronger expressiveness, better intuitiveness, and better compati-bility. As a result, linear time temporal logics receive a wide application in practice.Nevertheless, LTL is still not powerful enough to express all theω-regular prop-erties used in industrial verification. Hence, many extensions of LTL are suggested,and in a broad sense, these logics can be obtained by the following two approaches.1. One approach is to add infinitely many operators or regular expressions to obtainlogics as expressive asω-regular languages. Such extensions like ETLs, ForSpec,PSL etc.2. The other approach is to cooperate temporal logics with second order quantifiersor fixpoint operators. For example, MSOL, QTL, or linearμ-calculus.All these extensions are known to be as expressive asω-regular expressions. Forthese logics, the following issues are mostly concerned.1. The decision problem. i.e., the decidability of this logic and its inherit com-plexity. Those problems are usually solved at the first moment when the logicsare proposed.2. The axiomatization problem. i.e., to give a sound and complete axiomsystem for the logic. An axiom system usually consists of a set of axioms anddeductive rules, which re?ect the essence of the logic.3. The model checking problem. For a given temporal logic, finding its e?ectiveverification algorithm is always the most important aim in model checking.In fact, a logic is doomed to be rarely used in model checking if its e?ectiveverification algorithm does not exist. For variousω-extensions of linear temporal logic, the study of their axiom-atization and symbolic model checking has special significance: These languagesare powerful enough to express various specifications used in industrial community.Other temporal logics on linear structures can be viewed as fragments or sub-logicsof these extensions. Hence, one can derive their axiom system or symbolic modelchecking algorithm by a systematic encoding or instantiation.Major contributions of this thesis are listed as follows.1. Sound and Complete axiom systems for three kinds of ETLs (i.e., ETLl, ETLf,ETLr) are presented, and it is shown how to obtain sound and complete deduc-tive systems for ETL fragments via instantiating temporal connectives.2. Based on game theory, new proofs of completeness ofμ-calculus axiom systems(both branching and linear) are given. In comparison to the existing approaches,these proofs are relative succinct.3. BDD based symbolic model checking algorithms for three kinds of ETLs withalternating automata connectives (i.e., ATLf, ATLl, ATLr) and a variant ofPSL are given.4. BDD based symbolic model checking approaches for linearμ-calculus formulasin general and specific forms (namely,ν-form) are respectively presented.5. An extension of NuSMV, namely ENuSMV, is designed and implemented.ENuSMV is also a symbolic model checker, it allows users to customize theirown temporal connectives by writing automata. With which, all theω-regulartemporal properties can be verified.