Nondeterminism and Guarded Commands
The purpose of this paper is to discuss the relevance of nondeterminism in computer science, with a special emphasis on Dijkstra's guarded commands language.
cs.PL↗
arXiv subjects
Krzysztof R. Apt
Publications and source records attributed to Krzysztof R. Apt.
Iterated Elimination of Weakly Dominated Strategies in Well-Founded Games
Recently, in [K.R. Apt and S. Simon: Well-founded extensive games with perfect information, TARK21], we studied well-founded games, a natural extension of finite extensive games with perfect information in which all plays are finite. We extend here, to this class of games, two results concerned with iterated elimination of weakly dominated strategies, originally established for finite extensive games. The first one states that every finite extensive game with perfect information and injective payoff functions can be reduced by a specific iterated elimination of weakly dominated strategies to a trivial game containing the unique subgame perfect equilibrium. Our extension of this result to well-founded games admits transfinite iterated elimination of strategies. It applies to an infinite version of the centipede game. It also generalizes the original result to a class of finite games that may have several subgame perfect equilibria. The second one states that finite zero-sum games with 'n' outcomes can be solved by the maximal iterated elimination of weakly dominated strategies in 'n-1' steps. We generalize this result to a natural class of well-founded strictly competitive games.
cs.GT↗
Characterization of incentive compatible single-parameter mechanisms revisited
We reexamine the characterization of incentive compatible single-parameter mechanisms introduced in Archer & Tardos(2001). We argue that the claimed uniqueness result, called `Myerson's Lemma' was not well established. We provide an elementary proof of uniqueness that unifies the presentation for two classes of allocation functions used in the literature and show that the general case is a consequence of a little known result from the theory of real functions. We also clarify that our proof of uniqueness is more elementary than the previous one. Finally, by generalizing our characterization result to more dimensions, we provide alternative proofs of revenue equivalence results for multiunit auctions and combinatorial auctions.
cs.GT↗
A tutorial for computer scientists on finite extensive games with perfect information
We provide a self-contained introduction to finite extensive games with perfect information. In these games players proceed in turns having, at each stage, finitely many moves to their disposal, each play always ends, and in each play the players have complete knowledge of the previously made moves. Almost all discussed results are well-known, but often they are not presented in an optimal form. Also, they usually appear in the literature aimed at economists or mathematicians, so the algorithmic or logical aspects are underrepresented.
cs.GT↗
Well-Founded Extensive Games with Perfect Information
We consider extensive games with perfect information with well-founded game trees and study the problems of existence and of characterization of the sets of subgame perfect equilibria in these games. We also provide such characterizations for two classes of these games in which subgame perfect equilibria exist: two-player zero-sum games with, respectively, two and three outcomes.
cs.GT↗
Edsger W. Dijkstra: a Commemoration
This article is a multiauthored portrait of Edsger Wybe Dijkstra that consists of testimonials written by several friends, colleagues, and students of his. It provides unique insights into his personality, working style and habits, and his influence on other computer scientists, as a researcher, teacher, and mentor.
cs.GL↗
Coordination Games on Weighted Directed Graphs
We study strategic games on weighted directed graphs, in which the payoff of a player is defined as the sum of the weights on the edges from players who chose the same strategy, augmented by a fixed non-negative integer bonus for picking a given strategy. These games capture the idea of coordination in the absence of globally common strategies. We identify natural classes of graphs for which finite improvement or coalition-improvement paths of polynomial length always exist, and, as a consequence, a (pure) Nash equlibrium or a strong equilibrium can be found in polynomial time. The considered classes of graphs are typical in network topologies: simple cycles correspond to the token ring local area networks, while open chains of simple cycles correspond to multiple independent rings topology from the recommendation G.8032v2 on the Ethernet ring protection switching. For simple cycles these results are optimal in the sense that without the imposed conditions on the weights and bonuses a Nash equilibrium may not even exist. Finally, we prove that the problem of determining the existence of a Nash equilibrium or of a strong equilibrium in these games is NP-complete already for unweighted graphs and with no bonuses assumed. This implies that the same problems for polymatrix games are strongly NP-hard.
cs.GT↗
Edsger Dijkstra. The Man Who Carried Computer Science on His Shoulders
This a biographical essay about Edsger Wybe Dijkstra.
cs.GL↗
Reasoning about call-by-value: a missing result in the history of Hoare's logic
We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no such proof system has been proposed in the literature.
cs.LO↗
Open Problems in a Logic of Gossips
Gossip protocols are programs used in a setting in which each agent holds a secret and the aim is to reach a situation in which all agents know all secrets. Such protocols rely on a point-to-point or group communication. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. The advantage of the use of epistemic logic is that the resulting protocols are very concise and amenable for a simple verification. Recently, we introduced a natural modal logic that allows one to express distributed epistemic gossip protocols and to reason about their correctness. We proved that the resulting protocols are implementable and that all aspects of their correctness, including termination, are decidable. To establish these results we showed that both the definition of semantics and of truth of the underlying logic are decidable. We also showed that the analogous results hold for an extension of this logic with the 'common knowledge' operator. However, several, often deceptively simple, questions about this logic and the corresponding gossip protocols remain open. The purpose of this paper is to list and elucidate these questions and provide for them an appropriate background information in the form of partial of related results.
cs.AI↗
Self-Stabilization Through the Lens of Game Theory
In 1974 E.W. Dijkstra introduced the seminal concept of self-stabilization that turned out to be one of the main approaches to fault-tolerant computing. We show here how his three solutions can be formalized and reasoned about using the concepts of game theory. We also determine the precise number of steps needed to reach self-stabilization in his first solution.
cs.GT↗
When Are Two Gossips the Same? Types of Communication in Epistemic Gossip Protocols
We provide an in-depth study of the knowledge-theoretic aspects of communication in so-called gossip protocols. Pairs of agents communicate by means of calls in order to spread information---so-called secrets---within the group. Depending on the nature of such calls knowledge spreads in different ways within the group. Systematizing existing literature, we identify 18 different types of communication, and model their epistemic effects through corresponding indistinguishability relations. We then provide a classification of these relations and show its usefulness for an epistemic analysis in presence of different communication types. Finally, we explain how to formalise the assumption that the agents have common knowledge of a distributed epistemic gossip protocol.
cs.MA↗
Common Knowledge in a Logic of Gossips
Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other secrets. Recently a number of authors studied distributed epistemic gossip protocols. These protocols use as guards formulas from a simple epistemic logic, which makes their analysis and verification substantially easier. We study here common knowledge in the context of such a logic. First, we analyze when it can be reduced to iterated knowledge. Then we show that the semantics and truth for formulas without nested common knowledge operator are decidable. This implies that implementability, partial correctness and termination of distributed epistemic gossip protocols that use non-nested common knowledge operator is decidable, as well. Given that common knowledge is equivalent to an infinite conjunction of nested knowledge, these results are non-trivial generalizations of the corresponding decidability results for the original epistemic logic, established in (Apt & Wojtczak, 2016). K. R. Apt & D. Wojtczak (2016): On Decidability of a Logic of Gossips. In Proc. of JELIA 2016, pp. 18-33, doi:10.1007/ 978-3-319-48758-8_2.
cs.LO↗
Coordination Games on Graphs
We introduce natural strategic games on graphs, which capture the idea of coordination in a local setting. We study the existence of equilibria that are resilient to coalitional deviations of unbounded and bounded size (i.e., strong equilibria and k-equilibria respectively). We show that pure Nash equilibria and 2-equilibria exist, and give an example in which no 3-equilibrium exists. Moreover, we prove that strong equilibria exist for various special cases. We also study the price of anarchy (PoA) and price of stability (PoS) for these solution concepts. We show that the PoS for strong equilibria is 1 in almost all of the special cases for which we have proven strong equilibria to exist. The PoA for pure Nash equilbria turns out to be unbounded, even when we fix the graph on which the coordination game is to be played. For the PoA for k-equilibria, we show that the price of anarchy is between 2(n-1)/(k-1) - 1 and 2(n-1)/(k-1). The latter upper bound is tight for $k=n$ (i.e., strong equilibria). Finally, we consider the problems of computing strong equilibria and of determining whether a joint strategy is a k-equilibrium or strong equilibrium. We prove that, given a coordination game, a joint strategy s, and a number k as input, it is co-NP complete to determine whether s is a k-equilibrium. On the positive side, we give polynomial time algorithms to compute strong equilibria for various special cases.
cs.GT↗
Epistemic Protocols for Distributed Gossiping
Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other's secrets. We consider distributed gossip protocols which are expressed by means of epistemic logic. We provide an operational semantics of such protocols and set up an appropriate framework to argue about their correctness. Then we analyze specific protocols for complete graphs and for directed rings.
cs.AI↗
Coordination Games on Directed Graphs
We study natural strategic games on directed graphs, which capture the idea of coordination in the absence of globally common strategies. We show that these games do not need to have a pure Nash equilibrium and that the problem of determining their existence is NP-complete. The same holds for strong equilibria. We also exhibit some classes of games for which strong equilibria exist and prove that a strong equilibrium can then be found in linear time.
cs.GT↗
A Classification of Weakly Acyclic Games
Weakly acyclic games form a natural generalization of the class of games that have the finite improvement property (FIP). In such games one stipulates that from any initial joint strategy some finite improvement path exists. We classify weakly acyclic games using the concept of a scheduler introduced in arXiv:1202.2209. We also show that finite games that can be solved by the iterated elimination of never best response strategies are weakly acyclic. Finally, we explain how the schedulers allow us to improve the bounds on finding a Nash equilibrium in a weakly acyclic game.
cs.GT↗