  An extension of QPTL is considered where functional dependencies among the
quantified variables can be restricted in such a way that their current values
are independent of the future values of the other variables. This restriction
is tightly connected to the notion of behavioral strategies in game-theory and
allows the resulting logic to naturally express game-theoretic concepts. The
fragment where only restricted quantifications are considered, called
behavioral quantifications, can be decided, for both model checking and
satisfiability, in 2ExpTime and is expressively equivalent to QPTL, though
significantly less succinct.
