Finite-trace and generalized-reactivity specifications in temporal synthesis
Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both...
| Автори: | , , , , |
|---|---|
| Формат: | Journal article |
| Мова: | English |
| Опубліковано: |
Springer
2023
|
| _version_ | 1826313014274424832 |
|---|---|
| author | De Giacomo, G Di Stasio, A Tabajara, LM Vardi, MY Zhu, S |
| author_facet | De Giacomo, G Di Stasio, A Tabajara, LM Vardi, MY Zhu, S |
| author_sort | De Giacomo, G |
| collection | OXFORD |
| description | Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) environment specification. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis. |
| first_indexed | 2024-09-25T04:04:15Z |
| format | Journal article |
| id | oxford-uuid:db7f02cd-0eff-4ec8-bd0e-9cd00b17fdaa |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:04:15Z |
| publishDate | 2023 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:db7f02cd-0eff-4ec8-bd0e-9cd00b17fdaa2024-05-13T15:28:29ZFinite-trace and generalized-reactivity specifications in temporal synthesisJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:db7f02cd-0eff-4ec8-bd0e-9cd00b17fdaaEnglishSymplectic ElementsSpringer2023De Giacomo, GDi Stasio, ATabajara, LMVardi, MYZhu, SLinear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) environment specification. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis. |
| spellingShingle | De Giacomo, G Di Stasio, A Tabajara, LM Vardi, MY Zhu, S Finite-trace and generalized-reactivity specifications in temporal synthesis |
| title | Finite-trace and generalized-reactivity specifications in temporal synthesis |
| title_full | Finite-trace and generalized-reactivity specifications in temporal synthesis |
| title_fullStr | Finite-trace and generalized-reactivity specifications in temporal synthesis |
| title_full_unstemmed | Finite-trace and generalized-reactivity specifications in temporal synthesis |
| title_short | Finite-trace and generalized-reactivity specifications in temporal synthesis |
| title_sort | finite trace and generalized reactivity specifications in temporal synthesis |
| work_keys_str_mv | AT degiacomog finitetraceandgeneralizedreactivityspecificationsintemporalsynthesis AT distasioa finitetraceandgeneralizedreactivityspecificationsintemporalsynthesis AT tabajaralm finitetraceandgeneralizedreactivityspecificationsintemporalsynthesis AT vardimy finitetraceandgeneralizedreactivityspecificationsintemporalsynthesis AT zhus finitetraceandgeneralizedreactivityspecificationsintemporalsynthesis |