DQPTL: Dependency Quantified Propositional Linear-time Temporal Logic

We present an approach to specify the information flow between players in a concurrent game with LTL objectives. We use a dependency matrix D to reflect this information flow. On this basis, we define the so-called Dependency Quantified Propositional Linear-time Temporal Logic (DQPTL) whose for® where D is a dependency matrix, mulae are of the form D∃𝑝𝜑, ∃𝑝® informs which players form the coalition and 𝜑 is an LTL formula, whose semantics is a concurrent game. We show that our setting captures the standard semantics of Quantified Propositional Linear-time Temporal Logic (QPTL), for some adequate matrices D. Moreover, we provide an effective criterion to decide if a DQPTL formula is consistent in the sense that the concurrent game yields an entire labeling of the time line, so that the winning condition 𝜑 can be evaluated.

Authors

• Dylan Bellier
• Sophie Pinchinat
• François Schwarzentruber

Keywords

• Temporal logic
• Dependency
• Multiplayer Games