Compositionality for Cyber-Physical Systems Poster.pdf

The presentation materials cover results obtained for the two above-mentioned projects.  The poster presents material on an algebraic approach to modeling systems with both continuous and discrete behavior.  The framework is based on process algebra, which was developed for discrete systems, and features the development of a tree-based semantic model, called generalized synchronization trees, that uniformly captures a very general notions of time.  Composition operators then become operations over these trees, and notions of semantic equivalence based on bisimulation are generalized to this setting.  Recent work has focused on characterizing these equivalences logically.  Another line of work that has emerged based on this confluence of discrete and continuous behavior concerns cyber-security notions for cyber-physical systems.  In particular, notions of opacity that have been developed for discrete-event systems have been generalized to linear time-invariant systems.

The video concentrates on ongoing work devoted to model checking for hybrid systems.  Model checkers prove temporal properties automatically of systems; this work shows how a general-purpose technique based on proof search can be used to define a model checker for a very rich temporal logic, the modal mu-calculus.