Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
435541 | Theoretical Computer Science | 2016 | 17 Pages |
Abstract
This paper proposes a Canonical Form (CF) for chop formulas of Propositional Projection Temporal Logic (PPTL). Based on CF, an improved algorithm for constructing Labeled Normal Form Graph (LNFG) of a PPTL formula is presented. This improvement leads to a better decision procedure for PPTL with infinite models. In addition, a transformation from LNFGs to Generalized Büchi Automata (GBA) and then Büchi Automata (BA) is formalized. Thus, a SPIN based model checking approach is generalized for PPTL. To illustrate how these algorithms work, several examples are given.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Zhenhua Duan, Cong Tian, Nan Zhang,