2021/02/22 by Giuseppe De Giacomo, De Giacomo, Giuseppe, Giuseppe Perelli +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies #cs.LO
paper · pdf · doi:10.48550/arxiv.2102.11184
arxiv created 2021/02/22 · openalex publication_date 2021/02/22 · arxiv updated 2021/02/23 · openalex created_date 2024/04/10 · openalex updated_date 2026/07/28
In this paper we introduce Behavioral QLTL, which is a ``behavioral'' variant of linear-time temporal logic on infinite traces 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''. This gives to the logic a strategic flavor that we usually associate to planning. Indeed we show that temporally extended planning in nondeterministic domains, as well as 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 conditional 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 with simpler forms of behavioral semantics.