On identification of input/output extended automata with finite bisimilar quotients

We study the problem of finding a finite bisimilar abstraction for a class of reactive untimed infinite-state systems, modeled as input-output extended finite automata (I/O-EFA). We 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 termination condition is weaker than the one given in the work of Kumar et al. (2006) for the existence of a finite bisimilar quotient, and thus, the paper identifies a larger class of I/O-EFAs possessing a finite bisimilar abstraction.