Obligation Blackwell games and p-automata

DOI10.1017/JSL.2016.71MaRDI QIDQ4977213zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Nir Piterman

Publication date 3 August 2017

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.5174

zbMATH Keywords

automatatwo-player games

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45) 2-person games (91A05) Stochastic games, stochastic differential games (91A15) Algorithmic game theory and complexity (91A68)

Abstract: We recently introduced p-automata, automata that read discrete-time Markov chains. We used turn-based stochastic parity games to define acceptance of Markov chains by a subclass of p-automata. Definition of acceptance required a cumbersome and complicated reduction to a series of turn-based stochastic parity games. The reduction could not support acceptance by general p-automata, which was left undefined as there was no notion of games that supported it. Here we generalize two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1. One cannot define value in obligation games by the standard mechanism of considering the measure of winning paths on a Markov chain and taking the supremum of the infimum of all strategies. Mainly because obligations need definition even for Markov chains and the nature of obligations has the flavor of an infinite nesting of supremum and infimum operators. We define value via a reduction to turn-based games similar to Martin's proof of determinacy of Blackwell games with Borel objectives. Based on this definition, we show that games are determined. We show that for Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations there exists an alternative and simpler characterization of the value function. Based on this simpler definition we give an exponential time algorithm to analyze finite turn-based stochastic parity games with obligations. Finally, we show that obligation games provide the necessary framework for reasoning about p-automata and that they generalize the previous definition.

Recommendations

• Obliging games
• A survey of partial-observation stochastic parity games
• The complexity of partial-observation parity games
• Quantitative solution of -regular games
• Stochastic Müller Games are PSPACE-Complete

Cites work

• A logic for reasoning about time and reliability
• An automata-theoretic approach to branching-time model checking
• Automata, logics, and infinite games. A guide to current research
• Bisimulation through probabilistic testing
• Borel determinacy
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Fair simulation
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• scientific article; zbMATH DE number 7357543 (Why is no real title available?)
• On the equivalence of game and denotational semantics for the probabilistic -calculus
• Probabilistic modal \(\mu\)-calculus with independent product
• Probabilistic propositional temporal logics
• Real analysis
• The complexity of probabilistic verification
• The determinacy of Blackwell games
• Tractable probabilistic -calculus that expresses probabilistic temporal logics

Cited in

(1)

• Obliging games

Describes a project that uses

Uses Software

• LiQuor
• PRISM

This page was built for publication: Obligation Blackwell games and p-automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4977213)