Bisimulation based hierarchical system architecture for single-agent multi-modal systems

In this paper, a hierarchical system architecture for single-agent multi-modal systems is proposed. The layered system is designed to promote proof obligations so that system specification at one level of granularity conforms with that at another level and vice versa. The design principle for the construction of the hierarchy is based on bisimulation with respect to reachability specifications. Therefore, a higher-level system and a lower-level system axe bisimilar. Our approach is illustrated by designing a system architecture for controlling an autonomous agent.