The field is witnessing significant advancements in the development of safety-critical systems, with a focus on ensuring the reliability and correctness of autonomous and robotic systems. Innovations include the introduction of novel control strategies for discontinuous dynamics, enabling safer transitions within non-smooth safe sets. In the realm of timed automata, a new representation has been proposed to facilitate sound and complete timed bisimilarity checking, addressing a long-standing challenge in the verification of time-critical reactive systems. Additionally, there's a growing emphasis on the formal modeling and verification of robotic systems, particularly in the context of the Robot Operating System (ROS) 2, to guarantee correct behavior in real-time applications. Predictive monitoring techniques for black-box dynamical systems are also advancing, offering more accurate and computationally efficient methods for predicting safety violations. Furthermore, the validation of AI-based environment perception in automated driving systems is being enhanced through the development of function monitors that ensure compliance with safety regulations. Lastly, novel falsification approaches are being introduced to validate the behavior of autonomous systems in rich, uncertain environments, leveraging meta-planning techniques to improve the efficiency of finding falsifying examples.

Noteworthy Papers

• Safety-Critical Control of Discontinuous Systems with Nonsmooth Safe Sets: Introduces transition functions for safer control in discontinuous dynamics, enabling transitions between components of non-smooth safe sets.
• Checking Timed Bisimilarity with Virtual Clocks: Proposes a new representation of timed automata semantics for sound and complete timed bisimilarity checking, significantly reducing space requirements.
• Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis: Offers a trajectory repair technique that efficiently ensures compliance with traffic rules, saving computation time.
• Formal Modeling and Verification of Publisher-Subscriber Paradigm in ROS 2: Develops a framework for formal modeling and verification of ROS 2 programs, ensuring correct behavior in real-time robotic systems.
• Predictive Monitoring of Black-Box Dynamical Systems: Presents a novel framework for predictive runtime monitoring of black-box systems, enhancing safety prediction accuracy.
• A Method for the Runtime Validation of AI-based Environment Perception in Automated Driving System: Introduces a function monitor for the runtime validation of AI-based environment perception, ensuring safety compliance.
• Falsification of Autonomous Systems in Rich Environments: Contributes a novel falsification approach for autonomous systems, improving the efficiency of finding falsifying examples in rich environments.
• The behavioral approach for LPV data-driven representations: Advances data-driven analysis and control of LPV systems, offering stability and performance guarantees.