Modal Logic and Bisimulation for Generalized Synchronization Trees

This poster surveys results obtained by the project team in the area of logical characterizations for bisimulation over a general mathematical model for cyber-physical systems (CPSs) called Generalized Synchronization Trees (GSTs). GSTs extend traditional models for discrete-event systems with capabilities for modeling non-discrete behavior, and are intended to serve as a vehicle for giving mathematically well-defined notions of compositions for CPSs. Bisimulation represents a notion of equivalence over GSTs that captures when two GSTs are indistinguishable to an outside observer. The work described in the poster shows how the notion of bisimulation may be captured logically, in the following sense: two GSTS are bisimulation equivalent when they satisfy the same set of (very simple) formulas in modal logic.