An Embedding of Timed Transition Systems in HOL

The theory of Timed Transition Systems (TTSs) developed by Henzinger, Manna and Pnueli provides a formal framework for specifying and reasoning about realtime systems. In this theory a system is described by a set of state transitions with associated time constraints. We report on work in progress to mechanize the published theory of timed transition systems using the HOL theorem prover. Different specification languages may be defined in terms of the TTS model. In particular, a real-time temporal logic (RTTL) has been used for specifying requirements and a graphical notation for specifying system designs. A semantics for each of these languages can be given in terms of TTSs, which can in turn be represented in the HOL logic, and these common semantic interpretations enable formal proofs that one specification satisfies another. 1 Introduction The theory of Timed Transition Systems developed by Henzinger, Manna and Pnueli provides a formal framework for specifying and reasoning about ..