Clocked Transition Systems
Zohar Manna, Amir Pnueli · 1996
. This paper presents a new computational model for realtime systems, called the clocked transition system model. The model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. For verifying safety properties, we present a run-preserving reduction from the new real-time model to the untimed model of fair transition systems. This reduction allows the (re)use of safety verification methods and tools, developed for untimed reactive systems, for proving safety properties of real-time systems. 1 Introduction A formal framework for specifying and verifying temporal properties of reactive systems often contains the following components: ffl A computational model defining the set of behaviors (computations) that are to be associated with systems in the considered model. ffl A requirement...