CONCUR 2008 - Concurrency Theory

Nash equilibrium is the most commonly-used notion of equilibrium in game theory. However, it suffers from numerous problems. Some are well known in the game theory community; for example, the Nash equilibrium of repeated prisoner’s dilemma is neither normatively nor descriptively reasonable. However, new problems arise when considering Nash equilibrium from a computer science perspective: for example, Nash equilibriumis not robust (it does not tolerate “faulty” or “unexpected” behavior), it does not deal with coalitions, it does not take computation cost into account, and it does not deal with cases where players are not aware of all aspects of the game. Solution concepts that try to address these shortcomings of Nash equilibrium are discussed.

The paper appears in the

Proceedings of the Twenty-Seventh Annual ACM Symposium on Principles of Distributed Computing

, 2008.

Service oriented computing provides technologies that enable multiple organizations to integrate their businesses over the Internet. Typical execution behavior in this type of distributed systems involves a set of autonomous peers interacting with each other through messages. Modeling and analysis of interactions among the peers is a crucial problem in this domain due to following reasons: 1) Organizations may not want to share the internal details of the services they provide to other organizations. In order to achieve decoupling among different peers, it is necessary to specify the interactions among different services without referring to the details of their local implementations. 2) Modeling and analyzing the global behavior of this type of distributed systems is particularly challenging since no single party has access to the internal states of all the participating peers. Desired behaviors have to be specified as constraints on the interactions among different peers since the interactions are the only observable global behavior. Moreover, for this type of distributed systems, it might be worthwhile to specify the interactions among different peers before the services are implemented. Such a top-down design strategy may help different organizations to better coordinate their development efforts.

Concurrency theory is in an exciting period of confusion. Confusion is always exciting because it heralds the coming of new ideas and deeper understanding. There are several ingredients in the cauldron: some new, some not so new. The old ingredients are process algebra, bisimulation and other equivalences and modal logics. The not-so-old ingredients are probability, mobility and real-time, and the new ingredients are knowledge, games and information theory.

Concurrency, as a basic primitive for software construction, is more relevant today than ever before, primarily due to the multi-core revolution. General-purpose software applications must find ways to exploit concurrency explicitly in order to take advantage of multiple cores. However, experience has shown that explicitly parallel programs are difficult to get right. To deliver compelling software products in the multi-core era, we must improve our ability to reason about concurrency.

Dynamic separation is a new programming discipline for systems with transactional memory. We study it formally in the setting of a small calculus with transactions. We provide a precise formulation of dynamic separation and compare it with other programming disciplines. Furthermore, exploiting dynamic separation, we investigate some possible implementations of the calculus and we establish their correctness.

Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first

deterministic

specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a

complete

verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is

nondeterministic

and establishes correctness for all possible contention management schemes.

We investigate a general model of concurrency for shared-memory systems. We introduce some intuitive interleaving semantics within the general framework of automata with concurrency relations and connect it to some partial order approach. Then our main result identifies the expressive power of finite deterministic shared-memory systems with the notion of regular consistent sets of labeled partial orders. We characterize also by means of a coherence property the languages recognized by deadlock-free systems.

This paper presents SOAR: the first oblivious atomicity assertion with polynomial complexity. SOAR enables to check atomicity of a single-writer multi-reader register implementation. The basic idea underlying the low overhead induced by SOAR lies in greedily checking, in a backward manner, specific points of an execution where register operations could be linearized, rather than exploring all possible precedence relations among these.

We illustrate the use of SOAR by implementing it in +CAL. The performance of the resulting automatic verification outperforms comparable approaches by more than an order of magnitude already in executions with only 6 read/write operations. This difference increases to 3-4 orders of magnitude in the “negative” scenario, i.e., when checking some non-atomic execution, with only 5 operations. For example, checking atomicity of every possible execution of a single-writer single-reader (SWSR) register with at most 2 write and 3 read operations with the state of the art oblivious assertion takes more than 58 hours to complete, whereas SOAR takes just 9 seconds.

We introduce

R-automata

– finite state machines which operate on a finite number of unbounded counters. The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. R-automata can be, for example, used to model systems with resources (modeled by the counters) which are consumed in small parts but which can be replenished at once. We define the language accepted by an R-automaton relative to a natural number

D

as the set of words allowing a run along which no counter value exceeds

D

. As the main result, we show decidability of the universality problem, i.e., the problem whether there is a number

D

such that the corresponding language is universal. We present a proof based on finite monoids and the factorization forest theorem. This theorem was applied for distance automata in [12]– a special case of R-automata with one counter which is never reset. As a second technical contribution, we extend the decidability result to R-automata with Büchi acceptance conditions.

We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to.

There are two natural semantics for such systems. The

universal

semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. However, to check if a system avoids a negative specification, it is better to use the

existential

semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates.

We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness turns out to be undecidable. As an alternative to the universal semantics, we propose a

reactive

semantics that allows us to check positive specifications and yet describes a regular set of behaviors.

A well-known theorem in automata theory states that every context-free language is accepted by a pushdown automaton. We investigate this theorem in the setting of processes, using the rooted branching bisimulation and contrasimulation equivalences instead of language equivalence. In process theory, different from automata theory, interaction is explicit, so we realize a pushdown automaton as a regular process communicating with a stack.

For many cryptographic protocols, security relies on the assumption that adversarial entities have limited computational power. This type of security degrades progressively over the lifetime of a protocol. However, some cryptographic services, such as timestamping services or digital archives, are

long-lived

in nature; they are expected to be secure and operational for a very long time (

i.e.

super-polynomial). In such cases, security cannot be guaranteed in the traditional sense: a computationally secure protocol may become insecure if the attacker has a super-polynomial number of interactions with the protocol.

This paper proposes a new paradigm for the analysis of long-lived security protocols. We allow entities to be active for a potentially unbounded amount of real time, provided they perform only a polynomial amount of work

per unit of real time

. Moreover, the space used by these entities is allocated dynamically and must be polynomially bounded. We propose a new notion of

long-term implementation

, which is an adaptation of computational indistinguishability to the long-lived setting. We show that long-term implementation is preserved under polynomial parallel composition and exponential sequential composition. We illustrate the use of this new paradigm by analyzing some security properties of the long-lived timestamping protocol of Haber and Kamat.

The availability of repositories of Web service descriptions enables interesting forms of dynamic Web service discovery, such as searching for Web services exposing a specified behavior – or

contract

. This calls for a formal notion of contract equivalence satisfying two contrasting goals: being as coarse as possible so as to favor Web services reuse, and guaranteeing smooth client/service interaction. We study an equivalence relation under the assumption that interactions are controlled by

orchestrators

. We build a simple orchestration language on top of this theory and we show how to synthesize orchestrators out of Web services contracts.

The synthesis problem asks to construct a reactive finite-state system from an

ω

-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification

ϕ

by computing an environment assumption

ψ

such that the new specification

ψ

→

ϕ

is realizable. Our aim is to construct an assumption

ψ

that constrains only the environment and is as weak as possible. We present a two-step algorithm for computing assumptions. The algorithm operates on the game graph that is used to answer the realizability question. First, we compute a safety assumption that removes a minimal set of environment edges from the graph. Second, we compute a liveness assumption that puts fairness conditions on some of the remaining environment edges. We show that the problem of finding a minimal set of fair edges is computationally hard, and we use probabilistic games to compute a locally minimal fairness assumption.

This paper presents

Smyle

, a tool for synthesizing asynchronous and distributed implementation models from sets of scenarios that are given as message sequence charts (MSCs). The latter specify desired or unwanted behavior of the system to be. Provided with such positive and negative example scenarios,

Smyle

employs dedicated learning techniques and

propositional dynamic logic

(PDL) over MSCs to generate a system model that conforms with the given examples.

We present the tool

Sycraft

(

SYmboliC synthesizeR and Adder of Fault-Tolerance

). In

Sycraft

, a distributed fault-intolerant program is specified in terms of a set of processes and an invariant. Each process is specified as a set of actions in a guarded command language, a set of variables that the process can read, and a set of variables that the process can write. Given a set of fault actions and a specification, the tool transforms the input distributed fault-intolerant program into a distributed fault-tolerant program via a symbolic implementation of respective algorithms.

We introduce subsequence invariants, which characterize the behavior of a concurrent system in terms of the occurrences of synchronization events. Unlike state invariants, which refer to the state variables of the system, subsequence invariants are defined over auxiliary counter variables that reflect how often the event sequences from a given set have occurred so far. A subsequence invariant is a linear constraint over the possible counter values. We allow every occurrence of a subsequence to be interleaved arbitrarily with other events. As a result, subsequence invariants are preserved when a given process is composed with additional processes. Subsequence invariants can therefore be computed individually for each process and then be used to reason about the full system. We present an efficient algorithm for the synthesis of subsequence invariants. Our construction can be applied incrementally to obtain a growing set of invariants given a growing set of event sequences.

The concept of invariance for Parameterised Boolean Equation Systems (PBESs) is studied in greater detail. We identify a weakness with the associated theory and fix this problem by proposing a stronger notion of invariance called global invariance. A precise correspondence is proven between the solution of a PBES and the solution of its invariant-strengthened version; this enables one to exploit global invariants when solving PBESs. Furthermore, we show that global invariants are robust w.r.t. all common PBES transformations and that the existing encodings of verification problems into PBESs preserve the invariants of the processes involved. These traits provide additional support for our notion of global invariants, and, moreover, provide an easy manner for transferring (e.g. automatically discovered) process invariants to PBESs. Several examples are provided that illustrate the advantages of using global invariants in various verification problems.

We propose a framework for model-based diagnosis of systems with mobility and variable topologies, modelled as graph transformation systems. Generally speaking, model-based diagnosis is aimed at constructing explanations of observed faulty behaviours on the basis of a given model of the system. Since the number of possible explanations may be huge we exploit the unfolding as a compact data structure to store them, along the lines of previous work dealing with Petri net models. Given a model of a system and an observation, the explanations can be constructed by unfolding the model constrained by the observation, and then removing incomplete explanations in a pruning phase. The theory is formalised in a general categorical setting: constraining the system by the observation corresponds to taking a product in the chosen category of graph grammars, so that the correctness of the procedure can be proved by using the fact that the unfolding is a right adjoint and thus it preserves products. The theory thus should be easily applicable to a wide class of system models, including graph grammars and Petri nets.

We develop a theory of

sorted bigraphical reactive systems

.

Every application of bigraphs in the literature has required an extension, a sorting, of pure bigraphs. In turn, every such application has required a redevelopment of the theory of pure bigraphical reactive systems for the sorting at hand. Here we present a general construction of sortings. The constructed sortings always sustain the behavioural theory of pure bigraphs (in a precise sense), thus obviating the need to redevelop that theory for each new application. As an example, we recover Milner’s local bigraphs as a sorting on pure bigraphs.

Technically, we give our construction for ordinary reactive systems, then lift it to bigraphical reactive systems. As such, we give also a construction of sortings for ordinary reactive systems. This construction is an improvement over previous attempts in that it produces smaller and much more natural sortings, as witnessed by our recovery of local bigraphs as a sorting.

We present an algorithm for partial order reduction in the context of a countable universe of deterministic actions, of which finitely many are enabled at any given state. This means that the algorithm is suited for a setting in which resources, such as processes or objects, are dynamically created and destroyed, without an

a priori

bound. The algorithm relies on abstract enabling and disabling relations among actions, rather than associated sets of concurrent processes. It works by selecting so-called

probe sets

at every state, and backtracking in case the probe is later discovered to have missed some possible continuation.

We show that this improves the potential reduction with respect to persistent sets. We then instantiate the framework by assuming that states are essentially sets of

entities

(out of a countable universe) and actions test, delete and create such entities. Typical examples of systems that can be captured in this way are Petri nets and (more generally) graph transformation systems. We show that all the steps of the algorithm, including the estimation of the missed actions, can be effectively implemented for this setting.

In the context of probabilistic automata, time efficient algorithms for probabilistic simulations have been proposed lately. The space complexity thereof is quadratic in the size of the transition relation, thus space requirements often become the practical bottleneck. In this paper, we exploit ideas from [3] to arrive at a space-efficient algorithm for computing probabilistic simulations based on partition refinement. Experimental evidence is given that not only the space-efficiency is improved drastically. The experiments often require orders of magnitude less time.

Abstraction is a key technique to combat the state space explosion problem in model checking probabilistic systems. In this paper we present new ways to abstract Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). The main advantage of our abstractions is that they result in abstract models that are

purely probabilistic

, which maybe more amenable to automatic analysis than models with both nondeterministic and probabilistic steps that typically arise from previously known abstraction techniques. A key technical tool, developed in this paper, is the construction of least upper bounds for any collection of probability measures. This upper bound construction may be of independent interest that could be useful in the abstract interpretation and static analysis of probabilistic programs.

This paper proposes a novel abstraction technique based on Erlang’s method of stages for continuous-time Markov chains (CTMCs). As abstract models

Erlang-k

interval processes

are proposed where state residence times are governed by Poisson processes and transition probabilities are specified by intervals. We provide a three-valued semantics of CSL (Continuous Stochastic Logic) for Erlang-

k

interval processes, and show that both affirmative and negative verification results are preserved by our abstraction. The feasibility of our technique is demonstrated by a quantitative analysis of an enzyme-catalyzed substrate conversion, a well-known case study from biochemistry.

This paper presents a novel algorithm to compute weak bisimulation quotients for finite acyclic models. It is developed in the setting of interactive Markov chains, a model overarching both labelled transition systems and continuous-time Markov chains. This model has lately been used to give an acyclic compositional semantics to dynamic fault trees, a reliability modelling formalism.

While the theoretical complexity does not change substantially, the algorithm performs very well in practice, almost linear in the size of the input model. We use a number of case studies to show that it is vastly more efficient than the standard bisimulation minimisation algorithms. In particular we show the effectiveness in the analysis of dynamic fault trees.

Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the

quasi-static scheduling

problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining existence of quasi-static scheduling policies is undecidable. However, we show that the problem is decidable for the important sub-class of “data branching” systems in which control flow branchings are due exclusively to data-dependent internal choices made by the sequential components. This decidability result—which is non-trivial to establish—exploits ideas derived from the Karp and Miller coverability tree [8] as well as the existential boundedness notion of languages of message sequence charts [6].

We consider

imperfect-information

parity games in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games,

i.e.

to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent

perfect-information

game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies.

In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. We have implemented this algorithm as a prototype. To our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.

We consider asynchronous networks of finite-state systems communicating via a combination of reliable and lossy fifo channels. Depending on the topology, the reachability problem for such networks may be decidable. We provide a complete classification of network topologies according to whether they lead to a decidable reachability problem. Furthermore, this classification can be decided in polynomial-time.

We address the reachability problem in acyclic networks of pushdown systems. We consider communication based either on shared memory or on message passing through unbounded lossy channels. We prove mainly that the reachability problem between recognizable sets of configurations (i.e., definable by a finite union of products of finite-state automata) is decidable for such networks, and that for lossy channel pushdown networks, the channel language is effectively recognizable. This fact holds although the set of reachable configurations (including stack contents) for a network of depth (at least) 2 is not rational in general (i.e., not definable by a multi-tape finite automaton). Moreover, we prove that for a network of depth 1, the reachability set is rational and effectively constructible (under an additional condition on the topology for lossy channel networks).

We present a framework that combines ideas from spatial logics and Igarashi and Kobayashi’s behavioural type systems, drawing benefits from both. In our approach, type systems for the pi-calculus are introduced where newly declared (restricted) names are annotated with spatial process properties, predicating on those names, that are expected to hold in the scope of the declaration. Types are akin to

ccs

terms and account for the processes abstract behaviour and “shallow” spatial structure. The type systems relies on spatial model checking, but properties are checked against types rather than against processes. The considered class of properties is rather general and, differently from previous proposals, includes both safety and liveness ones, and is not limited to invariants.

Spatial logics have been proposed to reason locally and modularly on algebraic models of distributed systems. In this paper we define the spatial equational logic A

π

L whose models are processes of the applied

π

-calculus. This extension of the

π

-calculus allows term manipulation and records communications as active substitutions in a frame, thus augmenting the underlying predefined equational theory. Our logic allows one to reason locally either on frames or on processes, thanks to static and dynamic spatial operators. We study the logical equivalences induced by various relevant fragments of A

π

L, and show in particular that the whole logic induces a coarser equivalence than structural congruence. We give characteristic formulae for some of these equivalences and for static equivalence. Going further into the exploration of A

π

L’s expressivity, we also show that it can eliminate standard term quantification.

We propose an interactional generalisation of structured exceptions based on the session type discipline. Interactional exceptions allow communicating peers to asynchronously and collaboratively escape from the middle of a dialogue and reach another in a coordinated fashion, under an arbitrary nesting of exceptions. New exception types guarantee communication safety and offer a precise type-abstraction of advanced conversation patterns found in practice. Protocols for coordinating normal and exceptional exit among asynchronously running sessions are introduced. The liveness property established under these protocols guarantees consistency of coordinated exception handling among communicating peers.

A multiparty session forms a unit of structured interactions among many participants which follow a prescribed scenario specified as a global type signature. This paper develops, besides a more traditional

communication

type system, a novel static

interaction

type system for global progress in dynamically interleaved multiparty sessions.

We present a polynomial-time algorithm deciding bisimilarity between a normed BPA process and a normed BPP process. This improves the previously known exponential upper bound by Černá, Křetínský, Kučera (1999). The algorithm relies on a polynomial bound for the “finite-state core” of the transition system generated by the BPP process. The bound is derived from the “prime form” of the underlying BPP system (where bisimilarity coincides with equality); we suggest an original algorithm for the respective transformation.

We propose a rule format that guarantees associativity of binary operators with respect to all notions of behavioral equivalence that are defined in terms of (im)possibility of transitions, e.g., the notions below strong bisimilarity in van Glabbeek’s spectrum. The initial format is a subset of the De Simone format. We show that all trivial generalizations of our format are bound for failure. We further extend the format in a few directions and illustrate its application to several formalisms in the literature. A subset of the format is studied to obtain associativity with respect to graph isomorphism.

We present a new labelled transition system (

lts

) for the ambient calculus on which ordinary bisimilarity coincides with contextual equivalence. The key feature of this

lts

is that it is the fruit of ongoing work on developing a systematic procedure for deriving

lts

s in the structural style from the underlying reduction semantics and observability. Notably, even though we have derived our

lts

for ambients systematically it compares very favourably with existing transition systems for the same calculus.

We consider nondeterministic and probabilistic termination problems in a process algebra that is equivalent to basic chemistry. We show that the existence of a terminating computation is decidable, but that termination with any probability strictly greater than zero is undecidable. Moreover, we show that the fairness intrinsic in stochastic computations implies that termination of all computation paths is undecidable, while it is decidable in a nondeterministic framework.

In this paper, we present a unified approach to evaluating the relative expressive power of process calculi. In particular, we identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a good means for language comparison. We argue that the combination of such criteria is a valid proposal by noting that: (

i

) the best known encodings appeared in the literature satisfy them; (

ii

) this notion is not trivial, because there exist encodings that do not satisfy all the criteria we have proposed; (

iii

) the best known separation results can be formulated in terms of our criteria; and (

iv

) some widely believed (but never formally proved) separation results can be proved by using the criteria we propose. Moreover, the way in which we prove known separation results is easier and more uniform than the way in which such results were originally proved.

Comparison between different formalisms and models is often by flattening structure and reducing them to behaviorally equivalent models

e.g.

automaton and Turing machine. This leads to a notion of expressiveness which is not adequate for component-based systems where separation between behavior and coordination mechanisms is essential. The paper proposes a notion of glue expressiveness for component-based frameworks characterizing their ability to coordinate components.

Glue

is a closed under composition set of operators mapping tuples of behavior into behavior. Glue operators preserve behavioral equivalence. They only restrict the behavior of their arguments by performing memoryless coordination.

Behavioral equivalence induces an equivalence on glue operators. We compare expressiveness of two glues

G

1

and

G

2

by considering whether glue operators of

G

1

have equivalent ones in

G

2

(strong expressiveness). Weak expressiveness is defined by allowing a finite number of additional behaviors in the arguments of operators of

G

2

.

We propose an SOS-style definition of glues, where operators are characterized as sets of SOS-rules specifying the transition relation of composite components from the transition relations of their constituents. We provide expressiveness results for the glues of BIP and of process algebras such as CCS, CSP and SCCS. We show that for the considered expressiveness criteria, glues of the considered process calculi are less expressive than general SOS glue. Furthermore, glue of BIP has exactly the same strong expressiveness as glue definable by the SOS characterization.