Towards Formal Linear Multi-Agent Stochastic Model Predictive Control with Temporal Logic Specifications: A Risk-Aware and Formal Abstraction Approach

Control design, a foundational discipline in engineering and applied mathematics, encompasses a wide range of techniques and applications. Prominent industrial examples include lithography, assembly robots, and large-scale electrical power networks. Societal applications, on the other hand, feature drones, cars, and other autonomous navigational systems that often require cooperation to execute demanding, time-sensitive tasks safely. Such cooperation introduces intricate inter-agent dependencies that require coordinated decision-making during execution. Furthermore, not all requirements are specified in advance; some emerge during operation, making adaptability essential. At the same time, uncertainty in system dynamics and observations makes the control problem inherently stochastic. Taken together, cooperation, adaptability, and stochasticity form the central focus of this thesis, which develops formal control synthesis methods for stochastic multi-agent linear systems under the assumption that tasks may be introduced during runtime. Several key challenges emerge from this context. First, to achieve adaptability requires flexible planning under stochastic uncertainty while ensuring satisfaction of cooperative specifications. At the same time, excessive flexibility can undermine formal guarantees, underscoring the need for well-defined criteria that strike a balance between adaptability and rigour. Second, as in many stochastic control problems, scalability is crucial: computational demands increase rapidly with system complexity. Addressing this challenge requires principled methods to reduce both system complexity and computational cost while preserving correctness. In deterministic multi-agent systems, time-critical tasks expressed in temporal logic language have been integrated with control design methods such as Model Predictive Control (MPC), enabling adaptability at the control input level, while ensuring formal guarantees. In contrast, in stochastic single-agent systems, temporal logic language has been combined with Stochastic Simulation Relations (SSRs) to achieve scalable control while preserving the satisfaction of requirements. This thesis aims to bridge both approaches by developing a unified framework for stochastic multi-agent linear systems subject to temporal logic tasks provided at runtime. To tackle adaptability, this thesis introduces novel techniques within the framework of Stochastic Model Predictive Control (SMPC). First, a risk-aware SMPC method is proposed that allows for probability-adaptable polytopic constraints in the single-agent setting, while simultaneously ensuring constraint satisfaction, stability, and recursive feasibility. By enabling the adjustment of constraint satisfaction probabilities, the resulting framework achieves a careful balance between adaptability and the maintenance of rigorous formal guarantees. Building on this foundation, runtime temporal logic specifications—specifically Signal Temporal Logic (STL)—are then incorporated, allowing temporal logic tasks to be updated dynamically during execution without compromising the correctness or feasibility of the control strategy. This capability ensures that the control framework can respond flexibly to evolving mission objectives or environmental conditions. Finally, the framework is extended to heterogeneous multi-agent systems through decomposition of STL specifications, task allocation using heuristic filtering, and auction-based mechanisms for decentralized coordination. This extension enables the systematic distribution of temporal logic tasks among agents, facilitating both adaptability and cooperation in a decentralized control setting. Collectively, these contributions develop adaptable, correct-by-design stochastic model predictive control techniques that address both conventional chance constraints and runtime-provided signal temporal logic specifications, applicable in both single-agent and multi-agent contexts. To address scalability, the thesis develops two complementary formal abstraction techniques. The first approach considers disturbances as Gaussian mixtures, which can approximate arbitrary continuous disturbance distributions with high fidelity, providing a highly expressive representation of uncertainty. To maintain scalability in this expressive setting, stochastic simulation relations are employed to reduce the original system to an equivalent system with Gaussian and finite discrete disturbances. This approach is particularly effective at reducing structural complexity while retaining a formal correspondence between the original and abstracted systems. The second technique combines knowledge filtering with optimal Kalman filtering to reduce the dimensionality of Gaussian disturbances, directly addressing the challenges associated with high-dimensional uncertainty in stochastic control. Both abstraction methods guarantee that controllers synthesized on the reduced system can be rigorously refined and applied to the original system, preserving formal correctness and ensuring the correct-by-design property. All proposed theoretical developments are validated through academic simulations demonstrating the effectiveness and versatility of both the risk-aware SMPC approach and the formal abstraction methods. Single-agent control includes applications such as DC–DC converter regulation, vehicle path planning, and vehicle control over ill-maintained roads, illustrating both runtime adaptability and the satisfaction of stochastic constraints. In the multi-agent context, the framework is applied to a multi-shuttle system, showcasing dynamic allocation of temporal logic tasks among heterogeneous agents while maintaining correct-by-design behaviour. Finally, the formal abstraction techniques are demonstrated through academic examples, confirming their ability to reduce structural and dimensional complexity.