This program is tentative and subject to change.

Cyber-physical systems (CPSs) must meet safety-critical requirements and optimization goals. Reactive controller synthesis (RCS) from temporal logic (TL) specifications can automatically construct agent behaviors that ensure safety and liveness. However, RCS struggles with time and probability aspects. Reinforcement Learning (RL) can optimize system behaviors, but cannot guarantee correctness. RL and RCS can be combined by shielding an agent with a synthesized controller, ensuring that the agent behavior satisfies the TL specification. However, this requires aligning different models: the TL specification and the often hand-crafted RL training environment code. We propose a three-step method, centered around code generation and manual refinement, for streamlining this alignment: (1) Formalize discrete environment assumptions and guarantees into a Spectra TL specification. (2) From it, automatically generate Gymnasium-compatible training environment code. For the target code, we employ BPpy, which enables a unique one-to-one mapping of the Spectra properties to individual code modules. This allows users to refine time and probability aspects as well as optimization goals without misaligning the models. (3) Synthesize a permissive controller from the TL specification and integrate it as a shield for the agent. In contrast to previous work, our approach (a) guarantees not only safety, but also liveness; (b) even if the system is too complex for RCS, we can leverage the generated BPpy code as a model-at-runtime that shields the agent from unsafe actions.

This program is tentative and subject to change.

Wed 8 Oct

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 17:30
Session 5: Quality Assurance and Model ManagementNew Ideas and Emerging Results (NIER) / Research Papers / Journal-First at DCIH 102

Hybrid

16:00
18m
Talk
Streamlined Integration of GR(1) Synthesis and Reinforcement Learning for Optimizing Critical Cyber-Physical SystemsFT@In Person
Research Papers
Eric Roslin Wete Poaka Leibniz Universität Hannover, Joel Greenyer FHDW Hannover, Tom Yaacov Ben-Gurion University of the Negev, Daniel Kudenko L3S Research Center, Leibniz Universität Hannover, Germany, Wolfgang Nejdl Leibniz Universität Hannover
16:18
18m
Talk
Refactoring with Confidence: An Assistant for Repair-Integrated Refactoring in Block-based Industrial ModelsPT@In Person
Research Papers
Michael Oberlehner LIT CPS Lab, Johannes Kepler University Linz, Bianca Wiesmayr LIT CPS Lab, Johannes Kepler University Linz, Alois Zoitl LIT CPS Lab, Johannes Kepler University Linz
16:36
18m
Talk
Inclusive Model-Driven Engineering for Accessible SoftwareIn Person
New Ideas and Emerging Results (NIER)
Dominik Bork TU Wien, Stefan Klikovits Johannes Kepler University, Linz, Judith Michael University of Regensburg, Lukas Netz RWTH Aachen University, Bernhard Rumpe RWTH Aachen University
Pre-print
16:54
18m
Talk
A Model Cleansing Pipeline for Model-driven Engineering: Mitigating the Garbage In, Garbage Out Problem for Open Model Repositories@RemoteFT
Research Papers
17:12
18m
Talk
Modeling with Gentleman: a web-based projectional editorRemote
Journal-First
Louis-Edouard Lafontant University of Montreal, Eugene Syriani Université de Montréal
DOI