Clock specifications for temporal tasks in planning and learning

Conference item

Recently, Linear Temporal Logics on finite traces, such as LTL_𝑓 (or LDL_𝑓 ), have been advocated as high-level formalisms to express dynamic properties, such as goals in planning domains or rewards in Reinforcement Learning (RL). This paper addresses the challenge of separating high-level temporal specifications from the low-level details of the underlying environment (domain or MDP), by allowing for expressing the specifications at a different time granularity than the environment. We study the notion of a clock which progresses the high-level LTL_𝑓 specification, whose ticks are triggered by dynamic (low-level) properties defined on the underlying environment. The obtained separation enables terse high-level specifications while allowing for very expressive forms of clock expressed as general LTL_𝑓 properties over low-level features, such as counting or occurrence/alternation of special events. We devise an automata-based construction to compile away the clock into a deterministic automaton that is polynomial in the size of the automata characterizing the high-level and clock specifications. We show the correctness of the approach and discuss its application in several contexts, including FOND planning, RL with LTL_𝑓 Restraining Bolts, and Reward Machines.

Authors: De Giacomo, G; Favorito, M; Patrizi, F

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: CEUR Workshop Proceedings
• Host title: Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2023)
• Volume: 3629
• Pages: 93-98
• Series: Italian Association for Artificial Intelligence (AIxIA)
• Publication date: 2024-01-29
• Acceptance date: 2023-10-04
• Event title: 5th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2023)
• Event location: Rome, Italy
• Event website: https://overlay.uniud.it/workshop/2023/
• Event start date: 2023-11-07
• Event end date: 2023-11-07
• ISSN: 1613-0073
• Language: English
• Keywords: automata theory; planning and learning for temporal tasks; temporal logics