Autonomous agents increasingly interact with other independent agents, and such interactions typically admit multiple joint behaviors. When two agents prefer different ones, their independent strategies may be mutually incompatible and fail to reach a coordinated outcome; when they are identical, neither can differentiate its role when needed. Ideally, an agent should coordinate with any agent it encounters, regardless of which admissible joint behavior that agent aims to realize. We therefore propose a new form of strategy, the opinion-guided strategy, which keeps all the admissible joint behaviors available and postpones the selection to execution time, when the other agent's behavior reveals which one to realize. To realize this, nonlinear opinion dynamics are leveraged in a layered realization to guide the agent to a common admissible joint behavior in response to the other agent's evolving behavior, even without communication. We formally establish the conditions under which the strategy remains robust to every preference the other agent may hold. This robustness has an important implication: two agents running identical strategies can break symmetry when needed, a capability that conventional strategies lack. Three case studies across different applications show that the opinion-guided strategy coordinates with every randomly encountered agent, as long as it is willing to realize one of the admissible joint behaviors. One of them corresponds to a general-sum game: unlike conventional approaches devoted to finding a unique Nash equilibrium in advance, the opinion-guided strategy keeps every equilibrium open and guarantees the agents reach one, decided by their runtime interaction.

Real-time adaptive decision-making is essential in many stochastic applications, including air traffic control, converter regulation, and vehicle path planning. However, existing methods often impose rigid chance constraints or fail to guarantee constraint satisfaction under closed-loop dynamics. In response, this paper develops a risk-aware stochastic model predictive control (SMPC) framework that enables adaptability within chance constraints, mitigating the rigidity of traditional formulations while ensuring closed-loop constraint satisfaction in stochastic settings. To achieve this, we introduce elastic chance constraints-a flexible extension of conventional chance constraints that allows controlled adjustment of probability levels. By formulating an infinite-horizon stochastic optimization problem and approximating it with a deterministic, finite-horizon, tube-based model predictive control (MPC) formulation, we develop a risk-aware SMPC strategy expressed as an algorithm. Conditions ensuring closed-loop constraint satisfaction are established and embedded into the algorithm, together with stochastic stability guarantees expressed through an average asymptotic cost bound. The proposed SMPC algorithm is demonstrated on a DC-DC converter regulation problem and a vehicle path-planning scenario, both of which illustrate its effectiveness and broad applicability.

Discrete-time stochastic systems with continuous spaces are hard to verify and control, even with MDP abstractions due to the curse of dimensionality. We propose an abstraction-based framework with robust dynamic programming mappings that deliver control strategies with provable lower bounds on temporal-logic satisfaction, quantified via approximate stochastic simulation relations. Exploiting decoupled dynamics, we reveal a Canonical Polyadic Decomposition tensor structure in value functions that makes dynamic programming scalable. The proposed method provides correct-by-design probabilistic guarantees for temporal logic specifications. We validate our results on continuous-state linear stochastic systems.

By means of the linear parameter-varying (LPV) Fundamental Lemma, we derive novel data-driven predictive control (DPC) methods for LPV systems. In particular, we present output-feedback and state-feedback-based LPV-DPC methods with terminal ingredients, which guarantee exponential stability and recursive feasibility. We provide methods for the data-based computation of these terminal ingredients. Furthermore, an in-depth analysis of the application and implementation aspects of the LPV-DPC schemes is given, including application for nonlinear systems and handling noisy data. We compare and demonstrate the performance of the proposed methods in a detailed simulation example involving a nonlinear unbalanced disc system.

In this paper, we present a data-driven representation for linear parameter-varying (LPV) systems, which can be used for direct data-driven analysis and control of such systems. Specifically, we use the behavioral approach to develop a data-driven representation of the finite-horizon behavior of LPV systems for which there exists a kernel representation with shifted-affine scheduling dependence. Moreover, we provide a necessary and sufficient rank-based test on the available data that concludes whether the data fully represents the finite-horizon LPV behavior. Using the proposed data-driven representation, we also solve the data-driven simulation problem for LPV systems. Through multiple examples, we demonstrate that the results in this paper allow us to formulate a novel set of direct data-driven analysis and control methods for LPV systems, which are also applicable for LPV embeddings of nonlinear systems.

Correct-by-design synthesis provides a principled framework for establishing formal safety guarantees for stochastic multi-agent systems (MAS). However, conventional approaches based on finite abstractions often incur prohibitive computational costs as the number of agents and the complexity of temporal logic specifications increase. In this work, we study homogeneous stochastic MAS under counting linear temporal logic (cLTL) specifications, and show that the corresponding satisfaction probability admits a structured tensor decomposition via leveraging deterministic finite automata (DFA). Building on this structure, we develop a dual-tree-based value iteration framework that reduces redundant computation in the process of dynamic programming. Numerical results demonstrate the proposed approach's effectiveness and scalability for complex specifications and large-scale MAS.

Autonomous vehicles must plan trajectories that satisfy a multitude of requirements on safety, passenger comfort, and compliance with traffic rules. However, in safety-critical scenarios, it is not always possible to satisfy all requirements simultaneously, necessitating their prioritization based on importance. At the same time, in these safety-critical scenarios, the uncertainty in trajectory predictions of the surrounding traffic, such as other vehicles and pedestrians, should be explicitly accounted for. In this work, we propose an uncertainty-aware trajectory planning framework that incorporates a predefined lexicographic ordering over Signal Temporal Logic (STL) specifications that stays valid under uncertainty. We implement this formulation with Model Predictive Path Integral (MPPI) control and we demonstrate the effectiveness of our method on simulation scenarios, showing that our framework efficiently handles conflicting objectives under realistic multi-modal uncertainty.

While consciousness has been historically a heavily debated topic, awareness had less success in raising the interest of scholars. However, more and more researchers are getting interested in answering questions concerning what awareness is and how it can be artificially generated. The landscape is rapidly evolving, with multiple voices and interpretations of the concept being conceived and techniques being developed. The goal of this paper is to summarize and discuss the ones among these voices connected with projects funded by the EIC Pathfinder Challenge “Awareness Inside” callwithin Horizon Europe, designed specifically for fostering research on natural and synthetic awareness. In this perspective, we dedicate special attention to challenges and promises of applying synthetic awareness in robotics, as the development of mature techniques in this new field is expected to have a special impact on generating more capable and trustworthy embodied systems.

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year's edition of the competition. In particular, this report introduces three recently developed software tools, a new water distribution network benchmark, and a collection of simplified benchmarks intended to facilitate further comparisons among tools that were previously not directly comparable. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2025.

Formal safety guarantees on the synthesis of controllers for stochastic systems can be obtained using correct-by-design approaches. These approaches often use abstractions as finite-state Markov Decision Processes (MDPs). As the state space of these MDPs grows, the curse of dimensionality makes the computational and memory cost of the probabilistic guarantees, quantified with dynamic programming, scale exponentially. In this work, we leverage decoupled dynamics and unravel, via dynamic programming operations, a tree structure in the Canonical Polyadic Decomposition (CPD) of the value functions. For discrete-time stochastic systems with Deterministic Finite Automaton (DFA)-based temporal logic specifications, we provide provable probabilistic safety guarantees and significantly alleviate the computational burden. We provide numerical studies and validations of the theoretical results on several typical case studies and showcase that the uncovered tree structure enables efficient reductions in the computational burden.

We present SySCoRe 2.0, a MATLAB toolset that synthesizes controllers for stochastic systems to satisfy temporal logic specifications. Starting from a system description and a co-safe temporal logic specification, SySCoRe provides all necessary functions for synthesizing a robust controller and quantifying the associated formal robustness guarantees. It distinguishes itself from other available tools by supporting both stochastic model order reduction techniques and space discretizations, and by being applicable to nonlinear dynamics and complex co-safe temporal logic specifications over infinite horizons. To achieve this, SySCoRe generates a finite abstraction from a possibly reduced-order version of the provided model and performs probabilistic model checking. Then, it establishes a probabilistic coupling between the original model and its finite abstraction encoded in an approximate simulation relation, based on which a lower bound on the satisfaction probability is computed. The error computed by SySCoRe does not grow linearly in the horizon of the specification, thus it provides non-trivial lower bounds for infinite-horizon specifications and unbounded disturbances. SySCoRe exploits a tensor representation to facilitate an efficient computation of transition probabilities in the finite abstraction. We showcase these features on several benchmarks and compare the performance of the toolset with existing tools and with the previous version of SySCoRe.

This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. The focus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a class of robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form. We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systems that, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memory complexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of our methods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results.

As the airspace becomes increasingly congested, decentralized conflict resolution methods for airplane encounters have become essential. While decentralized safety controllers can prevent dangerous midair collisions, they do not always ensure prompt conflict resolution. As a result, airplane progress may be blocked for extended periods in certain situations. To address this blocking phenomenon, this paper proposes integrating bio-inspired nonlinear opinion dynamics into the airplane safety control framework, thereby guaranteeing both safety and blocking-free resolution. In particular, opinion dynamics enable the safety controller to achieve collaborative decision-making for blocking resolution and facilitate rapid, safe coordination without relying on communication or preset rules. Extensive simulation results validate the improved flight efficiency and safety guarantees. This study provides practical insights into the design of autonomous controllers for airplanes.

To enable autonomous driving in interactive traffic scenarios, various model predictive control (MPC) formulations have been proposed, each employing different interaction models. While higher-fidelity models enable more intelligent behavior, they incur increased computational cost. Since strong interactions are relatively infrequent in traffic, a practical strategy for balancing performance and computational overhead is to invoke an appropriate controller based on situational demands. To achieve this approach, we first conduct a comparative study to assess and hierarchize the interactive capabilities of different MPC formulations. Furthermore, we develop a neural network-based classifier to enable situation-aware switching among controllers with different levels of interactive capability. We demonstrate that this situation-aware switching can both substantially improve overall performance by activating the most advanced interactive MPC in rare but critical situations, and significantly reduce computational load by using a basic MPC in the majority of scenarios.

This paper presents a stochastic model predictive control (SMPC) algorithm for linear systems subject to additive Gaussian mixture disturbances, with the goal of satisfying chance constraints. We focus on a special case where each Gaussian mixture component has a similar variance. To solve the SMPC problem, we formulate a branch model predictive control (BMPC) problem on simplified dynamics and leverage stochastic simulation relations (SSR). Our contribution is an extension of the SMPC literature to accommodate Gaussian mixture disturbances while retaining recursive feasibility and closed-loop guarantees. We illustrate the retention of guarantees with a case study of vehicle control on an ill-maintained road.

Simulators are useful tools for testing automated driving controllers. Vehicle-in-the-loop (ViL) tests and digital twins (DTs) are widely used simulation technologies to facilitate the smooth deployment of controllers to physical vehicles. However, conventional ViL tests rely on full-size vehicles, requiring large space and high expenses. Also, physical-model-based DT suffers from the reality gap caused by modeling imprecision. This paper develops a comprehensive and practical simulator for testing automated driving controllers enhanced by scaled physical cars and AI-powered DT models. The scaled cars allow for saving space and expenses of simulation tests. The AI-powered DT models ensure superior simulation fidelity. Moreover, the simulator integrates well with off-the-shelf software and control algorithms, making it easy to extend. We use a filtered control benchmark with formal safety guarantees to showcase the capability of the simulator in validating automated driving controllers. Experimental studies are performed to showcase the efficacy of the simulator, implying its great potential in validating control solutions for autonomous vehicles and intelligent traffic.

Human drivers naturally balance the risks of different concerns while driving, including traffic rule violations, minor accidents, and fatalities. However, achieving the same behavior in autonomous driving systems remains an open problem. This paper extends a risk metric that has been verified in human-like driving studies to encompass more complex driving scenarios specified by linear temporal logic (LTL) that go beyond just collision risks. This extension incorporates the timing and severity of events into LTL specifications, thereby reflecting a human-like risk awareness. Without sacrificing expressivity for traffic rules, we adopt LTL specifications composed of safety and co-safety formulas, allowing the control synthesis problem to be reformulated as a reachability problem. By leveraging occupation measures, we further formulate a linear programming (LP) problem for this LTL-based risk metric. Consequently, the synthesized policy balances different types of driving risks, including both collision risks and traffic rule violations. The effectiveness of the proposed approach is validated by three typical traffic scenarios in Carla simulator.

This paper addresses the problem of data-driven computation of controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. With a focus on continuous-space stochastic systems with parametric uncertainty, we propose a two-stage approach that decomposes the problem into a learning stage and a robust formal controller synthesis stage. The first stage utilizes available Bayesian regression results to compute robust credible sets for the true parameters of the system. For the second stage, we introduce methods for systems subject to both stochastic and parametric uncertainties. We provide simulation relations for enabling correct-by-design control refinement that are founded on coupling uncertainties of stochastic systems via sub-probability measures. The presented relations are essential for constructing abstract models that are related to not only one model but to a set of parameterized models. The results are demonstrated on three case studies, including a nonlinear and a high-dimensional system.

The requirement for identifying accurate system representations has not only been a challenge to fulfill, but it has compromised the scalability of formal methods, as the resulting models are often too complex for effective decision making with formal correctness and performance guarantees. Focusing on probabilistic simulation relations and surrogate models of stochastic systems, we propose an approach that significantly enhances the scalability and practical applicability of such simulation relations by eliminating the need to compute error bounds directly. As a result, we provide an abstraction-based technique that scales effectively to higher dimensions while addressing complex nonlinear agent-environment interactions with infinite-horizon temporal logic guarantees amidst uncertainty. Our approach trades scalability for conservatism favorably, as demonstrated on a complex high-dimensional vehicle intersection case study.

This paper develops a correct-by-design controller for an autonomous vehicle interacting with opponent vehicles with unknown intentions. We define an intention-aware control problem incorporating epistemic uncertainties of the opponent vehicles and model their intentions as discrete-valued random variables. Then, we focus on a control objective specified as belief-space temporal logic specifications. From this stochastic control problem, we derive a sound deterministic control problem using stochastic expansion and solve it using shrinking-horizon model predictive control. The solved intention-aware controller allows a vehicle to adjust its behaviors according to its opponents' intentions. It ensures provable safety by restricting the probabilistic risk under a desired level. We show with experimental studies that the proposed method ensures strict limitation of risk probabilities, validating its efficacy in autonomous driving cases. This work provides a novel solution for the risk-aware control of interactive vehicles with formal safety guarantees.