CONCUR 2011 – Concurrency Theory

We give en example-guided introduction to a framework that we have developed in recent years in order to extend the applicability of program verification to the context of systems modeled as infinite-state Markov chains. In particular, we describe the class of

decisive Markov chains

, and show how to perform qualitative and quantitative analysis of Markov chains that arise from probabilistic extensions of classical models such as Petri nets and communicating finite-state processes.

State machine replication

reduces distributed to centralized computing. Any sequential service, modeled by a state machine, can be replicated over any number of processes and made highly available to all of them. At the heart of this fundamental reduction lies the so called

universal consensus

abstraction, key to providing the illusion of single shared service, despite replication.

Yet, as universal as it may be, consensus is just one specific instance of a more general abstraction,

k-set consensus

where, instead of agreeing on a unique decision, the processes may diverge but at most

k

different decisions are reached. It is legitimate to ask whether the celebrated state machine replication construct has its analogue with

k

 > 1. If it did not, one could question the aura of distributed computing deserving an underpinning Theory for 1, the unit of multiplication, would be special in a field, distributed computing, that does not arithmetically multiply.

This paper presents, two decades after

k

-set consensus was introduced, the generalization with

k

 > 1 of state machine replication. We show that with

k

-set consensus, any number of processes can emulate

k

state machines of which at least one remains highly available. While doing so, we also generalize the very notion of consensus universality.

Process discovery—discovering a process model from example behavior recorded in an event log—is one of the most challenging tasks in process mining. The primary reason is that conventional modeling languages (e.g., Petri nets, BPMN, EPCs, and ULM ADs) have difficulties representing the observed behavior properly and/or succinctly. Moreover, discovered process models tend to have deadlocks and livelocks. Therefore, we advocate a new representation more suitable for process discovery:

causal nets

. Causal nets are related to the representations used by several process discovery techniques (e.g., heuristic mining, fuzzy mining, and genetic mining). However, unlike existing approaches, we provide declarative semantics more suitable for process mining. To clarify these semantics and to illustrate the non-local nature of this new representation, we relate causal nets to Petri nets.

We consider approaches for causal semantics of Petri nets, explicitly representing dependencies between transition occurrences. For one-safe nets or condition/event-systems, the notion of process as defined by Carl Adam Petri provides a notion of a run of a system where causal dependencies are reflected in terms of a partial order. A wellknown problem is how to generalise this notion for nets where places may carry several tokens. Goltz and Reisig have defined such a generalisation by distinguishing tokens according to their causal history. However, this so-called

individual token interpretation

is often considered too detailed. A number of approaches have tackled the problem of defining a more abstract notion of process, thereby obtaining a so-called

collective token interpretation

. Here we give a short overview on these attempts and then identify a subclass of Petri nets, called

structural conflict nets

, where the interplay between conflict and concurrency due to token multiplicity does not occur. For this subclass, we define abstract processes as equivalence classes of Goltz-Reisig processes. We justify this approach by showing that we obtain exactly one maximal abstract process if and only if the underlying net is conflict-free with respect to a canonical notion of conflict.

Timed temporal logics exhibit a bewildering diversity of operators and the resulting decidability and expressiveness properties also vary considerably. We study the expressive power of timed logics

TPTL

[

U

,

S

] and

MTL

[

U

I

,

S

I

] as well as of their several fragments. Extending the LTL EF games of Etessami and Wilke, we define

MTL

Ehrenfeucht-Fraïssé games on a pair of timed words. Using the associated EF theorem, we show that, expressively, the timed logics

BoundedMTL

[

U

I

,

S

I

],

MTL

[

F

I

,

P

I

] and

MITL

[

U

I

,

S

I

] (respectively incorporating the restrictions of boundedness, unary modalities and non-punctuality), are all pairwise incomparable. As our first main result, we show that

MTL

[

U

I

,

S

I

] is

strictly contained

within the freeze logic

TPTL

[

U

,

S

] for both weakly and strictly monotonic timed words, thereby extending the result of Bouyer

et al

and completing the proof of the original conjecture of Alur and Henziger from 1990. We also relate the expressiveness of a recently proposed deterministic freeze logic

TTL

[

X

θ

,

Y

θ

] (with NP-complete satisfiability) to

MTL

. As our second main result, we show by an explicit reduction that

TTL

[

X

θ

,

Y

θ

] lies strictly within the unary, non-punctual logic

MITL

[

F

I

,

P

I

]. This shows that deterministic freezing with punctuality is expressible in the non-punctual

MITL

[

F

I

,

P

I

].

Timed automata follow a mathematical semantics, which assumes perfect precision and synchrony of clocks. Since this hypothesis does not hold in digital systems, properties proven formally on a timed automaton may be lost at implementation. In order to ensure implementability, several approaches have been considered, corresponding to different hypotheses on the implementation platform. We address two of these: A timed automaton is samplable if its semantics is preserved under a discretization of time; it is robust if its semantics is preserved when all timing constraints are relaxed by some small positive parameter.

We propose a construction which makes timed automata implementable in the above sense: From any timed automaton

A

, we build a timed automaton

A

′ that exhibits the same behaviour as

A

, and moreover

A

′ is both robust and samplable by construction.

An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are non-Zeno. Over the years important improvements have been obtained in checking reachability properties for timed automata. We show that some of these very efficient optimizations make testing for Zeno runs costly. In particular we show NP-completeness for the LU-extrapolation of Behrmann et al. We analyze the source of this complexity in detail and give general conditions on extrapolation operators that guarantee a (low) polynomial complexity of Zenoness checking. We propose a slight weakening of the LU-extrapolation that satisfies these conditions.

Probabilistic automata (PA) [20] have been successfully applied in the formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on PCTL [11] and its extension PCTL

*

[4]. Various behavioral equivalences are proposed for PAs, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the behavioral equivalences are well-known to be strictly stronger than the logical equivalences induced by PCTL or PCTL

*

. This paper introduces novel notions of strong bisimulation relations, which characterizes PCTL and PCTL

*

exactly. We also extend weak bisimulations characterizing PCTL and PCTL

*

without next operator, respectively. Thus, our paper bridges the gap between logical and behavioral equivalences in this setting.

Probabilistic nondeterministic processes are commonly modeled as probabilistic LTSs (PLTSs, a.k.a. probabilistic automata). A number of logical characterizations of the main behavioral relations on PLTSs have been studied. In particular, Parma and Segala [2007] define a probabilistic Hennessy-Milner logic interpreted over distributions, whose logical equivalence/preorder when restricted to Dirac distributions coincide with standard bisimulation/simulation between the states of a PLTS. This result is here extended by studying the full logical equivalence/preorder between distributions in terms of a notion of bisimulation/simulation defined on a LTS of probability distributions (DLTS). We show that the standard spectrum of behavioral relations on nonprobabilistic LTSs as well as its logical characterization in terms of Hennessy-Milner logic scales to the probabilistic setting when considering DLTSs.

We study long run average behavior of generalized semi-Markov processes with both fixed-delay events as well as variable-delay events. We show that allowing two fixed-delay events and one variable-delay event may cause an unstable behavior of a GSMP. In particular, we show that a frequency of a given state may not be defined for almost all runs (or more generally, an invariant measure may not exist). We use this observation to disprove several results from literature. Next we study GSMP with at most one fixed-delay event combined with an arbitrary number of variable-delay events. We prove that such a GSMP always possesses an invariant measure which means that the frequencies of states are always well defined and we provide algorithms for approximation of these frequencies. Additionally, we show that the positive results remain valid even if we allow an arbitrary number of reasonably restricted fixed-delay events.

Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout large-scale networks. In this paper, we propose a compositional analysis technique to study formal probabilistic models of gossip protocols in the context of wireless sensor networks. We introduce a simple probabilistic timed process calculus for modelling wireless sensor networks. A simulation theory is developed to compare probabilistic protocols that have similar behaviour up to a certain probability. This theory is used to prove a number of algebraic laws which revealed to be very effective to evaluate the performances of gossip networks with and without communication collisions.

We develop a general framework for the specification and implementation of systems whose executions are words, or partial orders, over an infinite alphabet. As a model of an implementation, we introduce class register automata, a one-way automata model over words with multiple data values. Our model combines register automata and class memory automata. It has natural interpretations. In particular, it captures communicating automata with an unbounded number of processes, whose semantics can be described as a set of (dynamic) message sequence charts. On the specification side, we provide a local existential monadic second-order logic that does not impose any restriction on the number of variables. We study the realizability problem and show that every formula from that logic can be effectively, and in elementary time, translated into an equivalent class register automaton.

Checking language inclusion between two nondeterministic Büchi automata

$\mathcal A$

and

$\mathcal B$

is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the

Ramsey-based approach

. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on

$\mathcal A$

and

$\mathcal B$

, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on

$\mathcal A$

and

$\mathcal B$

. (2) A method to additionally use forward simulation

between

$\mathcal A$

and

$\mathcal B$

. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from real-world model checking benchmarks, and on the Tabakov-Vardi random model, thus showing the usefulness of the proposed techniques.

A multi-stack pushdown system is a natural model of concurrent programs. The basic verification problems are in general undecidable (two stacks suffice to encode a Turing machine), and in the last years, there have been some successful approaches based on under-approximating the system behaviors. In this paper, we propose a restriction of the semantics of the general model such that a symbol that is pushed onto a stack can be popped only within a bounded number of context-switches. Note that, we allow runs to be formed of unboundedly many execution contexts, we just bound the scope (in terms of number of contexts) of matching push and pop transitions. We call the resulting model a

multi-stack pushdown system with scope-bounded matching relations

(

SMpds

). We show that the configuration reachability and the location reachability problems for

SMpds

are both

Pspace

-complete, and that the set of the reachable configurations is regular, in the sense that there exists a multi-tape finite automaton that accepts it.

When defining the semantics of shared-memory concurrent programming languages, one conventionally has to make assumptions about the atomicity of actions such as assignments. Running on physical hardware, these assumptions can fail to hold in practice, which puts in question reasoning about their concurrent execution. We address an observation, due to John Reynolds, that processes proved sound in concurrent separation logic are separated to an extent that these assumptions can be disregarded, so judgements remain sound even if the assumptions on atomicity fail to hold. We make use of a Petri-net based semantics for concurrent separation logic with explicit representations of the key notions of ownership and interference. A new characterization of the separation of processes is given and is shown to be stronger than existing race-freedom results for the logic. Exploiting this, sufficient criteria are then established for an operation of refinement of processes capable of changing the atomicity of assignments.

In 2004, Berdine, Calcagno and O’Hearn introduced a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. They showed that entailment in this fragment is in coNP, but the precise complexity of this problem has been open since. In this paper, we show that the problem can actually be solved in polynomial time. To this end, we represent separation logic formulae as graphs and show that every satisfiable formula is equivalent to one whose graph is in a particular normal form. Entailment between two such formulae then reduces to a graph homomorphism problem. We also discuss natural syntactic extensions that render entailment intractable.

This paper studies algebraic models for concurrency, in light of recent work on Concurrent Kleene Algebra and Separation Logic. It establishes a strong connection between the Concurrency and Frame Rules of Separation Logic and a variant of the exchange law of Category Theory. We investigate two standard models: one uses sets of traces, and the other is state-based, using assertions and weakest preconditions. We relate the latter to standard models of the heap as a partial function. We exploit the power of algebra to unify models and classify their variations.

A large variety of process calculi extend the

π

-calculus with more general notions of messages. Bengtson et al. have shown that many of these

π

-like calculi can be expressed as so-called

ψ

-calculi. In this paper, we describe a simple type system for

ψ

-calculi. The type system satisfies a subject reduction property and a general notion of channel safety. A number of existing systems are shown to be instances of our system, and other, new type systems can also be obtained. We first present a new type system for the calculus of explicit fusions by Wischik and Gardner, then one for the distributed

π

-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and shown to be safe.

We introduce a concise pi-calculus with directed choices and develop a theory of subtyping. Built on a simple behavioural intuition, the calculus offers exact semantic analysis of the extant notions of subtyping in functional programming languages and session-based programming languages. After illustrating the idea of subtyping through examples, we show type-directed embeddings of two known subtyped calculi, one for functions and another for session-based communications. In both cases, the behavioural content of the original subtyping is precisely captured in the fine-grained subtyping theory in the pi-calculus. We then establish full abstraction of these embeddings with respect to their standard semantics, Morris’s contextual congruence in the case of the functional calculus and testing equivalence for the concurrent calculus. For the full abstraction of the embedding of the session-based calculus, we introduce a new proof method centring on non-deterministic computational adequacy and definability. Partially suggested by a technique used by Quaglia and Walker for their full abstraction result, the new proof method extends the framework used in game-based semantics to the May/Must equivalences, giving a uniform proof method for both deterministic and non-deterministic languages.

We present in this paper a fine-grained rollback primitive for the higher-order

π

-calculus (HO

π

), that builds on the reversibility apparatus of reversible HO

π

[9]. The definition of a proper semantics for such a primitive is a surprisingly delicate matter because of the potential interferences between concurrent rollbacks. We define in this paper a high-level operational semantics which we prove sound and complete with respect to reversible HO

π

backward reduction. We also define a lower-level distributed semantics, which is closer to an actual implementation of the rollback primitive, and we prove it to be fully abstract with respect to the high-level semantics.

A quite flourishing research thread in the recent literature on component-based system is concerned with the algebraic properties of various kinds of connectors for defining well-engineered systems. In a recent paper, an algebra of stateless connectors was presented that consists of five kinds of basic connectors, plus their duals. The connectors can be composed in series or in parallel and employing a simple 1-state buffer they can model the coordination language Reo. Pawel Sobocinski employed essentially the same stateful extension of connector algebra to provide semantics-preserving mutual encoding with some sort of elementary Petri nets with boundaries. In this paper we show how the tile model can be used to extend Sobocinski’s approach to deal with P/T nets, thus paving the way towards more expressive connector models.

The reachability problem for vector addition systems is a central problem of net theory. This problem is known to be decidable but the complexity is still unknown. Whereas the problem is EXPSPACE-hard, no elementary upper bounds complexity are known. In this paper we consider the reversible reachability problem. This problem consists to decide if two configurations are reachable one from each other. We show that this problem is EXPSPACE-complete. As an application of the introduced materials we characterize the reversibility domains of a vector addition system.

A contextual net is a Petri net extended with read arcs, which allow transitions to check for tokens without consuming them. Contextual nets allow for better modelling of concurrent read access than Petri nets, and their unfoldings can be exponentially more compact than those of a corresponding Petri net. A constructive but abstract procedure for generating those unfoldings was proposed in earlier work; however, no concrete implementation existed. Here, we close this gap providing two concrete methods for computing contextual unfoldings, with a view to efficiency. We report on experiments carried out on a number of benchmarks. These show that not only are contextual unfoldings more compact than Petri net unfoldings, but they can be computed with the same or better efficiency, in particular with respect to the place-replication encoding of contextual nets into Petri nets.

We associate a graph with a 1-safe Petri net and study the parameterized complexity of various problems with parameters derived from the graph. With treewidth as the parameter, we give W[1]-hardness results for many problems about 1-safe Petri nets. As a corollary, this proves a conjecture of Downey et. al. about the hardness of some graph pebbling problems. We consider the parameter benefit depth (that is known to be helpful in getting better algorithms for general Petri nets) and again give W[1]-hardness results for various problems on 1-safe Petri nets.We also consider the stronger parameter vertex cover number. Combining the well known automata-theoretic method and a powerful fixed parameter tractability (

Fpt

) result about Integer Linear Programming, we give a Fpt algorithm for model checking Monadic Second Order (MSO) formulas on 1-safe Petri nets, with parameters vertex cover number and the size of the formula.

CCS

!

is a variant of CCS in which infinite behaviors are defined by the replication operator. We show that the reachability problem for CCS

!

is decidable by a reduction to the same problem for Petri Nets.

In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free through a static analysis of their syntax. In particular, we present a collection of rules, based on the inductive structure of terms, which guarantee livelock-freedom of the denoted process. This gives rise to an algorithm which conservatively flags processes that can potentially livelock. We illustrate our approach by applying both BDD-based and SAT-based implementations of our algorithm to a range of benchmarks, and show that our technique in general substantially outperforms the model checker FDR whilst exhibiting a low rate of inconclusive results.

State-transition systems communicating by shared variables have been the underlying model of choice for applications of model checking. Such formalisms, however, have difficulty with modeling process creation or death and communication reconfigurability. Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling formalism that supports dynamic reconfiguration and creation/death of processes. The resulting formalism supports two types of variables, data variables and reference variables. Reference variables enable changing the connectivity between processes and referring to instances of processes. We show how this new formalism supports parallel composition and refinement through trace containment. DRM provide a natural language for modeling (and ultimately reasoning about) biological systems and multiple threads communicating through shared variables.

We revisit the complexity of the model checking problem for formulas of linear-time temporal logic (LTL). We show that the classic PSPACE-hardness result is actually limited to a subclass of the Kripke frames, which is characterized by a simple structural condition: the model checking problem is only PSPACE-hard if there exists a strongly connected component with two distinct cycles. If no such component exists, the problem is in

coNP

. If, additionally, the model checking problem can be decomposed into a polynomial number of finite path checking problems, for example if the frame is a tree or a directed graph with constant depth, or the frame has an SCC graph of constant depth, then the complexity reduces further to

NC

.

Pushdown systems (PDS) are well adapted to model sequential programs with (possibly recursive) procedure calls. Therefore, it is important to have efficient model checking algorithms for PDSs. We consider in this paper CTL model checking for PDSs. We consider the “standard” CTL model checking problem where whether a configuration of a PDS satisfies an atomic proposition or not depends only on the control state of the configuration. We consider also CTL model checking with regular valuations, where the set of configurations in which an atomic proposition holds is a regular language. We reduce these problems to the emptiness problem in Alternating Büchi Pushdown Systems, and we give an algorithm to solve this emptiness problem. Our algorithms are more efficient than the other existing algorithms for CTL model checking for PDSs in the literature. We implemented our techniques in a tool, and we applied it to different case studies. Our results are encouraging. In particular, we were able to find bugs in linux source code.

The problem of model checking threads interacting purely via the standard synchronization primitives is key for many concurrent program analyses, particularly dataflow analysis. Unfortunately, it is undecidable even for the most commonly used synchronization primitive, i.e., mutex locks. Lock usage in concurrent programs can be characterized in terms of lock chains, where a sequence of mutex locks is said to be chained if the scopes of adjacent (non-nested) mutexes overlap. Although the model checking problem for fragments of Linear Temporal Logic (LTL) is known to be decidable for threads interacting via nested locks, i.e., chains of length one, these techniques don’t extend to programs with non-nested locks used in crucial applications like databases. We exploit the fact that lock usage patterns in real life programs do not produce unbounded lock chains. For such a framework, we show, by using the new concept of Lock Causality Automata (LCA), that

pre

*

-closures of regular sets of states can be computed efficiently. Leveraging this new technique then allows us to formulate decision procedures for model checking threads communicating via bounded lock chains for fragments of LTL. Our new results narrow the decidability gap for LTL model checking of threads communicating via locks by providing a more refined characterization for it in terms of boundedness of lock chains rather than the current state-of-the-art, i.e., nestedness of locks (chains of length one).

We propose an extension to

ATL

(

alternating-time logic

), called

BSIL

(

basic strategy-interaction logic

), for the specification of interaction among the strategies of agents in a multi-agent system. BSIL allows for the specifications of one system strategy that can cooperate with several strategies of the environment for different requirements. We argue that such properties are important in practice and rigorously show that such properties are not expressible in

ATL

*

,

GL

(

game logic

), and

AMC

(

alternating μ-calculus

). Specifically, we show that BSIL is more expressive than ATL but incomparable with ATL

*

, GL, and AMC in expressiveness. We show that a memoryful strategy is necessary for fulfilling a specification in BSIL. We also show that the model-checking problem of BSIL is PSPACE-complete and is of lower complexity than those of ATL

*

, GL, AMC, and the general strategy logics. This may imply that BSIL can be useful in closing the gap between real-world projects and the game-theoretical results. We then show the plausibility and feasibility of our techniques by reporting our implementation and experiment with our PSPACE model-checking algorithm for BSIL. Finally, we discuss an extension of BSIL.

We study the computational complexity of Nash equilibria in concurrent games with limit-average objectives. In particular, we prove that the existence of a Nash equilibrium in randomised strategies is undecidable, while the existence of a Nash equilibrium in pure strategies is decidable, even if we put a constraint on the payoff of the equilibrium. Our undecidability result holds even for a restricted class of concurrent games, where nonzero rewards occur only on terminal states. Moreover, we show that the constrained existence problem is undecidable not only for concurrent games but for turn-based games with the same restriction on rewards. Finally, we prove that the constrained existence problem for Nash equilibria in (pure or randomised) stationary strategies is decidable and analyse its complexity.

Verification tasks have non-elementary complexity for properties of linear traces specified in first-order logic, and thus various limited logical languages are employed. In this paper we consider two restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO

2

). LTL is more expressive, but FO

2

is often more succinct, and hence it is not clear which should be easier to verify. In this paper we take a comprehensive look at the issue, giving a comparison of verification problems for FO

2

, LTL, and the subset of LTL expressively equivalent to FO

2

, unary temporal logic (UTL). We give two logic-to-automata translations which can be used to give upper bounds for FO

2

and UTL; we apply these to get new bounds for both non-deterministic systems (hierarchical and recursive state machines, games) and for probabilistic systems (Markov chains, recursive Markov chains, and Markov decision processes). We couple this with lower-bound arguments for FO

2

and UTL. Our results give both a unified approach to understanding the behavior of FO

2

and UTL, along with a nearly comprehensive picture of the complexity of verification for these logics.

Given a system

$\mathcal{A}$

and objective Φ, the general task of controller synthesis is to design a decision making policy that ensures Φ to be satisfied. This paper deals with LTS-like system models and controllers that make their decisions based on the observables of the actions performed so far. Our main contribution is a compositional framework for treating multiple linear-time objectives inductively. For this purpose, we introduce a novel notion of strategies that serve as generators for observation-based decision functions. Our compositional approach will rely on most general (i.e., most permissive) strategies generating

all

decision functions that guarantee the objective under consideration. Finally we show that for safety and co-safety objectives Φ, most general strategies are realizable by finite-state controllers that exogenously enforce Φ.

We investigate normed commutative context-free processes (Basic Parallel Processes). We show that branching bisimilarity admits the

small response property

: in the Bisimulation Game, Duplicator always has a response leading to a process of size linearly bounded with respect to the Spoiler’s process. The linear bound is effective, which leads to decidability of branching bisimilarity. For weak bisimilarity, we are able merely to show existence of some linear bound, which is not sufficient for decidability. We conjecture however that the same effective bound holds for weak bisimilarity as well. We believe that further elaboration of novel techniques developed in this paper may be sufficient to demonstrate decidability.

In his seminal paper, R. Mayr introduced the well-known Process Rewrite Systems (PRS) hierarchy, which contains many well-studied classes of infinite systems including pushdown systems, Petri nets and PA-processes. A seperate development in the term rewriting community introduced the notion of Ground Tree Rewrite Systems (GTRS), which is a model that strictly extends pushdown systems while still enjoying desirable decidable properties. There have been striking similarities between the verification problems that have been shown decidable (and undecidable) over GTRS and over models in the PRS hierarchy such as PA and PAD processes. It is open to what extent PRS and GTRS are connected in terms of their expressive power. In this paper we pinpoint the exact connection between GTRS and models in the PRS hierarchy in terms of their expressive power with respect to strong, weak, and branching bisimulation. Among others, this connection allows us to give new insights into the decidability results for subclasses of PRS, e.g., simpler proofs of known decidability results of verifications problems on PAD.