A symbolic model checker for propositional projection temporal logic. (Chinese. English summary) Zbl 1340.68048

Summary: The formal specification languages for existing model checking tools such as computation tree logic (CTL) and linear temporal logic (LTL) are not powerful enough to describe \(\omega\)-regular properties, in which those properties cannot be verified. In this study, a design and implementation procedure of propositional projection temporal logic (PPTL) symbolic model checker (PLSMC) is developed by implementing the symbolic model checking algorithm for PPTL from author’s previous work based on the acclaimed symbolic model checking system NuSMV. As PPTL has the expressive power of full-regular expressions, both qualitative and quantitative properties can be verified with PLSMC. Moreover, PLSMC is an effective model checking tool to tackle the state space explosion problem. Finally, safety and iterative properties of a railway and highway crossing guardrail control system are checked with PLSMC. Experimental results show that the presented symbolic model checker for PPTL extends the validation functionality of the NuSMV system such that state sensitive, concurrent and periodic properties can be specified and verified with PPTL.


68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic


Full Text: DOI