Reachability Analysis Of Timed Transition Systems Based On Constraint Evaluation

Transition systems with timing constraints are a well known abstract representation of real time systems. Efficient analysis of timed transition systems is therefore a basis for real time verification. In this paper we introduce an algorithm for reachability analysis of timed transition systems with forced events which is based on an intuitive concept of constraint evaluation. During a depth-first search, the possible next states of each considered path are found by determining all transitions which are not in contradiction to the current timing constraints. The timing information is captured in a concise matrix representation for which a normal form is defined to guarantee the termination and improve the efficiency of the algorithm. 1 Introduction A model of a real time system can be obtained by augmenting a transition system with timing constraints. A transition system T is a 3-tupel (E; S; T ) of events, states and transitions. The system is always in one of its states s 2 S, and ..