Extending temporal logic with omega-automata
We investigate the extension of linear temporal logic with
omega-automata. We give an alternative translation from Extended
Temporal Logic [WVS83] formulas to nondeterministic Buchi automata.
The novelty in our translation is usage of alternating automata, thus,
simplifying the translation while staying with the same complexity bounds.
We continue and use alternating Buchi automata as temporal connectives
of the logic. Again we translate the formulas of the logic to nondeterministic
Buchi automata. Although alternating automata are exponentialy more succinct
than nondeterministic ones, the complexity of the translation does not change.
Finally we combine the extension in the expressive power of the logic
with the reference to the past. We use 2-way alternating automata as
temporal connectives. Also here we give a translation of logic formulas
to nondeterministic Buchi automata.
@mastersthesis{Pit00,
author = "N. Piterman",
title = "Extending temporal logic with $\omega$-automata",
school = "The Weizmann Institute of Science",
year = "2000"
}
PDF