Session 1: Structural Properties in Controller Synthesis

January 18th, 2023

Talk 1:  Compositional synthesis using the least-violating control framework.

by Antoine Girard (L2S – CentraleSupélec, France)

Compositional synthesis is a powerful approach to designing distributed control systems. An important challenge in compositional synthesis is to derive local specifications for components from a global system-level specification. In this talk, I will show how this can be done using the least-violating control framework, which aims at synthesizing controllers enforcing a closed-loop behavior that is the closest to a correct one. In particular, we will see how least-violating controllers can help us finding suitable assume-guarantee contracts for components from a given global safety or attractivity specification. We will illustrate our main results using numerical applications in abstraction based control design.

Talk 2: Unified Bisimulation for Compositional Verification, Synthesis and Time Optimization.

by Bengt Lennartson (Chalmers University of Technology, Sweden)

An alternative and simplified formulation of bisimulation is presented in this talk, based on equivalent block state transitions. This formulation unifies strong, weak, stuttering, and branching bisimulation, including both state and event labels in the abstraction. Applying this bisimulation abstraction on modular systems, where local events are identified incrementally and abstracted after each synchronization, is shown to generate efficient algorithms for model checking, modular opacity verification, and controller synthesis. This abstraction can be applied to different model structures, including modular Petri nets with shared variables and modular hybrid systems. Time optimization of modular systems based on timed automata is also shown to be efficiently solved by a combination of time optimal bisimulation and a modular A* search. Most of the concepts presented in this talk have been formulated in such a simple way that they have been included in an introductory course on discrete event systems in the master’s program Systems, Control and Mechatronics at Chalmers University of Technology.

Talk 3: Compositional verification and synthesis of interconnected control systems

by Majid Zamani (University of Colorado, Boulder, United States)

In this talk, I will present our recent results on compositional verification and synthesis of interconnected control systems against high-level temporal logic requirements. I propose a divide and conquer strategy to scale our proposed techniques by leveraging the natural structure present in the system to break the verification and synthesis problem into semi-independent ones. I will leverage small-gain type reasoning and notions of barrier certificates as two key tools to tackle the verification and synthesis complexity. I will illustrate the effectiveness of the proposed results on some case studies. I will show that our proposed results can handle large-scale complex systems, which would not have been possible to tackle using existing monolithic approaches.

Session 2: Information-Flow Properties in Dynamic Systems

February 15th, 2023

Talk 1: Probabilistic Hyperproperties of Markov Decision Processes: Information-Flow Properties and Beyond

by Rayna Dimitrova (Helmholtz Center for Information Security, Saarbrücken, Germany)

Hyperproperties describe the correctness of a system as a relation between multiple executions. They generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance.
In this talk, I will present a recently introduced temporal logic for the specification of hyperproperties of Markov decision processes (MDPs), called Probabilistic Hyper Logic (PHL). PHL extends classic probabilistic logics with quantification over schedulers and traces. It can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference and differential privacy, as well as novel applications in areas such as planning. A consequence of the generality of the logic is that the model-checking problem for PHL is undecidable. I will present methods both for proving and for refuting formulas from a fragment of the logic that includes many probabilistic hyperproperties of interest.

Talk 2: A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems

by Xiang Yin (Shanghai Jiao Tong University, Shanghai, China)

In this talk, we discuss property verification problems in partially-observed discrete-event systems (DES). Particularly, we are interested in verifying observational properties that are related to the information-flow of the system. Observational properties considered here include diagnosability, predictability, detectability and opacity, which have drawn considerable attentions in the literature. However, in contrast to existing results, where different verification procedures are developed for different properties case-by-case, in this talk, we introduce a unified framework for verifying all these properties by reducing each of them as an instance of HyperLTL model checking. Our approach is based on the construction of a Kripke structure that effectively captures the issue of unobservability as well as the finite string semantics in partially- observed DES so that HyperLTL model checking techniques can be suitably applied. Then for each observational property considered, we explicitly provide the HyperLTL formula to be checked over the Kripke structure for the purpose of verification. Our approach is uniform in the sense that all different properties can be verified with the same model checking engine. Furthermore, our unified framework also brings new insights for classifying observational properties for partially-observed DES in terms of their verification complexity.