Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata With Variables

Some discrete-event systems such as software are typically infinite state systems, and a commonly used technique for performing formal analysis such as automated verification is based on their finite abstractions. In this paper, we consider a model for reactive untimed infinite state systems called input-output extended finite automaton (I/O-EFA), which is an automaton extended with discrete variables such as inputs, outputs, and data. Using I/O-EFA as a model many value-passing processes can be represented by finite graphs. We study the problem of finding a finite abstraction that is bisimilar to a given I/O-EFA. We present a sufficient condition under which the underlying transition system of an I/O-EFA admits a finite bisimilar quotient. We then identify a class of I/O-EFAs for which a partition satisfying our sufficient condition can be constructed by inspecting the structure of the given I/O-EFA. We also identify a lower bound abstraction (that is coarser than any finite bisimilar abstraction), and present an iterative refinement algorithm whose termination guarantees the existence of a finite bisimilar abstraction. The results are illustrated through examples that model reactive software.