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

• Type: Conference
• Year: 2001
• Where: CONCUR
• Authors: Orna Kupferman, Nir Piterman, Moshe Y. Vardi
• Keywords: Alternating Automata, CONCUR 2001, Distributed And Parallel Computing, Linear Temporal Logic, Two-way Alternating Automata