Abstract
A new decision procedure for Propositional Projection Temporal Logic (PPTL) is proposed which is an improvement to the decision procedure given in [4]. The main contribution of the paper is as follows: (1) the relationship between paths in the NFG of a formula R and its models is established and proved; (2) a new Labeled NFG (LNFG) with a set of labels (propositions) is defined; (3) given a formula R, an LNFG of R can be generated by the new decision algorithm, and all models of R can be found; (4) based on the new decision procedure, an improved model checking algorithm is presented and implemented. © 2010 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Duan, Z., & Tian, C. (2010). An improved decision procedure for propositional projection temporal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6447 LNCS, pp. 90–105). https://doi.org/10.1007/978-3-642-16901-4_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
