Formal Synthesis of Supervisory Controllers under Linear Temporal Logic Constraints
When: Thursday, October 21, 2021, 3pm (CEST).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Formal Synthesis of Supervisory Controllers under Linear Temporal Logic Constraints.
Speaker: Ami Sakakibara, Postdoctoral researcher at the Division of Decision and Control Systems, KTH Royal Institute of Technology, Sweden.
Abstract
We consider a supervisory control problem of a discrete event system (DES), which is discrete-state, event-driven dynamical system model, in the presence of uncontrollable events. We aim to design an on-line supervisory controller that enforces the DES to satisfy a complex mission described by an syntactically co-safe linear temporal logic (scLTL) formula. In the precomputation process, we first compute a ranking function on the product automaton of the DES and an acceptor for the specification. The ranking function returns the minimum number of steps required to reach an accepting state from each state and embeds the influence of logical uncertainties modeled by uncontrollable events. We also show how to extend the ranking-function-based approach for different settings such as LTL over finite traces and multi-agent systems. The effectiveness of the proposed method is demonstrated in an illustrative example of a surveillance problem.
Short Bio
Ami Sakakibara is a postdoctoral researcher at the Division of Decision and Control Systems, KTH Royal Institute of Technology, Sweden, collaborating with Prof. Dimos Dimarogonas. She completed her PhD at the Graduate School of Engineering Science, Osaka University, Japan, under the supervision of Prof. Toshimitsu Ushio. Her research interests lie in formal synthesis, supervisory control, game theory, and reinforcement learning.