Good-for-Game QPTL: An Alternating Hodges Semantics

TL;DR

This paper introduces a new extension of QPTL called Good-for-Game QPTL, which incorporates behavioral quantifications linked to game theory, enabling natural expression of game-theoretic concepts with decidability results.

Contribution

It defines behavioral quantifications within QPTL, connecting logic to game theory, and proves their decidability and expressive power equivalence to QPTL.

Findings

Behavioral quantifications can be decided in 2ExpTime.

They are expressively equivalent to QPTL.

The fragment is less succinct but more natural for game-theoretic modeling.

Abstract

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.