Behavioral QLTL

TL;DR

Behavioral QLTL is a new variant of linear-time temporal logic that models strategies based on past-dependent functions, enabling expressive planning and synthesis in nondeterministic domains.

Contribution

It introduces a behavioral variant of QLTL where quantifier functions depend only on past, connecting logic to strategic planning and synthesis.

Findings

Expresses temporally extended planning and LTL synthesis with simple quantification.

Analyzes computational complexity and compares to original QLTL.

Shows how increased quantifier alternation mixes planning types.

Abstract

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.