Time and alternation
Abdelaziz Fellah · 2010
In this paper, we present a class of powerful canonical timed alternating automata and a formalism for describing timed linear temporal logic to software model checking. Time and alternation, these two "metaphors" have dominated automata theory research in recent years. For real-time systems, it is important to augment untimed and asynchronous models of computation with the notion of time. Nevertheless, alternation is a powerful parallelism feature that has the potential to improve and reduce the state-space explosion problem in building large software model checking systems. We show that the dual connection between timed automata-theoretical and propositional-logic frameworks support and model software specifications. This can be established through languages over infinite timed words; and has a direct impact for expressing logical aspects and properties of model checking software systems.