Security-Aware Planning and Control of Multi-Agent Systems with LTL Tasks

TL;DR

This paper introduces a formal framework for planning and control of multi-agent systems that ensures security by preventing intruders from inferring secret tasks or identifying responsible agents, while satisfying LTL specifications.

Contribution

It integrates security constraints directly into LTL synthesis, creating a secure planning method with formal guarantees for multi-agent systems.

Findings

Framework successfully prevents intruder inference of secret tasks.

Secure plans satisfy global LTL and security constraints.

Validated through a two-drone case study.

Abstract

This paper presents a secure-by-construction planning and control framework for multi-agent systems subject to linear temporal logic (LTL) specifications. The framework protects sensitive information from a passive intruder with partial observations of the agents' motion. Security in multi-agent coordination is captured by two notions that prevent the intruder from inferring whether a secret task has been executed and from identifying the agent responsible for its execution. The proposed framework incorporates the security constraints directly into the LTL synthesis procedure by constructing a secure finite transition system that removes all paths violating these constraints. Standard LTL synthesis is then applied to this secure abstraction to generate discrete plans, which are then refined into dynamically feasible continuous trajectories. This synthesis procedure provides formal guarantees that the resulting behavior of the multi-agent system satisfies both the global LTL specification and the security constraints. The effectiveness of the proposed framework is demonstrated through a two-drone case study.