Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language.The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games.However, the IF semantics exhibits some limitations, at least from a purely logical perspective.It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp., falsity, of a sentence.In addition, truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game.As a consequence, IF does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle.These idiosyncrasies limit its expressive power to the existential fragment of Second Order Logic (Sol).In this paper, we investigate an extension of IF, called Alternating Dependence/Independence Friendly Logic (ADIF), tailored to overcome these limitations.To this end, we introduce a novel compositional semantics, generalising the one based on trumps proposed by Hodges for IF.The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants ADIF the full descriptive power of Sol.We also provide an equivalent Herbrand-Skolem semantics and a gametheoretic semantics for the prenex fragment of ADIF, the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures.

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. Inspired by the work on logics of dependence and independence, we provide a new compositional semantics for QPTL that allows for expressing such functional dependencies among variables. The fragment where only restricted quantifications are considered, called behavioral quantifications , allows for linear-time properties that are satisfiable if and only if they are realisable in the Pnueli-Rosner sense. This fragment can be decided, for both model checking and satisfiability , in 2 Exp Time and is expressively equivalent to QPTL , though significantly less succinct.

In multi-player games, players take their decisions on the basis of their knowledge about what other players have done, or currently do, or even, in some cases, will do. An ability to reason in games with temporal dependencies between players' decisions is a challenging topic, in particular because it involves imperfect information. In this work, we propose a theoretical framework based on dependency matrices that includes many instances of strategic dependencies in multi-player imperfect information games. For our framework to be well-defined, we get inspiration from quantified linear-time logic where each player has to label the timeline with truth values of the propositional variable she owns. We study the problem of the existence of a winning strategy for a coalition of players, show it is undecidable in general, and exhibit an interesting subclass of dependency matrices that makes the problem decidable: the class of perfect-information dependency matrices.