A modal characterization of alternating approximate bisimilarity

Recently, alternating transition systems are adopted to describe control systems with disturbances and their finite abstract systems. In order to capture the equivalence relation between these systems, a notion of alternating approximate bisimilarity is introduced. This paper aims to establish a modal characterization for alternating approximate bisimilarity. Based on this result, we provide a link between specifications satisfied by the samples of control systems with disturbances and their finite abstractions. Moreover, a simple example is given to illustrate the application of such link in the design of controller of control systems.