Automatic abstraciton for worst-case analysis of discrete systems
Felice Balarin · 2000
Recently, a methodology for worst-case analysis of discrete systems has been proposed [1,2].The methodology relies on a user-provided abstraction of system components.In this paper we propose a procedure to automatically generate such abstractions for system components with Boolean transition functions.We use a binary decision diagram (BDD) of the transition function to generate a formula in Presburger arithmetic representing the desired abstraction.Our experiments indicate that the approach can be applied to control-dominated embedded systems.