zbMATH — the first resource for mathematics

Temporal logic can be more expressive. (English) Zbl 0534.03009
An extension of the propositional version of temporal logic (PTL), the extended temporal logic (ETL), is introduced. In ETL there are expressible properties definable by right-linear grammars, particularly by regular expressions. For ETL an axiomatization for the new temporal operator is shown (corresponding to right-linear grammars). The axiomatization is proved to be complete and a decision procedure for ETL is shown. Although ETL is more expressible than PTL, it is proved that satisfiability for ETL remains PSPACE-complete.
Reviewer: J.Zlatuska

03B45 Modal logic (including the logic of norms)
03F20 Complexity of proofs
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
03D05 Automata and formal grammars in connection with logical questions
Full Text: DOI