arXiv subjects

Sofie Haesaert

Publications and source records attributed to Sofie Haesaert.

At least 19 recordsLinked to original sources

arXiv2026

GNN-Accelerated Mixed-Integer Dual MPC for Interactive Driving

In interactions with uncertain opponents, dual model predictive control (MPC) can improve performance through information-seeking actions that reduce uncertainty about opponents' behavior. Its recent applications to autonomous driving, however, are limited to scenarios involving a single opponent on a single lane. This paper presents a mixed-integer dual MPC for multiple reactive opponents on multi-lane roads, jointly optimizing integer-valued maneuver decisions (lane changes and safe-region selections), and continuous motion over a scenario tree that samples plausible interactions with the opponents. As interaction complexity increases, solving the resulting mixed-integer nonlinear program becomes increasingly expensive. To reduce this computational burden, a graph neural network (GNN) predicts the optimal maneuver decisions, and high-confidence predictions are fixed before the reduced problem is solved. Simulations show that active probing behavior emerges in complex interactive scenarios, and that GNN guidance fixes $76.3\%$ of the integer decisions and reduces the solve time by $2.5\times$ on average, with negligible degradation of optimality.

eess.SY↗

arXiv2026

Opinion-Guided Layered Strategies for Decentralized Coordination

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.

cs.MA↗

arXiv2026

Autonomous Driving with Priority-Ordered STL Specifications Under Multimodal Uncertainty

Autonomous vehicles must plan trajectories that satisfy multiple requirements, such as safety, traffic-rule compliance, and passenger comfort. 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, the uncertainty in the predicted trajectories of surrounding road users, such as other vehicles and pedestrians, must be explicitly accounted for. In this work, we propose an uncertainty-aware trajectory planning framework that incorporates a predefined priority ordering over Signal Temporal Logic (STL) specifications and preserves the induced lexicographic ordering under multimodal uncertainty. We implement this formulation with Model Predictive Path Integral (MPPI) control and demonstrate the effectiveness of our method on simulation scenarios, showing that our framework efficiently handles conflicting objectives under realistic multimodal uncertainty.

cs.RO↗

arXiv2026

Situation-Aware Interactive MPC Switching for Autonomous Driving

Autonomous driving in interactive traffic scenarios remains challenging because of the mutual influence among vehicles and the inherent uncertainty of surrounding agents. Several model predictive control (MPC) formulations have been proposed to address this challenge, each adopting a different model of inter-agent interaction. While higher-fidelity interaction models enable more intelligent behavior, they incur substantially greater computational cost. Since strong interactions arise only occasionally in real traffic, a practical strategy for balancing performance and computational overhead is to invoke an appropriate controller based on situational demands. To this end, we first conduct a comparative study to assess and hierarchize the interactive capabilities of different MPC formulations. Building on this hierarchy, we then develop a neural network-based classifier for situation-aware switching among these controllers. We demonstrate that, by invoking the most advanced interactive MPC only in rare but critical situations and relying on a basic MPC in the majority of situations, situation-aware switching substantially improves overall performance while significantly reducing computational load.

cs.RO↗

arXiv2026

Unraveling tensor structures in correct-by-design controller synthesis

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. 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 syntactically co-safe linear temporal logic (scLTL) specifications, we provide provable probabilistic safety guarantees and significantly alleviate the computational burden. We provide an initial validation of the theoretical results on several typical case studies and showcase that the uncovered tree structure enables efficient reductions in the computational burden.

eess.SY↗

arXiv2026

Correct-by-Design Control Synthesis of Stochastic Multi-agent Systems: a Robust Tensor-based Solution

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.

eess.SY↗

arXiv2026

Compressing Correct-by-Design Synthesis for Stochastic Homogeneous Multi-Agent Systems with Counting LTL

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.

eess.SY↗

arXiv2026

Risk-Aware Autonomous Driving with Linear Temporal Logic Specifications

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.

eess.SY↗

arXiv2025

A Linear Parameter-Varying Approach to Data Predictive Control

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.

eess.SY↗

arXiv2025

Integrating Opinion Dynamics into Safety Control for Decentralized Airplane Encounter Resolution

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.

eess.SY↗

arXiv2025

A Vehicle-in-the-Loop Simulator with AI-Powered Digital Twins for Testing Automated Driving Controllers

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.

cs.RO↗

arXiv2025

A behavioral approach for LPV data-driven representations

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.

eess.SY↗

arXiv2025

Stochastic MPC for Finite Gaussian Mixture Disturbances with Guarantees

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.

eess.SY↗

arXiv2025

ARCH-COMP25 Category Report: Stochastic Models

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.

cs.LO↗

arXiv2025

Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)

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.

eess.SY↗

arXiv2025

Avoiding Deadlocks Is Not Enough: Analysis and Resolution of Blocked Airplanes

This paper is devoted to the analysis and resolution of a pathological phenomenon in airplane encounters called blocking mode. As autonomy in airplane systems increases, a pathological phenomenon can be observed in two-aircraft encounter scenarios, where airplanes stick together and fly in parallel for an extended period. This parallel flight results in a temporary blocking that significantly delays progress. In contrast to widely studied deadlocks in multi-robot systems, such transient blocking is often overlooked in existing literature. Since such prolonged parallel flying places high-speed airplanes at elevated risks of near-miss collisions, encounter conflicts must be resolved as quickly as possible in the context of aviation. We develop a mathematical model for a two-airplane encounter system that replicates this blocking phenomenon. Using this model, we analyze the conditions under which blocking occurs, quantify the duration of the blocking period, and demonstrate that the blocking condition is significantly less restrictive than that of deadlock. Based on these analytical insights, we propose an intention-aware strategy with an adaptive priority mechanism that enables efficient resolution of ongoing blocking phenomena while also incidentally eliminating deadlocks. Notably, the developed strategy does not rely on central coordination and communications that can be unreliable in harsh situations. The analytical findings and the proposed resolution strategy are validated through extensive simulations.

eess.SY↗

arXiv2025

Scalable control synthesis for stochastic systems via structural IMDP abstractions

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.

eess.SY↗

arXiv2025

VernaCopter: Disambiguated Natural-Language-Driven Robot via Formal Specifications

It has been an ambition of many to control a robot for a complex task using natural language (NL). The rise of large language models (LLMs) makes it closer to coming true. However, an LLM-powered system still suffers from the ambiguity inherent in an NL and the uncertainty brought up by LLMs. This paper proposes a novel LLM-based robot motion planner, named \textit{VernaCopter}, with signal temporal logic (STL) specifications serving as a bridge between NL commands and specific task objectives. The rigorous and abstract nature of formal specifications allows the planner to generate high-quality and highly consistent paths to guide the motion control of a robot. Compared to a conventional NL-prompting-based planner, the proposed VernaCopter planner is more stable and reliable due to less ambiguous uncertainty. Its efficacy and advantage have been validated by two small but challenging experimental scenarios, implying its potential in designing NL-driven robots.

cs.RO↗