Clock specifications for temporal tasks in planning and learning
Recently, Linear Temporal Logics on finite traces, such as LTL<sub>𝑓</sub> (or LDL<sub>𝑓</sub> ), 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...
| Hlavní autoři: | , , |
|---|---|
| Médium: | Conference item |
| Jazyk: | English |
| Vydáno: |
CEUR Workshop Proceedings
2024
|
| _version_ | 1826312742206701568 |
|---|---|
| author | De Giacomo, G Favorito, M Patrizi, F |
| author_facet | De Giacomo, G Favorito, M Patrizi, F |
| author_sort | De Giacomo, G |
| collection | OXFORD |
| description | Recently, Linear Temporal Logics on finite traces, such as LTL<sub>𝑓</sub> (or LDL<sub>𝑓</sub> ), 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<sub>𝑓</sub> 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<sub>𝑓</sub> 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<sub>𝑓</sub> Restraining Bolts, and Reward Machines. |
| first_indexed | 2024-04-23T08:25:04Z |
| format | Conference item |
| id | oxford-uuid:14fc64fc-2aa8-4c5e-8dfb-e3efc4944eac |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-04-23T08:25:04Z |
| publishDate | 2024 |
| publisher | CEUR Workshop Proceedings |
| record_format | dspace |
| spelling | oxford-uuid:14fc64fc-2aa8-4c5e-8dfb-e3efc4944eac2024-04-15T15:11:12ZClock specifications for temporal tasks in planning and learningConference itemhttp://purl.org/coar/resource_type/c_5794uuid:14fc64fc-2aa8-4c5e-8dfb-e3efc4944eacEnglishSymplectic ElementsCEUR Workshop Proceedings2024De Giacomo, GFavorito, MPatrizi, FRecently, Linear Temporal Logics on finite traces, such as LTL<sub>𝑓</sub> (or LDL<sub>𝑓</sub> ), 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<sub>𝑓</sub> 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<sub>𝑓</sub> 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<sub>𝑓</sub> Restraining Bolts, and Reward Machines. |
| spellingShingle | De Giacomo, G Favorito, M Patrizi, F Clock specifications for temporal tasks in planning and learning |
| title | Clock specifications for temporal tasks in planning and learning |
| title_full | Clock specifications for temporal tasks in planning and learning |
| title_fullStr | Clock specifications for temporal tasks in planning and learning |
| title_full_unstemmed | Clock specifications for temporal tasks in planning and learning |
| title_short | Clock specifications for temporal tasks in planning and learning |
| title_sort | clock specifications for temporal tasks in planning and learning |
| work_keys_str_mv | AT degiacomog clockspecificationsfortemporaltasksinplanningandlearning AT favoritom clockspecificationsfortemporaltasksinplanningandlearning AT patrizif clockspecificationsfortemporaltasksinplanningandlearning |