Efficient Computation of Timed Transition Relations

Finite State Machines (FSMs) are a convenient model for specification, analysis and synthesis of the control part of electronic systems. State traversal techniques have been developed to verify properties such as equivalence, reachability and so on for an FSM model. However, those techniques can be very expensive when applied in a synthesis environment, especially when the behavior involves long counting sequences. In this paper we address the problem of efficiently compute silent paths in an FSM. These paths are characterized by no observable activity under constant inputs. They can be used for a variety of applications, from verification, to synthesis, to simulation. In particular, we describe a new approach to compute the Timed Transition Relation of an FSM and we discuss a set of promising experimental results in which Timed Transition Relations are built.