(2022.10 - 2024.09, SymAware Project)
This research investigates formal specification and risk-aware control synthesis for multi-agent cyber-physical systems operating in uncertain environments.
Modern autonomous systems—including robotic teams, autonomous vehicles, and unmanned aerial systems—must execute complex missions while interacting with other agents and responding to unpredictable environmental changes. These missions are naturally described using temporal logic specifications, which capture high-level behavioral requirements such as safety, liveness, coordination, and task completion.
The central question of this research is:
How can controllers be synthesized from formal task specifications while remaining computationally scalable and robust to uncertainty and risk?
Rather than separating high-level planning from low-level control, this work focuses on integrating logical specifications, stochastic modeling, and control synthesis into a unified framework.
The resulting methods enable autonomous systems to reason about risk, interaction, and uncertainty while preserving formal correctness guarantees.
Applying formal specification-based control to real-world multi-agent systems introduces several fundamental difficulties:
Scalability limitations: temporal logic specifications often grow combinatorially with the number of agents and tasks.
Interactive uncertainty: agents must react to other agents whose intentions or behaviors are not fully known.
Specification conflicts: safety, task completion, and interaction constraints may compete with each other.
Runtime uncertainty: environmental conditions and task requirements may change during execution.
Traditional control methods based on Lyapunov analysis or transfer-function models do not directly accommodate high-level logical task specifications.
Conversely, classical formal synthesis approaches often struggle to incorporate uncertainty, stochastic reasoning, and runtime adaptability.
These limitations motivate the development of risk-aware formal control frameworks that combine logical guarantees with probabilistic reasoning.
This research develops scalable and uncertainty-aware synthesis methods for multi-agent systems under temporal logic specifications.
The work advances three complementary directions.
To address the computational complexity of temporal logic synthesis, this work introduces structured approaches that reduce specification complexity and enable modular controller design.
Key contributions include:
Specification decomposition techniques that split complex temporal logic formulas into tractable sub-specifications [7].
Modular synthesis frameworks for Signal Temporal Logic (STL) specifications.
Decentralized control architectures that distribute computation across agents [8].
These approaches significantly improve scalability and make formal synthesis feasible for larger multi-agent systems.
In interactive environments, the behavior of other agents may be uncertain or partially observable.
This work introduces belief-space and probabilistic models of agent intention to incorporate interaction uncertainty into control synthesis.
Key developments include:
Intention-aware control using belief-space temporal logic specifications [2]
Probabilistic modeling of agent behavior within formal control frameworks [2]
Refined risk models for resolving conflicting specifications [1]
These methods allow controllers to reason explicitly about uncertain agent intentions and interaction risks.
Real-world environments often require runtime adaptation when task specifications or environmental conditions change.
To address this challenge, this research develops risk-aware planning and control strategies that dynamically adapt to runtime conditions.
Key contributions include:
Risk-aware task allocation and rescheduling for stochastic multi-agent systems [4]
Risk-aware model predictive control under runtime temporal logic specifications [5]
Safety-driven replanning under environmental contracts [6]
These approaches enable autonomous systems to maintain safety guarantees while adapting to evolving mission conditions.
This research advances the practical applicability of formal specification-based control for autonomous multi-agent systems.
Key outcomes include:
Scalable synthesis methods for temporal logic specifications
Principled integration of probabilistic reasoning with formal guarantees
Risk-aware control strategies for uncertain multi-agent environments
The resulting framework bridges several research areas:
Formal methods and temporal logic
Stochastic control and decision theory
Multi-agent coordination
Safety-critical autonomous systems
The developed methods have been validated in autonomous driving and multi-agent coordination scenarios, demonstrating that formal correctness guarantees and scalable computation can coexist in complex uncertain environments.
In addition to risk-aware control synthesis, this research also explores how structural constraints influence uncertainty propagation in stochastic control systems.
Event-triggered control policies introduce communication-dependent truncations in probability distributions during state estimation.
Unlike classical Gaussian uncertainty propagation, these truncations generate nontrivial stochastic dynamics, which affect both control performance and risk evaluation.
This exploratory study analyzes:
How event-triggered communication reshapes uncertainty distributions
How truncated probabilistic models influence estimation and control
Implications for risk-aware decision-making in networked systems
The results provide theoretical insights into how structural control policies interact with uncertainty propagation in stochastic systems [3].
S. Qi, Z. Zhang, Z. Sun, S. Haesaert, “Risk-Aware Autonomous Driving for Linear Temporal Logic Specifications”, the IEEE/RJS International Conference on Intelligent RObots and Systems 2025, Hangzhou, China, Oct 19-25 2025. [IEEE Xplore][ArXiv]
Z. Zhang, Z. Sun, and S. Haesaert, “Intention-Aware Control Based on Belief-Space Specifications and Stochastic Expansion”, in IEEE Transactions on Intelligent Vehicles, vol. 10, no. 3, pp. 1989 - 1998, Mar 2025, DOI: 10.1109/TIV.2024. 3441315. [IEEE Xplore] [ArXiv]
Z. Zhang, Q. Liu, M. H. Mamduhi, S. Hirche, "Average Communication Rate for Event-Triggered Stochastic Control Systems", in IEEE Transactions on Control of Network Systems, vol. 12, no. 3, pp. 1894 - 1905, Feb 2025. [IEEE Xplore][arXiv]
M. H. W. Engelaar, Z. Zhang, E. E. Vlahakis, M. Lazar, and S. Haesaert, “Risk-Aware Real-Time Task Allocation for Stochastic Multi-Agent Systems under STL Specifications”, the 63rd IEEE Conference on Decision and Control (CDC 2024), Milan, Italy, Dec 16-19, 2024. [IEEE Xplore] [Arxiv]
M. H. W. Engelaar, Z. Zhang, M. Lazar, and S. Haesaert, "Risk-Aware MPC for Stochastic Systems with Runtime Temporal Logics", the 8th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2024), Boulder, the USA,1-3 July 2024. [ScienceDirect][Arxiv][ResearchGate]
S. Qi, Z. Zhang*, S. Haesaert, and Z. Sun, "Automated Formation Control Synthesis from Temporal Logic Specifications", 62nd IEEE Conference on Decision and Control (CDC 2023), Singapore, 13-15 Dec 2023.
Z. Zhang* and S. Haesaert, "Modularized Control Synthesis for Complex Signal Temporal Logic Specifications", 62nd IEEE Conference on Decision and Control (CDC 2023), Singapore, 13-15 Dec 2023.
N. Dang*, T. Brüdigam, Z. Zhang, F. Liu, M. Leibold, and M. Buss, "Distributed Stochastic Model Predictive Control for a Microscopic Interactive Traffic Model", in Electronics, vol. 12, no. 6, pp.1270, Mar. 2023, doi: 10.3390/electronics12061270. [MDPI]