Behavioral QLTL
This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic (LTL) with second-order quantifiers. Behavioral QLTL is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2023
|
| _version_ | 1811141173703606272 |
|---|---|
| author | De Giacomo, G Perelli, G |
| author_facet | De Giacomo, G Perelli, G |
| author_sort | De Giacomo, G |
| collection | OXFORD |
| description | This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic (LTL) with second-order quantifiers. Behavioral QLTL is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes” [1]. This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and LTL synthesis are expressed in Behavioral QLTL through formulas with a simple quantification alternation. While as this alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original QLTL (with non-behavioral semantics) and simpler forms of behavioral semantics. |
| first_indexed | 2024-04-23T08:25:56Z |
| format | Conference item |
| id | oxford-uuid:89364c96-ba59-44de-89eb-a41e69e44963 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:33:40Z |
| publishDate | 2023 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:89364c96-ba59-44de-89eb-a41e69e449632024-09-09T09:47:58ZBehavioral QLTLConference itemhttp://purl.org/coar/resource_type/c_5794uuid:89364c96-ba59-44de-89eb-a41e69e44963EnglishSymplectic ElementsSpringer2023De Giacomo, GPerelli, GThis paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic (LTL) with second-order quantifiers. Behavioral QLTL is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes” [1]. This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and LTL synthesis are expressed in Behavioral QLTL through formulas with a simple quantification alternation. While as this alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original QLTL (with non-behavioral semantics) and simpler forms of behavioral semantics. |
| spellingShingle | De Giacomo, G Perelli, G Behavioral QLTL |
| title | Behavioral QLTL |
| title_full | Behavioral QLTL |
| title_fullStr | Behavioral QLTL |
| title_full_unstemmed | Behavioral QLTL |
| title_short | Behavioral QLTL |
| title_sort | behavioral qltl |
| work_keys_str_mv | AT degiacomog behavioralqltl AT perellig behavioralqltl |