On the relationship between \(\omega\)-automata and temporal logic normal forms. (English) Zbl 1007.03014
The relationship between Büchi automata on infinite words and a specific logical formalism based on a normal form for temporal logic formulae, called SNF/PLTL (separated normal form for propositional linear-time temporal logic) is considered. The known representation of Büchi automata in quantified propositional temporal logic (QPTL) inspired the work of this paper. Two main theorems are proved. Theorem 1. Given a Büchi automaton \(A\), we can construct a characteristic clause set \(\text{SNF}(A)\) such that \(A\) has an accepting run if and only if \(\text{SNF}(A)\) is satisfiable. Theorem 2. Given a set \(C\) of SNF/PLTL clauses, we can construct a Büchi automaton \(A(C)\) such that \(C\) is satisfiable if and only if \(A(C)\) has an accepting run. SNF/PLTL is applied as a specification language to express the property “\(p\) occurs at every even moment of time”, i.e., the \(\text{Even}(p)\) property.
Reviewer: Alex Nabebin (Moskva)
MSC:
03B44 | Temporal logic |
03D05 | Automata and formal grammars in connection with logical questions |
03B35 | Mechanization of proofs and logical operations |