Bisimulation in Behavioral Dynamical Systems and Generalized Synchronization Trees

Abstract

In this paper, we describe a method for representing a behavioral dynamical system as a Generalized Synchronization Tree (GST). The method of representation we propose is analogous to the ``unrolling'' of a Labeled Transition System (LTS) into a bisimilar Synchronization Tree (ST). Thus, for behavioral systems endowed with state maps, we are able to establish conditions under which bisimilar behavioral systems result in bisimilar GST representations and conversely. Preservation of bisimulation equivalence is critical to future study of composition operators for behavioral systems and GSTs. Additionally, we define a composition operator for GSTs constructed from behavioral systems, and prove a congruence result for strong bisimulation.