Extended Temporal Logic Revisited

10 years 17 days ago
Extended Temporal Logic Revisited
A key issue in the design of a model-checking tool is the choice of the formal language with which properties are specified. It is now recognized that a good language should extend linear temporal logic with the ability to specify all  -regular properties. Also, designers, who are familiar with finite-state machines, prefer extensions based on automata than these based on fixed points or propositional quantification. Early extensions of linear temporal logic with automata use nondeterministic B¨uchi automata. Their drawback has been inability to refer to the past and the asymmetrical structure of nondeterministic automata. In this work we study an extension of linear temporal logic, called ETL© , that uses two-way alternating automata as temporal connectives. Two-way automata can traverse the input word back and forth and they are exponentially more succinct than one-way automata. Alternating automata combine existential and universal branching and they are exponentially more ...
Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Authors Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Comments (0)