Synthesis of Maximally Permissive Strategies for LTLf Specifications

Synthesis of Maximally Permissive Strategies for LTLf Specifications

Shufang Zhu, Giuseppe De Giacomo

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 2783-2789. https://doi.org/10.24963/ijcai.2022/386

In this paper, we study synthesis of maximally permissive strategies for Linear Temporal Logic on finite traces (LTLf) specifications. That is, instead of computing a single strategy (aka plan, or policy), we aim at computing the entire set of strategies at once and then choosing among them while in execution, without committing to a single one beforehand. Maximally permissive strategies have been introduced and investigated for safety properties, especially in the context of Discrete Event Control Theory. However, the available results for safety properties do not apply to reachability properties (eventually reach a given state of affair) nor to LTLf properties in general. In this paper, we show that maximally permissive strategies do exist also for reachability and general LTLf properties, and can in fact be computed with minimal overhead wrt the computation of a single strategy using state-of-the-art tools.
Keywords:
Knowledge Representation and Reasoning: Reasoning about actions
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis