This project develops a formal framework that enables autonomous vehicles, infrastructure, and cloud services to automatically negotiate, verify, and enforce safe cooperation through Behavior-Level Agreements (BLAs).
Behavior-Level Agreements for Automatic Cooperation in Intelligent Transportation Systems.
Project description
Future intelligent transportation systems depend on cooperation between heterogeneous cyber-physical systems, including automated vehicles, connected infrastructure, and cloud services. However, current approaches typically address cooperation within narrowly defined scenarios and lack a general framework for reasoning about cooperation itself—when it should be formed, how it should be structured, and how safety can be guaranteed. This project introduces Behavior-Level Agreements (BLAs), inspired by service-level agreements in cloud computing, as a formal mechanism to define, verify, and enforce cooperation guarantees among agents . By integrating temporal logic, reachability analysis, and assume/guarantee contracts, the project enables continuous online refinement of admissible behaviors under uncertainty and dynamic reconfiguration. The overall goal is to establish scalable, safe, and accountable automatic cooperation in complex traffic environments such as intelligent intersections and charging hubs.
Subproject 1 – Design and Formalization of Behavior-Level Agreements (PhD student Kaj Munhoz Arfvidsson)
This subproject develops the formal foundations of BLAs as a scalable framework for specifying and verifying cooperation in heterogeneous transport systems . BLAs are defined using assume/guarantee contracts combined with temporal logic and reachability analysis to express safety, liveness, and performance conditions across agents. The research focuses on how agreements are formed, negotiated, refined, and dissolved in real time as system configurations change.
A central contribution is the development of scalable online behavior refinement algorithms that check consistency between multiple BLAs and compute the resulting admissible behavior sets. The framework supports cooperation across abstraction levels—for example, between route-level decisions and low-level motion planning—and across independent agents with different dynamics and capabilities.
This subproject will result in a generalized BLA theory with formal guarantees, a software toolchain integrating Temporal Logic Trees with contract-based verification, and large-scale simulation studies evaluating robustness, negotiation overhead, and behavior-space contraction under uncertainty .
Subproject 2 – Control under Behavior-Level Agreements (PhD student Yidan Zhu)
The second subproject translates formally defined BLAs into real-time control architectures . Here, the focus is on how reachable behavior sets and contract guarantees can guide planners and controllers while ensuring recursive feasibility, stability, and safety under time-varying agreements.
The research develops interfaces that convert high-level BLA guarantees into control constraints, safety filters, or barrier-based conditions that can be enforced at the motion control layer. It also studies trade-offs between safety, efficiency, and responsiveness, particularly in situations where agreements change dynamically or become infeasible. In such cases, strategies for graceful degradation and fallback are designed to ensure that agents remain safe and operational even when cooperation must be updated or dissolved.
Validation will be carried out both in simulation and in a physical small-scale vehicle testbed, enabling experimental assessment of BLA-aware control in realistic cooperative transport scenarios . Expected outcomes include control architectures that natively incorporate cooperation guarantees, real-time safety filtering mechanisms, and design guidelines for deploying BLA-driven control in safety-critical multi-agent environments.
Project facts
Partner
KTH
Funded by
WASP (Wallenberg AI, Autonomous Systems and Software Program)
