A canonical form based decision procedure and model checking approach for propositional projection temporal logic
type: Item
instance of: scholarly article
title: A canonical form based decision procedure and model checking approach for propositional projection temporal logic
zbMATH Open document ID: 1370.68200
author: Zhenhua Duan
author: Cong Tian
author: Nan Zhang
published in: Theoretical Computer Science
publication date: 2015-12-11T00:00:00Z
review text: 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 u…
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
zbMATH DE Number: 6520541
zbMATH Keywords: linear-time temporal logic
zbMATH Keywords: interval temporal logic
zbMATH Keywords: decision procedure
zbMATH Keywords: propositional projection temporal logic
zbMATH Keywords: Büchi automata
zbMATH Keywords: model checking
zbMATH Keywords: specification
zbMATH Keywords: automatic verification
describes a project that uses: LTL2BA
describes a project that uses: SPIN
describes a project that uses: DART
describes a project that uses: CESAR
MaRDI profile type: Publication
full work available at URL: j.tcs.2015.08.039
OpenAlex ID: W1835747325
cites work: Q4385542
cites work: A decision procedure for propositional projection temporal logic with infinite models
cites work: A practical decision procedure for propositional projection temporal logic with infinite models
cites work: Q3806791
cites work: Expressiveness of propositional projection temporal logic with star
cites work: Q4551134
cites work: Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
cites work: Bounded model checking of traffic light control system
cites work: Q4270055
cites work: Complexity of propositional projection temporal logic with star
cites work: Q3141897
cites work: Counterexample-guided abstraction refinement for symbolic model checking
cites work: Q4804901
DOI: 10.1016/J.TCS.2015.08.039
description: scientific article; zbMATH DE number 6520541