Y.__Kesten
A decision algorithm for full propositional temporal logic
Integration graphs: a class of decidable hybrid systems
Symbolic model checking with rich assertional languages
Timed and hybrid statecharts and their textual representation