From timed automata to logic — and back

Abstract

In this paper, we define a timed logic Lv which is sufficiently expressive that we for any timed automaton may construct a single characteristic Lv formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisflability problem for Lv with respect to given bounds on the number of clocks and constants of the timed automata to be constructed.