Tropical linear-fractional programming and parametric mean payoff games

Tropical polyhedra have been recently used to represent disjunctive invariants in static analysis. To handle larger instances, tropical analogues of classical linear programming results need to be developed. This motivation leads us to study the tropical analogue of the classical linear-fractional programming problem. We construct an associated parametric mean payoff game problem, and show that the optimality of a given point, or the unboundedness of the problem, can be certified by exhibiting a strategy for one of the players having certain infinitesimal properties (involving the value of the game and its derivative) that we characterize combinatorially. We use this idea to design a Newton-like algorithm to solve tropical linear-fractional programming problems, by reduction to a sequence of auxiliary mean payoff game problems.     

Solving parity games by a reduction to SAT

This paper presents a reduction from the problem of solving parity games to the satisfiability problem in propositional logic (SAT). The reduction is done in two stages, first into difference logic, i.e. SAT combined with the theory of integer differences, an instance of the SAT modulo theories (SMT) framework. In the second stage the integer variables and constraints of the difference logic encoding are replaced with a set of Boolean variables and constraints on them, giving rise to a pure SAT encoding of the problem. The reduction uses Jurdziński?s characterisation of winning strategies via progress measures. The reduction is motivated by the success of SAT solvers in symbolic verification, bounded model checking in particular. The paper reports on prototype implementations of the reductions and presents some experimental results.     

A survey of partial-observation stochastic parity games

We consider two-player zero-sum stochastic games on graphs with ω-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode. On the basis of information, these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes (POMDPs), and the blind one-player games, known as probabilistic automata. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, Büchi, or coBüchi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability 1), limit-sure winning (i.e., winning with probability arbitrarily close to 1), and value-threshold winning (i.e., winning with probability at least ν, where ν is a given rational).     

A proof of the determinacy property of the data flow schema

Previous proofs of data flow determinacy proceeded indirectly and relied on results from abstract semantics. In this paper, a direct proof of the determinacy of data flow schema is given. This proof does not use high powered metamathematical theorems and consequently is accessible to all researchers in data flow, not just those intimately familiar with deep semantic results. Our proof proceeds in three stages. First, the data flow schema which contains instances of Link, Sink and Operator actors is proved to be determinate by reduction to the results of Karp and Miller (1966). Second, data flow schema containingSwitch actors, in addition to the above actors, are proved to be determinate. Finally, data flow schema which additionally contain Apply actors are proven to be determinate.     

On numerical solution of positional differential games with nonterminal payoff

We propose a numerical method for an approximate construction of the game value and optimal control laws in a linear-convex positional differential game with a quality index that evaluates the collection of deviations of the motion trajectory at given time moments from given targets. We show the algorithmic complexity of this method, details of software implementation, and results of numerical experiments.     

Reduction of stochastic parity to stochastic mean-payoff games

A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives, and mean-payoff (or limit-average) objectives. These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of stochastic parity games to stochastic mean-payoff games.     

Promoting cooperation by setting a ceiling payoff for defectors under three-strategy public good games

The puzzle of altruistic behaviours among multi-agent systems poses a dilemma, which has been an overlapping topic that covers many subjects. The public goods game can be regarded as a paradigm for modelling and exploring it. In the traditional definition of public goods game, the equally divided benefit among all participants leads to the dominance of defection. Much effort has been made to explain the evolution of cooperation, including the model in which the payoff ceilings for defectors are introduced. Further, we study a three-strategy evolutionary public goods game by providing the role of being loners. The payoff ceilings will take effect when the number of cooperators exceeds some threshold. Analysis results by following the replicator dynamics indicate that lower values of the payoff ceilings can better promote levels of public cooperation. Importantly, a remarkable cyclic route has been found: when receiving relative lower benefits, loners act as catalysts, helping the population to escape from mutual defection to cooperation. And, the stable equilibrium points from cooperation to isolation can be realised by improving the fixed payoffs of loners. Finally, broader ceilings also for cooperators provide us more hints about how to suppress the spreading of defectors under certain conditions.     

Entanglement of formation is non-monotonic with concurrence: a simple proof

In this paper we explore the non-monotonic nature of entanglement of formation with respect to concurrence for pure bipartite states. For pure bipartite system, one of the basic physical reason of this non-monotonicity character is due to the existence of incomparable states, i.e., the pure bipartite states which are not convertible to each other by LOCC with certainty.      

On the determinacy of concurrent games on event structures with infinite winning sets

We consider nondeterministic concurrent games played on event structures and study their determinacy problem—the existence of winning strategies. It is known that when the winning conditions of the games are characterised by a collection of finite winning sets/plays, a restriction (called race-freedom) on the boards where the games are played guarantees determinacy. However the games may no longer be determined when the winning sets are infinite. This paper provides a study of concurrent games and nondeterministic winning strategies by analysing conditions that ensure determinacy when infinitely many events are played, that is, when the winning sets are infinite. The main result is a determinacy theorem for a class of games with a bounded concurrency property and infinite winning sets shown to be finitely decidable.     

Characterization of simple edge-firing games

In a recent publication, Latapy and Magnien [Inform. Process. Lett. 83 (2002) 125-128] show how every distributive lattice can be represented as the set of configurations of a simple edge firing game (EFG). This is a converse of the result of Propp [Preprint, 1993] that shows that the set of configurations of an EFG forms a distributive lattice. Using this result and then the result of Latapy and Magnien gives an algorithm for converting an arbitrary EFG to a simple one with isomorphic state space.The purpose of this note is to provide a characterization of simple edge firing games. The characterization will emerge from a more general result which determines how often a particular vertex can be fired in such a game.     

A simple proof of Kharitonov's theorem

An alternative proof of Kharitonov's theorem on the stability of linear time-invariant continuous systems under parameter variations is presented.     

Practical synthesis of reactive systems from LTL specifications via parity games

Acta Informatica - The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption...     

A simple proof of the optimality of a threshold policy in a two-server queueing system

Lin and Kumar (1984) introduced a control model with a single queue and two heterogeneous servers. They showed, using policy iteration, that the slower server should only be used if the queue length is above a certain level, i.e., the optimal policy is of threshold type. In this note we give a simple iterative proof of this result.     

A new and simple proof of the equivalence theorem for behaviors

Two full row rank representations of the same behavior are related through a left unimodular transformation. We present a new and extremely simple and insightful proof for this well-established fact.     

A simple proof of the uniform consensus synchronous lower bound

We give a simple and intuitive proof of an f+2 round lower bound for uniform consensus. That is, we show that for every uniform consensus algorithm tolerating t failures, and for every f?t−2, there is an execution with f failures that requires f+2 rounds.     

A simple proof of Pach's extremal theorem for convex polygons

A simple proof is given that the minimum-area triangle inscribed in a convex polygon has two sides which are edges of the polygon.     

A simple proof of the Pontryagin maximum principle on manifolds

Applying the tubular neighborhood theorem, we give a simple proof of the Pontryagin maximum principle on a smooth manifold. The idea is as follows. Given a control system on a manifold M, we embed it into some Rⁿ and extend the control system to Rⁿ. Then, we apply the Pontryagin maximum principle on Rⁿ to the extended system and project the consequence to M.