  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.
