-
Winning Cores in Parity Games
Authors:
Steen Vester
Abstract:
We introduce the novel notion of winning cores in parity games and develop a deterministic polynomial-time under-approximation algorithm for solving parity games based on winning core approximation. Underlying this algorithm are a number properties about winning cores which are interesting in their own right. In particular, we show that the winning core and the winning region for a player in a par…
▽ More
We introduce the novel notion of winning cores in parity games and develop a deterministic polynomial-time under-approximation algorithm for solving parity games based on winning core approximation. Underlying this algorithm are a number properties about winning cores which are interesting in their own right. In particular, we show that the winning core and the winning region for a player in a parity game are equivalently empty. Moreover, the winning core contains all fatal attractors but is not necessarily a dominion itself. Experimental results are very positive both with respect to quality of approximation and running time. It outperforms existing state-of-the-art algorithms significantly on most benchmarks.
△ Less
Submitted 5 February, 2016;
originally announced February 2016.
-
Distributed Synthesis in Continuous Time
Authors:
Holger Hermanns,
Jan Krčál,
Steen Vester
Abstract:
We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesising local strategies for individual agents such that a specified set of goal states is reached, or reached with at least a given probability. The flow of time is modelled explicitly based on continuous-time randomness, with two natural implicat…
▽ More
We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesising local strategies for individual agents such that a specified set of goal states is reached, or reached with at least a given probability. The flow of time is modelled explicitly based on continuous-time randomness, with two natural implications: First, the non-determinism stemming from interleaving disappears. Second, when we restrict to a subclass of non-urgent models, the quantitative value problem for two players can be solved in EXPTIME. Indeed, the explicit continuous time enables players to communicate their states by delaying synchronisation (which is unrestricted for non-urgent models). In general, the problems are undecidable already for two players in the quantitative case and three players in the qualitative case. The qualitative undecidability is shown by a reduction to decentralized POMDPs for which we provide the strongest (and rather surprising) undecidability result so far.
△ Less
Submitted 7 January, 2016;
originally announced January 2016.
-
Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
Authors:
Steen Vester
Abstract:
We consider quantitative extensions of the alternating-time temporal logics ATL/ATLs called quantitative alternating-time temporal logics (QATL/QATLs) in which the value of a counter can be compared to constants using equality, inequality and modulo constraints. We interpret these logics in one-counter game models which are infinite duration games played on finite control graphs where each transit…
▽ More
We consider quantitative extensions of the alternating-time temporal logics ATL/ATLs called quantitative alternating-time temporal logics (QATL/QATLs) in which the value of a counter can be compared to constants using equality, inequality and modulo constraints. We interpret these logics in one-counter game models which are infinite duration games played on finite control graphs where each transition can increase or decrease the value of an unbounded counter. That is, the state-space of these games are, generally, infinite. We consider the model-checking problem of the logics QATL and QATLs on one-counter game models with VASS semantics for which we develop algorithms and provide matching lower bounds. Our algorithms are based on reductions of the model-checking problems to model-checking games. This approach makes it quite simple for us to deal with extensions of the logical languages as well as the infinite state spaces. The framework generalizes on one hand qualitative problems such as ATL/ATLs model-checking of finite-state systems, model-checking of the branching-time temporal logics CTL and CTLs on one-counter processes and the realizability problem of LTL specifications. On the other hand the model-checking problem for QATL/QATLs generalizes quantitative problems such as the fixed-initial credit problem for energy games (in the case of QATL) and energy parity games (in the case of QATLs). Our results are positive as we show that the generalizations are not too costly with respect to complexity. As a byproduct we obtain new results on the complexity of model-checking CTLs in one-counter processes and show that deciding the winner in one-counter games with LTL objectives is 2ExpSpace-complete.
△ Less
Submitted 19 September, 2014;
originally announced September 2014.
-
Nash Equilibria in Symmetric Games with Partial Observation
Authors:
Patricia Bouyer,
Nicolas Markey,
Steen Vester
Abstract:
We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidab…
▽ More
We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.
△ Less
Submitted 3 April, 2014;
originally announced April 2014.
-
Alternating-time temporal logic with finite-memory strategies
Authors:
Steen Vester
Abstract:
Model-checking the alternating-time temporal logics ATL and ATL* with incomplete information is undecidable for perfect recall semantics. However, when restricting to memoryless strategies the model-checking problem becomes decidable. In this paper we consider two other types of semantics based on finite-memory strategies. One where the memory size allowed is bounded and one where the memory size…
▽ More
Model-checking the alternating-time temporal logics ATL and ATL* with incomplete information is undecidable for perfect recall semantics. However, when restricting to memoryless strategies the model-checking problem becomes decidable. In this paper we consider two other types of semantics based on finite-memory strategies. One where the memory size allowed is bounded and one where the memory size is unbounded (but must be finite). This is motivated by the high complexity of model-checking with perfect recall semantics and the severe limitations of memoryless strategies. We show that both types of semantics introduced are different from perfect recall and memoryless semantics and next focus on the decidability and complexity of model-checking in both complete and incomplete information games for ATL/ATL*. In particular, we show that the complexity of model-checking with bounded-memory semantics is Delta_2p-complete for ATL and PSPACE-complete for ATL* in incomplete information games just as in the memoryless case. We also present a proof that ATL and ATL* model-checking is undecidable for n >= 3 players with finite-memory semantics in incomplete information games.
△ Less
Submitted 16 July, 2013;
originally announced July 2013.
-
Multi-Agent Programming Contest 2012 - The Python-DTU Team
Authors:
Jørgen Villadsen,
Andreas Schmidt Jensen,
Mikko Berggren Ettienne,
Steen Vester,
Kenneth Balsiger Andersen,
Andreas Frøsig
Abstract:
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
△ Less
Submitted 1 October, 2012;
originally announced October 2012.
-
Multi-Agent Programming Contest 2011 - The Python-DTU Team
Authors:
Jørgen Villadsen,
Mikko Berggren Ettienne,
Steen Vester
Abstract:
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
△ Less
Submitted 1 October, 2011;
originally announced October 2011.
-
Multi-Agent Programming Contest 2010 - The Jason-DTU Team
Authors:
Jørgen Villadsen,
Niklas Skamriis Boss,
Andreas Schmidt Jensen,
Steen Vester
Abstract:
We provide a brief description of the Jason-DTU system, including the methodology, the tools and the team strategy that we plan to use in the agent contest.
We provide a brief description of the Jason-DTU system, including the methodology, the tools and the team strategy that we plan to use in the agent contest.
△ Less
Submitted 1 October, 2010;
originally announced October 2010.
