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 [15] 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 (than that given in [15]).