Constructing (Bi)similar finite state abstractions using asynchronous l-complete approximations

This paper constructs a finite state abstraction of a possibly continuous-time and infinite state model in two steps. First, a finite external signal space is added, generating a so called φ-dynamical system. Secondly, the strongest asynchronous l-complete approximation of the external dynamics is constructed. As our main results, we show that (i) the abstraction simulates the original system, and (ii) bisimilarity between the original system and its abstraction holds, if and only if the original system is l-complete and its state space satisfies an additional property.