Slicing of Timed Automata with Discrete Data

The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic CTL _{-X} *.