CONCUR 2012 – Concurrency Theory

We enhance the notion of a computation of the classical theory of computing with the notion of interaction from concurrency theory. In this way, we enhance a Turing machine as a model of computation to a Reactive Turing Machine that is an abstract model of a computer as it is used nowadays, always interacting with the user and the world.

The algebraic theory of effects [7,8,4] continues Moggi’s monadic approach to effects [5,6,1] by concentrating on a particular class of monads: the

algebraic

ones, that is, the free algebra monads of given equational theories. The operations of such equational theories can be thought of as

effect constructors

, as it is they that give rise to effects. Examples include exceptions (when the theory is that of a set of constants with no axioms), nondeterminism (when the theory could be that of a semilattice, for nondeterminism, with a zero, for deadlock), and action (when the theory could be a set of unary operations with no axioms).

I describe my investigations into the highly-secret role that Alan Turing played during World War II, after his pre-war theoretical work on computability and the concept of a universal machine, in the development of the world’s first electronic computers. These investigations resulted in my obtaining and publishing, in 1972, some limited information about Turing’s contributions to the work on code-breaking machines at Bletchley Park, the fore-runner of the UK Government Communications Headquarters (GCHQ). Some years later I was able to obtain permission to compile and publish the first officially-authorised account of the work, led by T.H. (Tommy) Flowers at the Post Office Dollis Hill Research Station, on the construction of a series of special purpose electronic computers for Bletchley Park, computers that made a vital contribution to the Allied war effort.

Concurrency theory and real-world multiprocessors have developed in parallel for the last 50 years, from their beginnings in the mid 1960s. Both have been very productive: concurrency theory has given us a host of models, calculi, and proof techniques, while engineered multiprocessors are now ubiquitous, from 2-8 core smartphones and laptops through to servers with 1024 or more hardware threads. But the fields have scarcely communicated, and the shared-memory interaction primitives offered by those mainstream multiprocessors are very different from the theoretical models that have been heavily studied.

We propose to study concurrent games on a new extension of Vector Addition Systems with States, where inhibition conditions are added for modeling purposes. Games are a well-suited framework to solve control problems, and concurrent semantics reflect realistic situations where the environment can always produce a move before the controller, although it is never required to do so. This is in contrast with previous works, which focused mainly on turn-based semantics. Moreover, we consider asymmetric games, where environment and controller do not have the same capabilities, although they both have restricted power. In this setting, we investigate reachability and safety objectives, which are not dual to each other anymore, and we prove that (i) reachability games are undecidable for finite targets, (ii) they are 2-EXPTIME-complete for upward-closed targets and (iii) safety games are co-NP-complete for finite, upward-closed and semi-linear targets. Moreover, for the decidable cases, we build a finite representation of the corresponding controllers.

This paper is about reachability analysis in a restricted subclass of multi-pushdown automata: we assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We prove decidability of the reachability problem, and computability of the backward reachability set. As the main contribution, we identify relevant subclasses where the reachability problem becomes NP-complete. This matches the complexity of the same problem for communication-free vector addition systems (known also as commutative context-free graphs), a special case of stateless multi-pushdown automata.

We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnueli’s probabilistic concurrent programs. Some characterizations of the reachable space, uniformly repeatedly reachable space and termination of a concurrent quantum program are derived by the analysis of their mathematical structures. Based on these characterizations, algorithms for computing the reachable space and uniformly repeatedly reachable space and for deciding the termination are given.

Weighted automata map input words to real numbers and are useful in reasoning about quantitative systems and specifications. The containment problem for weighted automata asks, given two weighted automata

$\mathcal{A}$

and

$\mathcal{B}$

, whether for all words

w

, the value that

$\mathcal{A}$

assigns to

w

is less than or equal to the value

$\mathcal{B}$

assigns to

w

. The problem is of great practical interest, yet is known to be undecidable. Efforts to approximate weighted containment by weighted variants of the simulation pre-order still have to cope with large state spaces. One of the leading approaches for coping with large state spaces is abstraction. We introduce an abstraction-refinement paradigm for weighted automata and show that it nicely combines with weighted simulation, giving rise to a feasible approach for the containment problem. The weighted-simulation pre-order we define is based on a quantitative two-player game, and the technical challenge in the setting origins from the fact the values that the automata assign to words are unbounded. The abstraction-refinement paradigm is based on under- and over-approximation of the automata, where approximation, and hence also the refinement steps, refer not only to the languages of the automata but also to the values they assign to words.

Networks of timed automata (NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given a NTA

A

1

 ∥ 

A

2

where

A

2

reads some clocks reset by

A

1

, does there exist a NTA

A

′

1

 ∥ 

A

′

2

without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only. We discuss a formalization of the problem and give a criterion using the notion of contextual timed transition system, which represents the behavior of

A

2

when in parallel with

A

1

. Finally, we effectively build

A

′

1

 ∥ 

A

′

2

when it exists.

Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express

ω

-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.

A weighted automaton is functional if any two accepting runs on the same finite word have the same value. In this paper, we investigate functional weighted automata for four different measures: the sum, the mean, the discounted sum of weights along edges and the ratio between rewards and costs. On the positive side, we show that functionality is decidable for the four measures. Furthermore, the existential and universal threshold problems, the language inclusion problem and the equivalence problem are all decidable when the weighted automata are functional. On the negative side, we also study the quantitative extension of the realizability problem and show that it is undecidable for sum, mean and ratio. We finally show how to decide whether the language associated with a given functional automaton can be defined with a deterministic one, for sum, mean and discounted sum. The results on functionality and determinizability are expressed for the more general class of functional weighted automata over groups. This allows one to formulate within the same framework new results related to discounted sum automata and known results on sum and mean automata. Ratio automata do not fit within this general scheme and specific techniques are required to decide functionality.

We study the succinctness of different classes of succinctly presented finite transition systems with respect to bisimulation equivalence. Our results show that synchronized product of finite automata, hierarchical graphs, and timed automata are pairwise incomparable in this sense. We moreover study the computational complexity of deciding simulation preorder and bisimulation equivalence on these classes.

In a previous publication, we enumerated all stuttering-insensitive linear-time (in a well-defined sense) congruences with respect to action prefix, hiding, relational renaming, and parallel composition for finite labelled transition systems. There are 20 of them. They are built from the alphabet, traces, two kinds of divergence traces, and five kinds of failures. Now we remove the finiteness assumption. To re-establish the congruence property, four kinds of infinite traces are needed. Some congruences split to two and some to three, yielding altogether 40 congruences. Like its predecessor, because of lack of space, also this publication concentrates on proving the absence of more congruences.

While it was defined long ago, the extension of

CTL

with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that

QCTL

coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking

ATL

-like temporal logics for games.

Strategy Logic

(

Sl

, for short) has been recently introduced by Mogavero, Murano, and Vardi as a formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, strictly subsuming all major previously studied modal logics for strategic reasoning, including

Atl

,

Atl

*, and the like. The price that one has to pay for the expressiveness of

Sl

is the lack of important model-theoretic properties and an increased complexity of decision problems. In particular,

Sl

does not have the bounded-tree model property and the related satisfiability problem is

highly undecidable

while for

Atl

* it is 2

ExpTime-complete

. An obvious question that arises is then what makes

Atl

* decidable. Understanding this should enable us to identify decidable fragments of

Sl

. We focus, in this work, on the limitation of

Atl

* to allow only one temporal goal for each strategic assertion and study the fragment of

Sl

with the same restriction. Specifically, we introduce and study the syntactic fragment

One-Goal Strategy Logic

(

Sl[1g]

, for short), which consists of formulas in prenex normal form having a single temporal goal at a time for every strategy quantification of agents. We show that

Sl[1g]

is strictly more expressive than

Atl

*. Our main result is that

Sl[1g]

has the bounded tree-model property and its satisfiability problem is 2

ExpTime-complete

, as it is for

Atl

*.

Having

stateful

specifications to track the states of processes, such as the balance of a customer for online shopping or the booking number of a transaction, is needed to verify real-life interacting systems. For safety assurance of distributed IT infrastructures, specifications need to capture states in the presence of asynchronous interactions. We demonstrate that not all specifications are suitable for asynchronous observations because they implicitly rely on an order-preservation assumption. To establish a theory of asynchronous specifications, we use the interplay between synchronous and asynchronous semantics, through which we characterise the class of specifications suitable for verifications through asynchronous interactions. The resulting theory offers a general semantic setting as well as concrete methods to analyse and determine semantic well-formedness (healthiness) of specifications with respect to asynchronous observations, for both static and dynamic verifications. In particular, our theory offers a key criterion for suitability of specifications for distributed dynamic verifications.

Designing and analysing multiparty distributed interactions can be achieved either by means of a global view (e.g. in choreography-based approaches) or by composing available computational entities (e.g. in service orchestration).

This paper proposes a typing systems which allows, under some conditions, to synthesise a choreography (i.e. a multiparty global type) from a set of local session types which describe end-point behaviours (i.e. local types).

History dependent abstraction operators are the key for scaling existing methods for active learning of automata to realistic applications. Recently, Aarts, Jonsson & Uijen have proposed a framework for history dependent abstraction operators. Using this framework they succeeded to automatically infer models of several realistic software components with large state spaces, including fragments of the TCP and SIP protocols. Despite this success, the approach of Aarts et al. suffers from limitations that seriously hinder its applicability in practice. In this article, we get rid of some of these limitations and present four important generalizations/improvements of the theory of history dependent abstraction operators. Our abstraction framework supports: (a) interface automata instead of the more restricted Mealy machines, (b) the concept of a learning purpose, which allows one to restrict the learning process to relevant behaviors only, (c) a richer class of abstractions, which includes abstractions that overapproximate the behavior of the system-under-test, and (d) a conceptually superior approach for testing correctness of the hypotheses that are generated by the learner.

Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. Unfortunately, it assumes a complete isolation between a library and its client, with interactions limited to passing values of a given data type. This is inappropriate for common programming languages, where libraries and their clients can communicate via the heap, transferring the ownership of data structures, and can even run in a shared address space without any memory protection. In this paper, we present the first definition of linearizability that lifts this limitation and establish an Abstraction Theorem: while proving a property of a client of a concurrent library, we can soundly replace the library by its abstract implementation related to the original one by our generalisation of linearizability. We also prove that linearizability with ownership transfer can be derived from the classical one if the library does not access some of data structures transferred to it by the client.

We propose an improvement to session-types, introducing nested protocols, the possibility to call a subprotocol from a parent protocol. This feature adds expressiveness and modularity to the existing session-type theory, allowing arguments to be passed and enabling higher-order protocols definition. Our theory is introduced through a new type system for protocols handling subprotocol calls, and its implementation in a session-calculus. We propose validation and satisfaction relations between specification and implementation. Sound behaviour is enforced thanks to the usage of kinds and well-formedness, allowing us to ensure progress and subject reduction. In addition, we describe an extension of our framework allowing subprotocols to send back results.

We introduce an observational theory of global progress properties such as non-blockingness and wait-freedom based on a linear

π

-calculus. The theory uniformly captures such properties both extensionally and intensionally, by using fair transition relations and partial failures, which represent stalling activities. A fairness-enriched bisimilarity preserves these properties and is a congruence. The framework is applied to the semantic characterisation and separation results for concurrent data structures including different queue implementations.

We study duality between input and output in the

π

-calculus. In dualisable versions of

π

, including

πI

and fusions, duality breaks with the addition of ordinary input/output types. We introduce

$\overline\pi$

, intuitively the minimal symmetrical conservative extension of

π

with input/output types. We prove some duality properties for

$\overline\pi$

and we study embeddings between

$\overline\pi$

and

π

in both directions. As an example of application of the dualities, we exploit the dualities of

$\overline\pi$

and its theory to relate two encodings of call-by-name

λ

-calculus, by Milner and by van Bakel and Vigliotti, syntactically quite different from each other.

We introduce spatial and epistemic process calculi for reasoning about spatial information and knowledge distributed among the agents of a system. We introduce domain-theoretical structures to represent spatial and epistemic information. We provide operational and denotational techniques for reasoning about the potentially infinite behaviour of spatial and epistemic processes. We also give compact representations of infinite objects that can be used by processes to simulate announcements of common knowledge and global information.

In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC which depends on the environment and on the other agents only through the solution of the fluid differential equation. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae and of reachability probabilities. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.

We study stochastic two-player games where the goal of one player is to achieve

precisely

a given expected value of the objective function, while the goal of the opponent is the opposite. Potential applications for such games include controller synthesis problems where the optimisation objective is to maximise or minimise a given payoff function while respecting a strict upper or lower bound, respectively. We consider a number of objective functions including reachability,

ω

-regular, discounted reward, and total reward. We show that precise value games are not determined, and compare the memory requirements for winning strategies. For stopping games we establish necessary and sufficient conditions for the existence of a winning strategy of the controller for a large class of functions, as well as provide the constructions of compact strategies for the studied objectives.

This paper introduces a framework for the efficient modelling and generation of Markov automata. It consists of (1) the data-rich process-algebraic language MAPA, allowing concise modelling of systems with nondeterminism, probability and Markovian timing; (2) a restricted form of the language, the MLPPE, enabling easy state space generation and parallel composition; and (3) several syntactic reduction techniques on the MLPPE format, for generating equivalent but smaller models.

Technically, the framework relies on an encoding of MAPA into the existing prCRL language for probabilistic automata. First, we identify a class of transformations on prCRL that can be lifted to the Markovian realm using our encoding. Then, we employ this result to reuse prCRL’s linearisation procedure to transform any MAPA specification to an equivalent MLPPE, and to lift three prCRL reduction techniques to MAPA. Additionally, we define two novel reduction techniques for MLPPEs. All our techniques treat data as well as Markovian and interactive behaviour in a fully symbolic manner, working on specifications instead of models and thus reducing state spaces prior to their construction. The framework has been implemented in our tool SCOOP, and a case study on polling systems and mutual exclusion protocols shows its practical applicability.

We study behavioural relations for process algebra with a fluid semantics given in terms of a system of ordinary differential equations (ODEs). We introduce

label equivalence

, a relation which is shown to induce an

exactly lumped fluid model

, a potentially smaller ODE system which can be exactly related to the original one. We show that, in general, for two processes that are related in the fluid sense nothing can be said about their relationship from stochastic viewpoint. However, we identify a class of models for which label equivalence implies a correspondence, called

semi-isomorphism

, between their transition systems that are at the basis of the Markovian interpretation.

We present a method to decompose HML formulae for reactive probabilistic processes. This gives rise to a compositional modal proof system for the satisfaction relation of probabilistic process algebras. The satisfaction problem of a probabilistic HML formula for a process term is reduced to the question of whether its subterms satisfy a derived formula obtained via the operational semantics.

Coalgebras in a Kleisli category yield a generic definition of trace semantics for various types of labelled transition systems. In this paper we apply this generic theory to generative

probabilistic transition systems

, short

PTS

, with

arbitrary (possibly uncountable) state spaces

. We consider the

sub-probability monad

and the

probability monad (Giry monad)

on the category of measurable spaces and measurable functions. Our main contribution is that the existence of a final coalgebra in the Kleisli category of these monads is closely connected to the measure-theoretic extension theorem for sigma-finite pre-measures. In fact, we obtain a practical definition of the trace measure for both

finite

and

infinite traces

of PTS that subsumes a well-known result for discrete probabilistic transition systems.

Interval order structures

are useful tools to model abstract concurrent histories, i.e. sets of equivalent system runs, when system runs are modeled with

interval orders

. The paper shows how interval order structures can be modeled by

partially commutative monoids

, called

interval traces

.

We develop a polynomial translation from finite control processes (an important fragment of

π

-calculus) to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural (there is a close correspondence between the control flow of the original specification and the resulting Petri net), enjoys a bisimulation result, and it is suitable for practical model checking.

Traces – and their extension called combined traces (comtraces) – are two formal models used in the analysis and verification of concurrent systems. Both models are based on concepts originating in the theory of formal languages, and they are able to capture the notions of causality and simultaneity of atomic actions which take place during the process of a system’s operation. The aim of this paper is a transfer to the domain of comtraces and developing of some fundamental notions, which proved to be successful in the theory of traces. In particular, we introduce and then apply the lexicographical canonical form of comtraces, as well as the representation of a comtrace utilising its linear projections to binary action subalphabets. We also provide two algorithms related to the new notions. Using them, one can solve, in an efficient way, the problem of step sequence equivalence in the context of comtraces. One may view our results as a first step towards the development of infinite combined traces, as well as recognisable languages of combined traces.

Recent work studied the unfolding construction for contextual nets, i.e. nets with read arcs. Such unfoldings are more concise and can usually be constructed more efficiently than for Petri nets. However, concrete verification algorithms exploiting these advantages were lacking so far. We address this question and propose SAT-based verification algorithms for deadlock and reachability of contextual nets. Moreover, we study optimizations of the SAT encoding and report on experiments.

Link reversal is an algorithmic method with various applications. Originally proposed by Gafni and Bertsekas in 1981 for routing in radio networks, it has been later applied also to solve concurrency related problems as mutual exclusion, resource allocation, and leader election. For resource allocation, conflicts can be represented by conflict graphs, and link reversal algorithms work on these graphs to resolve conflicts. In this paper we establish that executions of link reversal algorithms on large graphs are similar (a notion which we make precise in the paper) to executions on smaller graphs. This similarity then allows to verify linear time temporal properties of large systems, by verifying a smaller one.

We consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the

coverability problem

for

well-structured transition systems

(WSTS). In this paper, we present a novel, sound and complete yet empirically much improved solution to this problem. The key idea to achieve a compact search structure is to track

uncoverability

only for

minimal

uncoverable elements, even if these elements are not part of the original coverability query. To this end, our algorithm examines elements in the downward closure of elements backward-reachable from the initial queries. A downside is that the algorithm may unnecessarily explore elements that turn out coverable and thus fail to contribute to the proof minimization. We counter this effect using a forward search engine that simultaneously generates (a subset of all) coverable elements, e.g., a generalized Karp-Miller procedure. We demonstrate in extensive experiments on

$\mathcal{C}$

programs that our approach targeting minimal uncoverability proofs outperforms existing techniques by orders of magnitude.

We present a framework for verifying transactional memory (TM) algorithms. Specifications and algorithms are specified using I/O automata, enabling hierarchical proofs that the algorithms implement the specifications. We have used this framework to develop what we believe is the first fully formal machine-checked verification of a practical TM algorithm: the NOrec algorithm of Dalessandro, Spear and Scott.

Our framework is available for others to use and extend. New proofs can leverage existing ones, eliminating significant work and complexity.

The model checking problem for propositional dynamic logic (PDL) over message sequence charts (MSCs) and communicating finite state machines (CFMs) asks, given a channel bound

B

, a PDL formula

ϕ

and a CFM

$\mathcal{C}$

, whether every existentially

B

-bounded MSC

M

accepted by

$\mathcal{C}$

satisfies

ϕ

. Recently, it was shown that this problem is PSPACE-complete. In the present work, we consider CRPDL over MSCs which is PDL equipped with the operators converse and repeat. The former enables one to walk back and forth within an MSC using a single path expression whereas the latter allows to express that a path expression can be repeated infinitely often. To solve the model checking problem for this logic, we define global message sequence chart automata (gMSCAs) which are multi-way alternating parity automata walking on MSCs. By exploiting a new concept called concatenation states, we are able to inductively construct, for every CRPDL formula

ϕ

, a finite set of gMSCAs

$\mathfrak{G}$

such that the set of models of

ϕ

equals the union of the languages of the gMSCAs from

$\mathfrak{G}$

. As a result, we obtain that the model checking problem for CRPDL and CFMs is still in PSPACE.

Multi-threaded programs with recursion are naturally modeled as multi-pushdown systems. The behaviors are represented as multiply nested words (MNWs), which are words enriched with additional binary relations for each stack matching a push operation with the corresponding pop operation. Any MNW can be decomposed by two basic and natural operations: shuffle of two sequences of factors and merge of consecutive factors of a sequence. We say that the split-width of a MNW is k if it admits a decomposition where the number of factors in each sequence is at most k. The MSO theory of MNWs with split-width

k

is decidable. We introduce two very general classes of MNWs that strictly generalize known decidable classes and prove their MSO decidability via their split-width and obtain comparable or better bounds of tree-width of known classes.

We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a relevant feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. Such decidability result holds in actors with states when the number of actors is finite and the state is read-only.

In the original version, the name of the second author is incorrect. Instead of “Mahdi M. Jaghoori” it should be read as “Mohammad Mahdi Jaghoori”.