Automatic abstraction for worst-case analysis of discrete systems

Recently a methodology for worst-case analysis of discrete systems has been proposed by the author. The methodology relies on a user-provided abstraction of system components. In this paper the author proposes a procedure to automatically generate such abstractions for system components with Boolean transition functions. She use a binary decision diagram (BDD) of the transition function to generate a formula in Presburger arithmetic representing the desired abstraction. The author's experiments indicate that the approach can be applied to control-dominated embedded systems.