A canonical form based decision procedure and model checking approach for propositional projection temporal logic (Q896152)

Propositional 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.