arXiv subjects

Sven Schewe

Publications and source records attributed to Sven Schewe.

At least 73 records · Page 4Linked to original sources

arXiv2016

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that - in contrast to existing techniques - tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states.

cs.LO↗

arXiv2016

Fast Two-Robot Disk Evacuation with Wireless Communication

In the fast evacuation problem, we study the path planning problem for two robots who want to minimize the worst-case evacuation time on the unit disk. The robots are initially placed at the center of the disk. In order to evacuate, they need to reach an unknown point, the exit, on the boundary of the disk. Once one of the robots finds the exit, it will instantaneously notify the other agent, who will make a beeline to it. The problem has been studied for robots with the same speed~\cite{s1}. We study a more general case where one robot has speed $1$ and the other has speed $s \geq 1$. We provide optimal evacuation strategies in the case that $s \geq c_{2.75} \approx 2.75$ by showing matching upper and lower bounds on the worst-case evacuation time. For $1\leq s < c_{2.75}$, we show (non-matching) upper and lower bounds on the evacuation time with a ratio less than $1.22$. Moreover, we demonstrate that a generalization of the two-robot search strategy from~\cite{s1} is outperformed by our proposed strategies for any $s \geq c_{1.71} \approx 1.71$.

cs.DC↗

arXiv2015

Incentive Stackelberg Mean-payoff Games

We introduce and study incentive equilibria for multi-player meanpayoff games. Incentive equilibria generalise well-studied solution concepts such as Nash equilibria and leader equilibria (also known as Stackelberg equilibria). Recall that a strategy profile is a Nash equilibrium if no player can improve his payoff by changing his strategy unilaterally. In the setting of incentive and leader equilibria, there is a distinguished player called the leader who can assign strategies to all other players, referred to as her followers. A strategy profile is a leader strategy profile if no player, except for the leader, can improve his payoff by changing his strategy unilaterally, and a leader equilibrium is a leader strategy profile with a maximal return for the leader. In the proposed case of incentive equilibria, the leader can additionally influence the behaviour of her followers by transferring parts of her payoff to her followers. The ability to incentivise her followers provides the leader with more freedom in selecting strategy profiles, and we show that this can indeed improve the payoff for the leader in such games. The key fundamental result of the paper is the existence of incentive equilibria in mean-payoff games. We further show that the decision problem related to constructing incentive equilibria is NP-complete. On a positive note, we show that, when the number of players is fixed, the complexity of the problem falls in the same class as two-player mean-payoff games. We also present an implementation of the proposed algorithms, and discuss experimental results that demonstrate the feasibility of the analysis of medium sized games.

cs.GT↗

arXiv2015

Making the Best of Limited Memory in Multi-Player Discounted Sum Games

In this paper, we establish the existence of optimal bounded memory strategy profiles in multi-player discounted sum games. We introduce a non-deterministic approach to compute optimal strategy profiles with bounded memory. Our approach can be used to obtain optimal rewards in a setting where a powerful player selects the strategies of all players for Nash and leader equilibria, where in leader equilibria the Nash condition is waived for the strategy of this powerful player. The resulting strategy profiles are optimal for this player among all strategy profiles that respect the given memory bound, and the related decision problem is NP-complete. We also provide simple examples, which show that having more memory will improve the optimal strategy profile, and that sufficient memory to obtain optimal strategy profiles cannot be inferred from the structure of the game.

cs.GT↗

arXiv2015

Lazy Probabilistic Model Checking without Determinisation

The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach---both explicit and symbolic versions---in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.

cs.LO↗

arXiv2015

Symmetric Strategy Improvement

Symmetry is inherent in the definition of most of the two-player zero-sum games, including parity, mean-payoff, and discounted-payoff games. It is therefore quite surprising that no symmetric analysis techniques for these games exist. We develop a novel symmetric strategy improvement algorithm where, in each iteration, the strategies of both players are improved simultaneously. We show that symmetric strategy improvement defies Friedmann's traps, which shook the belief in the potential of classic strategy improvement to be polynomial.

cs.GT↗

arXiv2014

Bounded-Rate Multi-Mode Systems Based Motion Planning

Bounded-rate multi-mode systems are hybrid systems that can switch among a finite set of modes. Its dynamics is specified by a finite number of real-valued variables with mode-dependent rates that can vary within given bounded sets. Given an arbitrary piecewise linear trajectory, we study the problem of following the trajectory with arbitrary precision, using motion primitives given as bounded-rate multi-mode systems. We give an algorithm to solve the problem and show that the problem is co-NP complete. We further prove that the problem can be solved in polynomial time for multi-mode systems with fixed dimension. We study the problem with dwell-time requirement and show the decidability of the problem under certain positivity restriction on the rate vectors. Finally, we show that introducing structure to the multi-mode systems leads to undecidability, even when using only a single clock variable.

cs.LO↗

arXiv2014

Tight Bounds for Complementing Parity Automata

We follow a connection between tight determinisation and complementation and establish a complementation procedure from parity automata to nondeterministic Büchi automata and prove it to be tight up to an $O(n)$ factor, where $n$ is the size of the nondeterministic parity automaton. This factor does not depend on the number of priorities.

cs.FL↗

arXiv2014

Determinising Parity Automata

Parity word automata and their determinisation play an important role in automata and game theory. We discuss a determinisation procedure for nondeterministic parity automata through deterministic Rabin to deterministic parity automata. We prove that the intermediate determinisation to Rabin automata is optimal. We show that the resulting determinisation to parity automata is optimal up to a small constant. Moreover, the lower bound refers to the more liberal Streett acceptance. We thus show that determinisation to Streett would not lead to better bounds than determinisation to parity. As a side-result, this optimality extends to the determinisation of Büchi automata.

cs.FL↗

arXiv2013

Coverage Games for Testing Nondeterministic Systems

Modern software systems may exhibit a nondeterministic behavior due to many unpredictable factors. In this work, we propose the node coverage game, a two player turn-based game played on a finite game graph, as a formalization of the problem to test such systems. Each node in the graph represents a {\em functional equivalence class} of the software under test (SUT). One player, the tester, wants to maximize the node coverage, measured by the number of nodes visited when exploring the game graphs, while his opponent, the SUT, wants to minimize it. An optimal test would maximize the cover, and it is an interesting problem to find the maximal number of nodes that the tester can guarantee to visit, irrespective of the responses of the SUT. We show that the decision problem of whether the guarantee is less than a given number is NP-complete. Then we present techniques for testing nondeterministic SUTs with existing test suites for deterministic models. Finally, we report our implementation and experiments.

cs.SE↗

arXiv2013

The benefit of law-making power

We study optimal equilibria in multi-player games. An equilibrium is optimal for a player, if her payoff is maximal. A tempting approach to solving this problem is to seek optimal Nash equilibria, the standard form of equilibria where no player has an incentive to deviate from her strategy. We argue that a player with the power to define an equilibrium is in a position, where she should not be interested in the symmetry of a Nash equilibrium, and ignore the question of whether or not her outcome can be improved if the other strategies are fixed. That is, she would only have to make sure that the other players have no incentive to deviate. This defines a greater class of equilibria, which may have better (and cannot have worse) optimal equilibria for the designated powerful player. We apply this strategy to concurrent bimatrix games and to turn based multi-player mean-payoff games. For the latter, we show that such political equilibria as well as Nash equilibria always exist, and provide simple examples where the political equilibrium is superior. We show that constructing political and Nash equilibria are NP-complete problems. We also show that, for a fixed number of players, the hardest part is to solve the underlying two-player mean-payoff games: using an MPG oracle, the problem is solvable in polynomial time. It is therefore in UP and CoUP, and can be solved in pseudo polynomial and expected subexponential time.

cs.GT↗

arXiv2013

Time and Parallelizability Results for Parity Games with Bounded Tree and DAG Width

Parity games are a much researched class of games in NP intersect CoNP that are not known to be in P. Consequently, researchers have considered specialised algorithms for the case where certain graph parameters are small. In this paper, we study parity games on graphs with bounded treewidth, and graphs with bounded DAG width. We show that parity games with bounded DAG width can be solved in O(n^(k+3) k^(k + 2) (d + 1)^(3k + 2)) time, where n, k, and d are the size, treewidth, and number of priorities in the parity game. This is an improvement over the previous best algorithm, given by Berwanger et al., which runs in n^O(k^2) time. We also show that, if a tree decomposition is provided, then parity games with bounded treewidth can be solved in O(n k^(k + 5) (d + 1)^(3k + 5)) time. This improves over previous best algorithm, given by Obdrzalek, which runs in O(n d^(2(k+1)^2)) time. Our techniques can also be adapted to show that the problem of solving parity games with bounded treewidth lies in the complexity class NC^2, which is the class of problems that can be efficiently parallelized. This is in stark contrast to the general parity game problem, which is known to be P-hard, and thus unlikely to be contained in NC.

cs.GT↗

arXiv2012

Multiplayer Cost Games with Simple Nash Equilibria

Multiplayer games with selfish agents naturally occur in the design of distributed and embedded systems. As the goals of selfish agents are usually neither equivalent nor antagonistic to each other, such games are non zero-sum games. We study such games and show that a large class of these games, including games where the individual objectives are mean- or discounted-payoff, or quantitative reachability, and show that they do not only have a solution, but a simple solution. We establish the existence of Nash equilibria that are composed of k memoryless strategies for each agent in a setting with k agents, one main and k-1 minor strategies. The main strategy describes what happens when all agents comply, whereas the minor strategies ensure that all other agents immediately start to co-operate against the agent who first deviates from the plan. This simplicity is important, as rational agents are an idealisation. Realistically, agents have to decide on their moves with very limited resources, and complicated strategies that require exponential--or even non-elementary--implementations cannot realistically be implemented. The existence of simple strategies that we prove in this paper therefore holds a promise of implementability.

cs.GT↗

arXiv2012

Rapid Recovery for Systems with Scarce Faults

Our goal is to achieve a high degree of fault tolerance through the control of a safety critical systems. This reduces to solving a game between a malicious environment that injects failures and a controller who tries to establish a correct behavior. We suggest a new control objective for such systems that offers a better balance between complexity and precision: we seek systems that are k-resilient. In order to be k-resilient, a system needs to be able to rapidly recover from a small number, up to k, of local faults infinitely many times, provided that blocks of up to k faults are separated by short recovery periods in which no fault occurs. k-resilience is a simple but powerful abstraction from the precise distribution of local faults, but much more refined than the traditional objective to maximize the number of local faults. We argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We show that the computational complexity of constructing optimal control with respect to resilience is low and demonstrate the feasibility through an implementation and experimental results.

eess.SY↗

arXiv2012

Proceedings First Workshop on Synthesis

This volume contains the proceedings of the First Workshop on Synthesis (SYNT 2012). The workshop is held is held in Berkeley, California, on June 6th and 7th, as a satellite event to the 24th International Conference on Computer Aided Verification (CAV 2012). SYNT aims at bringing together and providing an open platform for researchers interested in synthesis.

cs.LO↗

arXiv2012

Synthesis of Succinct Systems

Synthesis of correct by design systems from specification has recently attracted much attention. The theoretical results imply that this problem is highly intractable, e.g., synthesizing a system is 2EXPTIME-complete for an LTL specification, and EXPTIME-complete for a CTL specification. However, an argument against it is that the temporal specification is highly compact, and the complexity reflects the large size of the system constructed. In that respect, the complexity should, perhaps, be specified relative to the size of the minimal satisfying system. A careful observation reveals that the size of the system is presented in such arguments as the size of its state space. This view is a bit nonstandard, in the sense that the state space can be exponentially larger than the size of a reasonable implementation such as a circuit or a program. Although this alternative measure of the size of the synthesized system is more intuitive (e.g., this is the standard way model checking problems are measured), research on synthesis has so far stayed with measuring the system in terms of the explicit state space. This raises the question of whether or not there always exists a small system. In this paper, we show that this is the case if, and only if, PSPACE = EXPTIME.

cs.FL↗

arXiv2012

Bounded Satisfiability for PCTL

While model checking PCTL for Markov chains is decidable in polynomial-time, the decidability of PCTL satisfiability, as well as its finite model property, are long standing open problems. While general satisfiability is an intriguing challenge from a purely theoretical point of view, we argue that general solutions would not be of interest to practitioners: such solutions could be too big to be implementable or even infinite. Inspired by bounded synthesis techniques, we turn to the more applied problem of seeking models of a bounded size: we restrict our search to implementable -- and therefore reasonably simple -- models. We propose a procedure to decide whether or not a given PCTL formula has an implementable model by reducing it to an SMT problem. We have implemented our techniques and found that they can be applied to the practical problem of sanity checking -- a procedure that allows a system designer to check whether their formula has an unexpectedly small model.

cs.LO↗

arXiv2011

Practical Distributed Control Synthesis

Classic distributed control problems have an interesting dichotomy: they are either trivial or undecidable. If we allow the controllers to fully synchronize, then synthesis is trivial. In this case, controllers can effectively act as a single controller with complete information, resulting in a trivial control problem. But when we eliminate communication and restrict the supervisors to locally available information, the problem becomes undecidable. In this paper we argue in favor of a middle way. Communication is, in most applications, expensive, and should hence be minimized. We therefore study a solution that tries to communicate only scarcely and, while allowing communication in order to make joint decision, favors local decisions over joint decisions that require communication.

cs.LO↗