相关论文: A Game Semantics of Concurrent Separation Logic

Two-player win/lose games of infinite duration are involved in several disciplines including computer science and logic. If such a game has deterministic winning strategies, one may ask how simple such strategies can get. The answer may…

Separation logic and its variants can describe various properties on pointer programs. However, when it comes to properties on sequences, one may find it hard to formalize. To deal with properties on variable-length sequences and multilevel…

Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program logics can express specifications about the full distributions…

Probabilistic concurrent/distributed strategies have so far not been investigated thoroughly in the context of imperfect information, where the Player has only partial knowledge of the moves made by the Opponent. In a situation where the…

Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to…

We present a framework that takes a concurrent program composed of unsynchronized processes, along with a temporal specification of their global concurrent behaviour, and automatically generates a concurrent program with synchronization…

We introduce the concept of budget games. Players choose a set of tasks and each task has a certain demand on every resource in the game. Each resource has a budget. If the budget is not enough to satisfy the sum of all demands, it has to…

We study two-player zero-sum concurrent stochastic games with finite state and action space played for an infinite number of steps. In every step, the two players simultaneously and independently choose an action. Given the current state…

Execution of concurrent programs implies frequent switching between different thread contexts. This property perplexes analyzing and reasoning about concurrent programs. Trace simplification is a technique that aims at alleviating this…

We use a reformulation of compositional game theory to reunite game theory with game semantics, by viewing an open game as the System and its choice of contexts as the Environment. Specifically, the system is jointly controlled by $n \geq…

In a distributed game we imagine a team Player engaging a team Opponent in a distributed fashion. Such games and their strategies have been formalised in concurrent games based on event structures. However there are limitations in founding…

We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports…

Using formal tools in computer science to describe games is an interesting problem. We give games, exactly two person games, an axiomatic foundation based on the process algebra ACP (Algebra of Communicating Process). A fresh operator…

Motivated by emerging decentralized applications, the \emph{game of coding} framework has been recently introduced to address scenarios where the adversary's control over coded symbols surpasses the fundamental limits of traditional coding…

Concurrent multi-player games with $\omega$-regular objectives are a standard model for systems that consist of several interacting components, each with its own objective. The standard solution concept for such games is Nash Equilibrium,…

This paper presents a program logic for reasoning about multithreaded Java-like programs with dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed…

We propose a model for games in which the players have shared access to a blockchain that allows them to deploy smart contracts to act on their behalf. This changes fundamental game-theoretic assumptions about rationality since a contract…

We examine sequential equilibrium in the context of computational games, where agents are charged for computation. In such games, an agent can rationally choose to forget, so issues of imperfect recall arise. In this setting, we consider…

Making threaded programs safe and easy to reason about is one of the chief difficulties in modern programming. This work provides an efficient execution model for SCOOP, a concurrency approach that provides not only data race freedom but…

Sabotage games are played on a dynamic graph, in which one agent, called a runner, attempts to reach a goal state, while being obstructed by a demon who at each round removes an edge from the graph. Sabotage modal logic was proposed to…