Translating a continuous-time temporal logic into timed automata

LTLC is a continuous-time linear temporal logic for the specification of real-time systems. It can express both real-time systems and their properties. With LTLC, real-time systems can be described at different levels of abstraction, from high-level requirement specifications to low-level implementation models, and the conformance between different descriptions can be expressed by logical implication. The full logic of LTLC is undecidable. This paper will show that the existentially quantified fragment of LTLC is decidable. We achieve this goal by showing that the fragment can be translated into timed automata. Because the emptiness problem for timed automata is decidable, we then get a decision procedure for satisfiability for this fragment. This decidable part of LTLC is quite expressive. Many important real-time properties, such as bounded-response and bounded-invariance properties, can be expressed in it. The translation also enables us to develop a decision procedure for model checking real-time systems with quantifier-free LTLC specifications.