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 words, such functions must be “processes” (Abadi et al., Realizable and Unrealizable Specifications of Reactive Systems, 1989). 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. As such 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.