 |
 |
23rd International Conference on Concurrency Theory (CONCUR 2012)
2012 Editors: Irek Ulidowski, Maciej Koutny
1. Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems
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 $\varphi$ and a CFM $\mathcal{C}$, whether every existentially $B$-bounded MSC $M$ accepted by $\mathcal{C}$ satisfies $\varphi$. 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 message sequence chart automata (MSCAs) 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 $\varphi$, an MSCA precisely accepting the set of models of $\varphi$. As a result, we obtain that the model checking problem for CRPDL and CFMs is still in PSPACE.
2. Algebraic Structure of Combined Traces
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 notion of indivisible steps, 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.
3. Reachability Problem for Weak Multi-Pushdown Automata
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, a special case of stateless multi-pushdown automata.
4. All Linear-Time Congruences for Familiar Operators
The detailed behaviour of a system is often represented as a labelled transition system (LTS) and the abstract behaviour as a stuttering-insensitive semantic congruence. Numerous congruences have been presented in the literature. On the other hand, there have not been many results proving the absence of more congruences. This publication fully analyses the linear-time (in a well-defined sense) region with respect to action prefix, hiding, relational renaming, and parallel composition. It contains 40 congruences. They are built from the alphabet, two kinds of traces, two kinds of divergence traces, five kinds of failures, and four kinds of infinite traces. In the case of finite LTSs, infinite traces lose their role and the number of congruences drops to 20. The publication concentrates on the hardest and most novel part of the result, that is, proving the absence of more congruences.
5. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems
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. Finally we consider two example systems with uncountable state spaces and apply our theory to calculate their trace measures.
6. Linearizability with Ownership Transfer
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. This allows abstracting from the details of the library implementation while reasoning about the client. 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.
7. A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets
We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys a bisimulation result, and is suitable for practical model checking.
8. Avoiding Shared Clocks in Networks of Timed Automata
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, i.e. transitions of one automaton may be guarded by conditions on the value of clocks reset by another automaton. 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 an NTA A1 || A2 where A2 reads some clocks reset by A1, does there exist an 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, in particular by copying the value of their neighbor's clocks. We discuss a formalization of the problem and define an appropriate behavioural equivalence. Then we give a criterion using the notion of contextual timed transition system, which represents the behavior of A2 when in parallel with A1. Finally, we effectively build A'1 || A'2 when it exists.