Security-Aware Planning and Control of Multi-Agent Systems with LTL Tasks
It addresses security concerns in multi-agent coordination for applications requiring privacy, but the contribution is incremental as it integrates existing security notions into LTL synthesis.
This paper proposes a secure-by-construction planning and control framework for multi-agent systems with LTL tasks, ensuring that a passive intruder cannot infer secret task execution or identify the responsible agent. The framework is validated through a two-drone case study.
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.