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. This sufficient condition is existential as it relies on the existence of a suitable partition of the state space. 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