Verification of infinite-state dynamic systems using approximate quotient transition systems

This paper concerns computational methods for verifying properties of labeled infinite-state transition systems (e.g., hybrid systems) using quotient transition system (QTS). A QTS is a conservative approximation to the infinite-state transition system based on a finite partition of the infinite state space. For universal specifications, positive verification for a QTS implies the specification is true for the infinite-state transition system. Since in most applications exact reachability mappings required to compute the QTS cannot be represented or computed, we introduce the approximate quotient transition system (AQTS). The AQTS is an approximation to the QTS obtained from a conservative approximation to the reachability mapping. The paper presents a sufficient condition for an AQTS to be a bisimulation of the infinite state transition system. An AQTS bisimulation is essentially equivalent to the infinite-state system for the purposes of verification. It is well known, however, that finite-state bisimulations do not exist for most hybrid systems of practical interest. Therefore, the use of the AQTS for verification of universal specifications is proposed and illustrated with an example. This approach has been implemented in a tool for computer-aided verification of a general class of hybrid systems.