A canonical form based decision procedure and model checking approach for propositional projection temporal logic.

*(English)*Zbl 1370.68200Propositional Projection Temporal Logic (PPTL) is a formalism for specifying linear-time properties. It has full regular expressive power which is owed to the presence of the projection operator – a less intuitive but powerful construct that basically expresses how an interval should be partitioned such that each part satisfies some property locally, and at the same time some subsequence satisfies another property globally. In fact, PPTL uses an infinite family of such operators parametrised by their arity or, equivalently, the size of the underlying partition. This, at least, makes PPTL’s status as a logic disputable.

The paper itself is part of a series of papers mainly by the authors of this paper, whose aim it is to establish the practical usefulness of PPTL as a specification formalism for automatic verification. Thus, decidability of satisfiability and model checking (which are closely related for linear-time logics and can typically be handled by the same automata-theoretic constructions) is the main focus. To this end, the authors have previously devised a procedure that is based on the syntactic manipulation of formulas into some normal form which closely resembles the transition table of an \(\omega\)-automaton.

The paper at hand presents an improvement of the construction of this normal form. The paper is not entirely self-contained as it makes lots of references to previous work, especially to explain the nature of this improvement and sometimes also for technical content. Hence, the full value of this paper is best judged with knowledge of the authors’ previous work in this area. The paper’s bibliography is a great source for the interested reader in this respect: almost 50% of the references are self-citations.

It must be said that the paper’s quality is below the usual standards one expects of the journal Theoretical Computer Science. The editing process should at least have eliminated awkward formulations and ensured that mathematical symbols are used for what they are typeset for; this would have eased the readers’ understanding of the paper’s content.

The paper itself is part of a series of papers mainly by the authors of this paper, whose aim it is to establish the practical usefulness of PPTL as a specification formalism for automatic verification. Thus, decidability of satisfiability and model checking (which are closely related for linear-time logics and can typically be handled by the same automata-theoretic constructions) is the main focus. To this end, the authors have previously devised a procedure that is based on the syntactic manipulation of formulas into some normal form which closely resembles the transition table of an \(\omega\)-automaton.

The paper at hand presents an improvement of the construction of this normal form. The paper is not entirely self-contained as it makes lots of references to previous work, especially to explain the nature of this improvement and sometimes also for technical content. Hence, the full value of this paper is best judged with knowledge of the authors’ previous work in this area. The paper’s bibliography is a great source for the interested reader in this respect: almost 50% of the references are self-citations.

It must be said that the paper’s quality is below the usual standards one expects of the journal Theoretical Computer Science. The editing process should at least have eliminated awkward formulations and ensured that mathematical symbols are used for what they are typeset for; this would have eased the readers’ understanding of the paper’s content.

Reviewer: Martin Lange (Kassel)

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

03B44 | Temporal logic |

##### Keywords:

linear-time temporal logic; interval temporal logic; decision procedure; propositional projection temporal logic; Büchi automata; model checking; specification; automatic verification
PDF
BibTeX
XML
Cite

\textit{Z. Duan} et al., Theor. Comput. Sci. 609, Part 3, 544--560 (2016; Zbl 1370.68200)

Full Text:
DOI

##### References:

[1] | Clarke, E. M.; Emerson, E. A., Desigh and syntesis of of synchronization skeletons using branching time temporal logic, (Logic of Programs Workshop, Yorktown Heights, NY, May 1981, LNCS, vol. 131, (1981), Springer) |

[2] | Quielle, J. P.; Sifakis, J., Specification and verification of concurrent systems in CESAR, (Proceedings of the 5th International Symposium on Programming, (1981)), 337-350 |

[3] | Pnueli, A., The temporal logic of programs, (Proc. 18th IEEE Symp. Found. of Comp. Sci, (1977)), 46-57 |

[4] | Emerson, E. Allen, Temporal and modal logic, (van Leeuwen, Jan, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, (1990)), 995-1072 · Zbl 0900.03030 |

[5] | Duan, Z.; Tian, C.; Zhang, Li, A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78, (2008) · Zbl 1141.68039 |

[6] | Duan, Zhenhua; Tian, Cong, A practical decision procedure for propositional projection temporal logic with infinite models, Theor. Comp. Sci., 554, 169-190, (2014) · Zbl 1358.68188 |

[7] | Duan, Z., Temporal logic and temporal logic programming, (2006), Science Press Beijing |

[8] | Tian, Cong; Duan, Zhenhua, Model checking propositional projection temporal logic based on SPIN, (ICFEM 2007, (Nov 2007), Springer-Verlag), 246-265 |

[9] | Moszkowski, B., Executing temporal logic programs, (1986), Cambridge University Press · Zbl 0658.68014 |

[10] | Duan, Z., An extended interval temporal logic and a framing technique for temporal logic programming, (1996), University of Newcastle upon Tyne, Ph.D. thesis |

[11] | Tian, Cong; Duan, Zhenhua, Expressiveness of propositional projection temporal logic, Theoret. Comput. Sci., 412, 18, 1729-1744, (Aug 2011) |

[12] | Clarke, E. M.; Grumberg, O.; Peled, D. A., Model checking, (1999), MIT Press |

[13] | Duan, Zhenhua; Tian, Cong, An improved decision procedure for propositional projection temporal logic, formal methods and software engineering, 90-105, (2010), Springer Berlin/Heidelberg |

[14] | Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (Computer Aided Verification, (2001), Springer-Verlag), 53-65 · Zbl 0991.68044 |

[15] | Holzmann, Gerard J., The model checker spin, IEEE Trans. Softw. Eng., 23, 5, 279-295, (1997) |

[16] | Tian, C.; Duan, Z., Propositional projection temporal logic, Büchi automata and ω-regular expressions, (Theory and Applications of Models of Computation, (2008), Springer Berlin/Heidelberg), 47-58 · Zbl 1140.03305 |

[17] | Yang, Kai; Duan, Zhenhua; Tian, Cong, Modeling and verification of RBC handover protocol, Electron. Notes Theor. Comput. Sci., 309, 51-62, (2014) |

[18] | Yu, Bin; Duan, Zhenhua; Tian, Cong, Bounded model checking of traffic light control system, Electron. Notes Theor. Comput. Sci., 309, 63-74, (2014) · Zbl 1351.68169 |

[19] | Katoen, Joost-Pieter, Concepts, algorithms, and tools for model checking, (Lecture Notes of the Course Mechanised Validation of Parrel Systems, (1999)) · Zbl 0934.03044 |

[20] | Tian, Cong; Duan, Zhenhua, Complexity of propositional projection temporal logic with star, Math. Structures Comput. Sci., 19, 1, 73-100, (2009) · Zbl 1161.03008 |

[21] | McMillan, K. L., Symbolic model checking, (1993), Kluwer Academic Publishers · Zbl 0784.68004 |

[22] | Biere, A.; Cimatti, A.; Clarke, E. M.; Strichman, O.; Zue, Y., Bounded model checking, Advances in Computers, vol. 58, (2003), Academic Press |

[23] | Clarke, Edmund M.; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 5, 752-794, (2003) · Zbl 1325.68145 |

[24] | Clarke, E. M.; Gupta, A.; Kukula, J. H.; Strichman, O., SAT based abstraction-refinement using ILP and machine learning techniques, (Brinksma, E.; Larsen, K. G., Proc. Computer-Aided Verification, CAV, (2002)), 265-279 · Zbl 1010.68515 |

[25] | Duan, Zhenhua; Tian, Cong, A unified model checking approach with projection temporal logic, (ICFEM 2008, (2008)), 167-186 |

[26] | Tian, Cong; Duan, Zhenhua; Duan, Zhao, Making CEGAR more efficient in software model checking, IEEE Trans. Softw. Eng., 40, 12, 1206-1223, (2014) |

[27] | Cong Tian; Duan, Zhenhua, Detecting spurious counterexamples efficiently in abstract model checking, (ICSE 2013, (2013)), 202-211 |

[28] | Godefroid, P.; Klarlund, N.; Sen, K., DART: directed automated random testing, (PLDI, (2005), ACM), 213-223 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.