Aiswarya Cyriac
email: cyriac@lsv.ens-cachan.fr

Paul Gastin
email: gastin@lsv.ens-cachan.fr

K Narayan Kumar

Verifying Communicating Multi-pushdown Systems

Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. Hence their verification problems are undecidable in general. The behaviours of these systems can be represented as directed graphs, which subsume both Message Sequence Charts and nested words. We extend the notion of split-width [8] to these graphs, defining a simple algebra to compose/decompose these behaviours using two natural operations: shuffle and merge. We obtain simple, uniform and optimal decision procedures for various verification problems parametrized by split-width, ranging from reachability to model-checking against MSO, PDL and Temporal Logics.

Introduction

Networks of multi-threaded recursive programs communicating via reliable unbounded channels are ubiquitous and their verification is as crucial as it is challenging. Recent researches have developed several approximation techniques for the verification of multi-threaded recursive programs (abstracted as multi-pushdown systems) and communicating machines. We continue this line of research. We propose a more general and unifying formalism for their modelling and consider various verification problems including reachability and model checking against logical specifications.

Towards getting a general formalism, we introduce a simple system model, Concurrent Processes with Store (CPS), which abstract the various data-structures (stacks for recursion and queues for channels) appearing in the system by a simple global store. A program in the system may write to the global store or read a value from the global store. Reads are destructive, as this is the case with stacks (pops) and queues (dequeue).

The behaviour of a CPS will be a tuple of sequences of events (one per program/process). In addition a binary matching relation links corresponding writes and reads. Such a graph is called a Concurrent Behaviour with Matching (CBM).

The matching relation can be further refined to retrieve the case when the store consists of several stacks and queues. The system model in this case is called CPSQ (Concurrent Processes with Stacks and Queues) and the behaviours are called MSCN (Message Sequence Charts with Nestings), which generalize nested words [START_REF] Alur | Adding nesting structure to words[END_REF], multiply nested words [START_REF] La | A robust class of context-sensitive languages[END_REF], Message Sequence Charts [START_REF]Message Sequence Chart (MSC)[END_REF] and stack-queue graphs [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF]. For specifying their properties, we consider Monadic Second Order logic (MSO), Propositional Dynamic Logic with and without intersection (IPDL/PDL) and Temporal Logics (TL).

We show that the reachability problem for CPS is decidable, though with high complexity. It is infact equivalent to reachability in Petri-nets/VAS. Model checking and satisfiability of PDL without intersection is also shown to be decidable. All other problems for CPS/CBM turns out to be undecidable. Moreover, all the verification problems are undecidable for CPSQ/MSCN. However, the verification of these systems is an important concern. Hence, we consider upper-approximate verification. We extend the technique of split-width to cope with CPS/CPSQ. Split-width was introduced in [START_REF] Cyriac | MSO decidability of multipushdown systems via split-width[END_REF] for getting decidability for MSO model checking of multi-pushdown systems.

Split-width is based on a simple and intuitive algebra which generates CBMs. We first generalize CBMs to split-CBMs which are CBMs with holes. The holes may be seen as place holders where an actual behaviour may be inserted later. Our algebra is over split-CBMs. The atomic elements are (i) the single matching edge relating a write and the corresponding read and (ii) a single internal event. The shuffle operator lets us combine two split-CBMs by inserting parts of one into the holes of the other (and vice-versa). The merge operator allows us to close some of the holes in a split-CBM. Every CBM can be generated from the atomic ones using these two operations. split-CBM is the number of holes it has. We say that a CBM has split-width k if it can be generated by this algebra in such a way that each split-CBM obtained in any intermediate step has at most k holes. We call a term in this algebra a split-term.

The algebra allows us to recursively divide a CBM into independent parts which can be reasoned about separately. Thus, it provides a divide-and-conquer approach (or compositional reasoning) for the analysis of a behaviour. Note that, two events linked by a matching read-write are never separated in this algebra. The algebra also gives a natural embedding of CBMs into trees via split-terms, similar to how parse trees give a tree-representation for a word in a context-free language.

The valid tree-embeddings of CBMs with split-width at most k form a regular tree-language. Thus we can translate every problem on CBM/CPS to an equivalent one on tree-domain. With split-width as a parameter, we get uniform decision procedures with optimal complexities for all verification problems on CBM/CPS as well as MSCN/CPSQ. The complexities range from non-elementary for MSO to 2ExpTime for IPDL to ExpTime for PDL/TL to PTime for reachability.

The simple notion of split-width, while giving us uniform and optimal decision procedures for a wide range of verification problems, is also very powerful. In [START_REF] Cyriac | MSO decidability of multipushdown systems via split-width[END_REF][START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF] a bound on split-width is established for many behaviour restrictions for which decidability of reachability was known before, e.g., for multi-pushdown systems having a bound on context [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF], scope [START_REF] La | Reachability of multistack pushdown systems with scope-bounded matching relations[END_REF], phase [START_REF] La | A robust class of context-sensitive languages[END_REF], ordered [START_REF] Breveglieri | Multi-pushdown languages and grammars[END_REF][START_REF] Faouzi Atig | Emptiness of multipushdown automata is 2ETIME-Complete[END_REF] and for communicating pushdown systems over acyclic topologies [START_REF] Heußner | Reachability analysis of communicating pushdown systems[END_REF]. The systematic way of bounding the split-width also helped us to generalise these restrictions and to discover several new decidable classes.

In [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF] it is further shown that a class of CBMs has bounded split-width if and only if it has bounded clique-width, and the corresponding bounds lie in a linear factor. Thus, by Courcelle's results, if a class of CBMs have a decidable MSO theory, then it also has bounded split-width. Thus split-width is not only sufficient but also necessary for MSO decidability of CBMs.

Related work [START_REF] Heußner | Reachability analysis of communicating pushdown systems[END_REF] identifies topologies which give decidability of reachability for communicating pushdown systems. A unified proof of decidability of reachability of the known decidable restrictions (having a bound on context [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF], scope [START_REF] La | Reachability of multistack pushdown systems with scope-bounded matching relations[END_REF], phase [START_REF] La | A robust class of context-sensitive languages[END_REF], ordered [START_REF] Breveglieri | Multi-pushdown languages and grammars[END_REF][START_REF] Faouzi Atig | Emptiness of multipushdown automata is 2ETIME-Complete[END_REF] for multi-pushdown systems and communicating pushdown systems over acyclic topologies) is given in [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF] via demonstrating their bounded tree-width. An abstract representation of these tree-decompositions is studied in [START_REF] Inverso | Looking at computations from a different angle[END_REF]. Reachability in acyclic networks of pushdown systems connected via lossy FIFO channels is considered in [START_REF] Faouzi | On the reachability analysis of acyclic networks of pushdown systems[END_REF].

Concurrent Behaviours with Matching (CBM)

Let Procs = {1, . . . , p} be a finite set of processes and Σ be a finite set of actions. We are interested in systems of concurrent processes with data structures such as queues, stacks, bags etc. With such data structures, a write action adds a value to the store, while a read action removes a value from it. We describe a behaviour of such a system as a tuple of sequences of actions (one for each process) enriched with a relation matching write events to their corresponding read events. Thus an action can be part of at most one matching edge. Furthermore, since writes must precede reads, the resulting graph is a partial order. Definition 1. A concurrent behaviour with matching (abbraviated as CBM) over an alphabet Σ and a set Procs of processes is a tuple M = (E, λ, pid, →, ⊲) where -E is a non-empty finite set of events, -λ : E → Σ labels each event with an action, -pid : E → Procs assigns a process to each event, -→ ⊆ p∈Procs pid -1 (p) × pid -1 (p) describes the linear orders on processes:

for each process p ∈ Procs, the restriction of → to the events of process p is the direct-successor relation of some total order on pid -1 (p),

-⊲ ⊆ E × E is the relation matching write events with their corresponding read events: it is irreflexive and disjoint, i.e., if e 1 ⊲ e 2 then e 1 = e 2 and two distinct edges e 1 ⊲ e 2 and e 3 ⊲ e 4 must be disjoint (|{e 1 , e 2 , e 3 , e 4 }| = 4), -The underlying graph (E, (→ ∪ ⊲) * ) is a partial order.

The set of all CBMs over Procs and Σ is denoted CBM(Procs, Σ). Notice that, the definition of CBMs does not involve any specific data-structures such as queues or stacks. However, the ⊲ edges may be thought of as those arising from a global store shared by all processes. Observe that the underlying graph has no cycles. Notice also that the ⊲ edges do not follow any LIFO or FIFO policy.

In the following, an event which is the source (resp. the target) of a ⊲ edge is called a write event (resp. read event), and all other are called internal events.

Stacks and Queues To model behaviours of concurrent recursive multithreaded programs communicating via FIFO channels, we will consider restrictions of CBMs called Message Sequence Charts with Nestings (MSCNs) that subsume stack-queue graphs [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF]. They are obtained by assuming that the global store shared by all processes is actually composed of disjoint data structures that are either stacks or queues. So we consider a finite set DS = Stacks ⊎ Queues of data-structure labels. The read and write accesses are specified by mappings Writer : DS → Procs and Reader : DS → Procs. We restrict to self-stacks, i.e., for all d ∈ Stacks we have Writer(d) = Reader(d). We define an architecture to be a tuple A = (Procs, Stacks, Queues, Writer, Reader).

An MSCN is a CBM in which events accessing the store will be additionally labeled with a data-structure and the matching relation is restricted so that it complies with the with LIFO or FIFO policies.

Definition 2. An MSCN over architecture A and alphabet

Σ is a tuple M = (E, λ, pid, δ, →, ⊲) where M = (E, λ, pid, →, ⊲) is a CBM and δ : E → DS is a partial map satisfying -dom(δ) = {e ∈ E | e ⊲ f or f ⊲ e for some f ∈ E}, -If e ⊲ f , then δ(e) = δ(f ), Writer(δ(e)) = pid(e) and Reader(δ(f )) = pid(f ). -For each d ∈ Stacks, ⊲ d = ⊲ ∩ (δ -1 (d)) 2 conforms to LIFO: if e 1 ⊲ d f 1 and e 2 ⊲ d f 2 are different edges then we do not have e 1 → + e 2 → + f 1 → + f 2 . -For each d ∈ Queues, ⊲ d = ⊲ ∩ (δ -1 (d)) 2 conforms to FIFO: if e 1 ⊲ d f 1
and e 2 ⊲ d f 2 are different message edges then we do not have e 1 → + e 2 and f 2 → + f 1 .

We denote by MSCN(A, Σ) the set of MSCNs over architecture A and action labels Σ.

Example 2. An MSCN is shown in Fig. 2. The data-structures consist of one stack on process 1, two stacks on process 2 (one using solid arrows and the other dashed arrows) and one queue from process 2 to process 1. For readability, we do not include the DS labels to the events, they can be recovered from the various matching edges.

When data structures are queues between pairs of processes, MSCNs extend message sequence charts which are scenarios standardised by ITU [START_REF]Message Sequence Chart (MSC)[END_REF]. When on the other hand there is a single process and our data structures are stacks, our setting extends nested words [START_REF] Alur | Adding nesting structure to words[END_REF] and multiply nested words [START_REF] La | A robust class of context-sensitive languages[END_REF].

Concurrent Processes with Store (CPS)

We now describe a system model whose behaviours are CBMs. It consists of a set of finite state processes which share a single store data-structure. The store is just an unordered multi-set of unbounded size supporting two actions -add a value and remove a value. The intended operational semantics is the following. A write transition of the form (ℓ 1 , a, ℓ 2 , ℓ) results in process p performing an action labeled a while moving from location ℓ 1 to ℓ 2 and inserting value ℓ into the store. A read transition of the form (ℓ 1 , ℓ, a, ℓ 2 ) results in process p performing an action labeled a whilst consuming a value ℓ from the store and moving from ℓ 1 to ℓ 2 .

As is well known in concurrency theory, it is also possible to provide the semantics of such systems directly on a partially ordered structure that represents the causal relationship between the events in the execution. For a CPS, the appropriate structure is that of CBMs, where the relation ⊲ relates the insertion of a value into the store and its corresponding consumption. It is easy to provide an equivalent operational semantics (see [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF]).

We now define the notion of a run of a CPS over a CBM. Such a run labels the events of a CBM with the control locations of the CPS. This is given by the control location labeling ρ : E → Locs. Further, in order to keep track of the values in the store, a run also labels write events by the value that was added to the store. This is specified by a partial data mapping ν : E → Locs such that e ∈ dom(ν) iff e is a write event.

A run of a CPS S= (Locs, (Trans p ) p∈Procs , ℓ in , Locs fin ) over a CBM M = (E, λ, pid, →, ⊲) is a pair (ρ, ν) such that the following additional consistency conditions hold for all e ∈ E. We denote by e -, the unique event such that e -→ e if it exists, and otherwise e -= ⊥ pid(e) / ∈ E. We set ρ(⊥ p ) = ℓ in as a convention.

1. if e ⊲ f then (ρ(e -), λ(e), ρ(e), ν(e)) ∈ Trans pid(e)! , 2. if f ⊲ e then (ρ(e -), ν(f ), λ(e), ρ(e)) ∈ Trans pid(e)? , 3. if e is internal then (ρ(e -), λ(e), ρ(e)) ∈ Trans pid(e),i .

Let f p denote the maximal event on process p if it exists. Otherwise, we set

f p = ⊥ p / ∈ E (recall that ρ(⊥ p ) = ℓ in ). A run is accepting if (ρ(f 1 ), . . . , ρ(f p )) ∈ Locs fin .
The language accepted by a CPS S is the set of CBMs on which it has an accepting run. We denote it by L (S).

Stacks and Queues Let A = (Procs, Stacks, Queues, Writer, Reader) be an architecture. When operating over A, the transitions of a CPS are refined into Trans p! = d∈Writer -1 (p) Trans p!d and Trans p? = d∈Reader -1 (p) Trans p?d .

For the operational semantics, the store is split into stacks and queues whose contents are words in Locs * . A write transition (ℓ 1 , a, ℓ 2 , ℓ) ∈ Trans p!d adds the value ℓ on the right of the word holding the contents of data-structure d. A read transition (ℓ 1 , ℓ, a, ℓ 2 ) ∈ Trans p?d removes the value ℓ on the left (resp. right) of the word for queue (resp. stack) d.

The modification is even easier for runs defined over an MSCN. We only have to change the conditions above for the write and read transitions to:

1. if e ⊲ d f then (ρ(e -), λ(e), ρ(e), ν(e)) ∈ Trans pid(e)!d , 2. if f ⊲ d e then (ρ(e -), ν(f ), λ(e), ρ(e)) ∈ Trans pid(e)?d .

A CPS S over an architecture A is called a system of concurrent processes with stacks and queues (CPSQ). It defines the language L MSCN (S) of MSCNs in MSCN(A, Σ) admitting an accepting run.

Specification formalisms

We now describe three classical logical formalisms that will be used for specifying properties of CBMs. We only give their syntax and intuitive semantics here.

Monadic Second Order Logic over CBM(Procs, Σ) is denoted MSO(Procs, Σ). Its syntax is given below, where p ∈ Procs and a ∈ Σ.

ϕ ::= a(x) | p(x) | x = y | x ∈ X | x → y | x ⊲ y | ϕ ∨ ϕ | ¬ϕ | ∃x ϕ | ∃X ϕ
Every sentence in MSO defines a language of CBMs consisting of all those that satisfy that sentence. As is well known, monadic second-order quantifiers can be used to express transitive closures -that is, for each MSO formula ϕ(x, y) defining a relation R over its domain, one can construct another formula ϕ * (x, y) which defines the transitive closure of R. Thus, the predicates ≤ and ≤ p , denoting transitive closures of (⊲ ∪ →) and → respectively, are MSO(Procs, Σ) definable.

The formula ∀x∀y.a(x) =⇒ (x ≤ y) ∨ (y ≤ x) asserts that events labeled a cannot occur concurrently to some other event. The formula

∀x∀y.(x ≤ p y ∧ x ⊲ y) =⇒ ¬∃z.(x ≤ p z ∧ z ≤ p y ∧ b(z))
prohibits, in any process, occurrence of b events from the point a value is inserted into the store to the point it is taken back.

Remark 1. The language of a CPS S over Procs and Σ can be described in MSO(Procs, Σ). We use second order variables {X ℓ } ℓ∈Locs to identify the ρ mapping and {Y ℓ } ℓ∈Locs to identify the ν mapping and the rest of the formula asserts that the second order variable assignment identifies a valid run of the CPS.

This generous expressive power of MSO comes at a cost -in general, satisfiability and model-checking are undecidable and even for decidable fragments the decision procedures have non-elementary complexity. Therefore we examine less expressive logics with reasonable decision procedures.

Propositional Dynamic Logic (PDL) A well-studied logical formalism for describing properties of programs is that of PDL, a generalization of modal logic. As in a modal logic, formulas in PDL assert properties of nodes in a graph, in our case events in a CBM. Unlike a modal logic where modal operators only refer to neighbours of the current node, PDL uses path modalities to assert properties on nodes reachable via paths conforming to some regular expressions. Traditionally, PDL is used to express branching-time properties of transition systems (or kripke structures). However, in the study of concurrent systems where each behaviour has a graph-like structure, PDL may be used to express properties of behaviours (i.e., linear-time properties of the system under consideration) as illustrated in [START_REF] Jesper | Dynamic linear time temporal logic[END_REF][START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF][START_REF] Bollig | Propositional dynamic logic for messagepassing systems[END_REF]. PDL and its extensions with converse and intersection are studied in this sense, as linear-time logics, here. The syntax of state formulas (σ) and path formulas (π) of ICPDL(Procs, Σ) are given by

σ ::= ⊤ | p | a | σ ∨ σ | ¬σ | π σ π ::= σ | → | ⊲ | → -1 | ⊲ -1 | π + π | π ∩ π | π • π | π *
where p ∈ Procs and a ∈ Σ. If backward edges → -1 and ⊲ -1 are not allowed the fragment is called PDL with intersection (IPDL). If intersection π ∩ π is not allowed, the fragment is PDL with converse (CPDL). The basic PDL is when neither backwards edges nor intersection are allowed.

The formula p asserts that current event belongs to process p while a asserts that it is labeled by a. The formula π σ at e asserts the existence of an e ′ satisfying σ and a path e = e 1 , e 2 , . . . , e k = e ′ that conforms to π. The only paths that conform to σ are the trivial paths from e to e for any e that satisfies σ. Similarly → and ⊲ identify pairs related by the corresponding edge relation in the CBM. Finally •, + and * correspond to composition, union and iteration of paths as in regular expressions.

The formula → * α asserts that α holds at some future event on the same process while the formula (β • → -1 ) * α asserts that, β has been true at all the events in the current process since the last event (on this process) that satisfied α.

Intersection of path expressions is a powerful feature. The formula π 1 ∩ π 2 α at an event e asserts the existence of an e ′ satisfying α, a path from e to e ′ conforming to π 1 and a path from e to e ′ conforming to π 2 . For instance, the formula ⊲ ∩ (→ * • b • → * ) true is true at an event e only if there is an e ′ with e ⊲ e ′ on the same process and b holds somewhere between e and e ′ (on this process).

Observe that PDL formulas have implicit free variables. To define languages of CBMs with PDL we introduce sentences φ of ICPDL(Procs, Σ) with the following syntax:

φ = ⊤ | E σ | φ ∨ φ | ¬φ where σ is an ICPDL(Procs, Σ) state formula. The sentence E σ is true on CBM M if M, e |= σ for some event e of M. With this interpretation the formula ¬ E ⊲ ∩ (→ * • b • → * )
true is equivalent to the second MSO property written above.

Temporal Logics Another reason to study PDL over CBMs is that it naturally subsumes an entire family of temporal logics. The classical linear time temporal logic (LTL) is interpreted over discrete linear orders and comes with two basic temporal operators: the next state (Xϕ) which asserts the truth of ϕ at the next position and the until (ϕ 1 U ϕ 2 ) which asserts the existence of some future position where ϕ 2 holds such that ϕ 1 holds everywhere in between. In the setting of CBMs, following [START_REF] Jesper | Dynamic linear time temporal logic[END_REF], it is profitable to extend this to a whole family of temporal operators by parametrizing the steps used by next and until with path expressions. Despite of their differing expressive powers, they can all be translated into PDL uniformly.

The syntax of local temporal logics TL(Procs, Σ) is as follows, where a ∈ Σ, p ∈ Procs and π is a path expression:

ϕ = a | p | ¬ϕ | ϕ ∨ ϕ | X π ϕ | ϕ U π ϕ
For example, ϕ U π ψ asks for the existence of a sequence of events related by π-steps and such that ψ holds at the last event of the sequence and ϕ holds at intervening events in the sequence. The translation in PDL gives (Φ • π) * Ψ , where Φ and Ψ are the PDL translations of ϕ and ψ respectively. When π is → it corresponds to the classical until along a process, and when π is → + ⊲ it corresponds to an existential until in the partial order of the CBM. We may also use backward steps such as → -1 or → -1 + ⊲ -1 and thus TL(Procs, Σ) has both future and past modalities.

Stacks and Queues

Let A = (Procs, Stacks, Queues, Writer, Reader) be an architecture. The logics above may be used to specify properties of MSCNs over (A, Σ). We provide the ability to talk about the data-structures by adding atomic formulas. For MSO logic, we add d(x), meaning that event x is labeled d ∈ DS. For PDL or TL, we simply add atomic propositions d ∈ DS to the syntax of state formulas. Then, every sentence of MSO(A, Σ), ICPDL(A, Σ) and TL(A, Σ) defines a language of MSCN(A, Σ).

Note that MSO logic or IPDL are powerful enough to express the LIFO or FIFO restrictions. More precisely, let

x ⊲ d x ′ = x ⊲ x ′ ∧ d(x) ∧ d(x ′ ).
The LIFO condition for data-structure d can be expressed with the MSO formula

¬∃x, x ′ , y, y ′ , x ⊲ d x ′ ∧ y ⊲ d y ′ ∧ x < y < x ′ < y ′ .
The same property is expressed by the IPDL formula

¬ E (⊲ d • → • (⊲ d • → + ¬ ⊲ d ⊤ • →) * ) ∩ (→ + • ⊲ d ) true
where the path expression ⊲ d stands for d • ⊲ • d.

Split concurrent behaviour with matching

Our analysis of CBMs via split-width will be based on a divide and conquer approach. More precisely, we will divide a CBM in smaller behaviours by splitting (cutting) some of the process (linear) edges so that the graph becomes disconnected. Such subgraphs are called split-CBMs. Once a CBM is split, a process may have several connected components and we relate them with elastic edges to remember the original ordering between them.

Example 3. The split-CBM M of Fig. 3 is obtained by splitting 5 process edges from the CBM M of Fig. 1, replacing them by elastic edges (wavy edges in the picture).

If we omit the elastic edges, this split-CBM is composed of 3 disconnected subgraphs which can be easily seen in Fig. 4. Hence, M can be divided into the two split-CBMs of Fig. 4. Notice that in these split-CBMs, we still include elastic edges allowing to recover the original ordering between events. Also, the split-CBM on the right of Fig. 4 can be further divided into two split-CBMs, one where only process 1 is active, the other where only process 2 is active. Stacks and Queues Indeed, this definition carries over to MSCNs: a split-MSCN over some architecture A is simply a tuple

M = (E, λ, pid, δ, r - →, e - →, ⊲) such that M = (E, λ, pid, δ, r - → ⊎ e - →, ⊲) is an MSCN over A.

Merge and Shuffle

We have motivated split-CBMs with a top-down divide and conquer approach: starting from a CBM, we split some process edges and then divide the graph in smaller split-CBMs that are no more connected. Dually, we may reconstruct bottom-up CBMs. The dual operation of divide is shuffle, it takes two split-CBMs and shuffles their components to get a single split-CBM. The dual for split is merge, it turns an elastic edge split-CBM into a rigid edge.

The merge operation may transform any of the elastic edges into a rigid one, though only one at a time. Hence merge(M) is a set of split-CBMs. Definition 5. Formally, let M = (E, λ, pid, r -→, e -→, ⊲) be a split-CBM. Then, merge(M) consists of the split-CBMs

M ′ = (E, λ, pid, r - → ′ , e - → ′ , ⊲) such that r - → ′ ⊎ e - → ′ = r - → ⊎ e - →, e - → ′ ⊆ e - → and | e - →| -| e - → ′ | = 1.
Notice that the number of components and the elasticity decrease by 1 as the result of a merge and that |merge(M)| = elasticity(M). For instance, the split-CBM M of Fig. 3 has 5 elastic edges, hence merge(M) consists of five split-CBMs, each of elasticity 4.

The binary shuffle operation, denoted ✁, when applied to two split-CBMs, gives a set of split-CBMs, obtained by shuffling on each process their components. For instance, the split-CBM of Fig. 3 belongs to the shuffle of the two split-CBMs of Fig. 4.

Definition 6. Let M i = (E i , λ i , pid i , r - → i , e - → i , ⊲ i ) for i ∈ {1, 2} be two split- CBMs with E 1 ∩ E 2 = ∅. Then, M 1 ✁ M 2 is the set of split-CBMs M = (E, λ, pid, r - →, e - →, ⊲) such that -apart from the elastic edges, M is the disjoint union of M 1 and M 2 , i.e., E = E 1 ⊎ E 2 , λ = λ 1 ⊎ λ 2 , pid = pid 1 ⊎ pid 2 , ⊲ = ⊲ 1 ⊎ ⊲ 2 and r - → = r - → 1 ⊎ r - → 2 ,
for each i, the order of the components of M i , as prescribed by the elastic edges

e - → i , is preserved in M: e - → 1 ∪ e - → 2 ⊆ ( r - → ∪ e - →) * .
Note that, two consecutive components in M i may either be still consecutive in M or may be separated by components from M 3-i . An elastic edge between two components of a split-CBM is a place holder where some other components may be inserted during a shuffle. If we decide that no more components should be inserted, the elastic edge can be replaced with a rigid edge using the merge operation.

Example 4. Considering again the two split-CBMs from Fig. 4, we can see that their shuffle contains 18 split-CBMs, one of which is presented in Fig. 3, two others are presented in Fig. 5. Note that, the number of components of any split-CBM M ∈ M 1 ✁ M 2 is the sum of the number of components in M 1 and the number of components in M 2 . We deduce that

elasticity(M) = elasticity(M 1 ) + elasticity(M 2 ) + |Procs(M 1 ) ∩ Procs(M 2 )| .
We can lift the definition of merge and shuffle to sets of split-CBMs in the natural way. Let L, L 1 and L 2 be sets of split-CBMs. We define

merge(L) = M∈L merge(M) (1)
L 1 ✁ L 2 = M1∈L1,M2∈L2 M 1 ✁ M 2 (2)
Stacks and Queues Again, merge and shuffle carry over to MSCNs by replacing split-CBMs by split-MSCNs in Def. 5 and Def. 6. Any elastic edge of a split-MSCN may be turned into a rigid edge with the merge operation. On the other hand, notice that, the shuffle operation of split-MSCNs is more restricted than for split-CBMs since the LIFO and FIFO policies of the data-structures must be respected.

An algebra over split-CBMs

We define an algebra which allows to reconstruct bottom-up (split)-CBMs from atomic ones (single events) using three very simple constructs: adding a matching edge between two events, shuffling two split-CBMs into a single one, or merging two consecutive components of a split-CBM into a single one. We describe a combination of these constructs with split-terms over (Procs, Σ) whose syntax is given by:

s ::= (a, p) | (a, p) ⊲ (a ′ , p ′ ) | merge(s) | s ✁ s
where a, a ′ ∈ Σ and p, p ′ ∈ Procs. Note that, in this algebra, the binary operator ⊲ may only be applied to atomic terms.

Each split-term s represents a set s of split-CBMs. This semantics is defined as follows:

-(a, p) is the CBM consisting of a single event labeled a on process p. -(a, p) ⊲ (a ′ , p ′ ) is the CBM consisting of two events, e labeled a on process p, and e ′ labeled a ′ on process p ′ . These events are connected by a matching edge: e ⊲ e ′ . Moreover, if p = p ′ , these two events are also linked by an elastic edge: e e -→ e ′ . -merge(s) = merge( s ) (cf. (1) in Sec. 6).

-

s 1 ✁ s 2 = s 1 ✁ s 2 (cf. (2) in Sec. 6).
Example 5. For instance, consider the split-term s = merge(((a, 1) ⊲ (b, 1)) ✁ (((b, 2) ⊲ (a, 1)) ✁ (a, 2))).

This term can be depicted as the following tree merge ✁ ⊲ (a, 1) (b, 1)

✁ ⊲ (b, 2) (a, 1) (a, 2)
and its semantics consists of 18 split-CBMs, two of which are given in Fig. 6. We can easily check that all the split-CBMs in the semantics s of a split-term s have the same set of non-empty processes, denoted Procs(s), the same number of components, hence also the same elasticity, donoted elasticity(s). We have The width of a split-term s, denoted swd(s), is the maximum elasticity of all its sub-terms. For instance, the elasticity of the split-term in Example 5 is two and its width is three.

-elasticity((a, p)) = 0, -elasticity((a, p) ⊲ (a ′ , p ′ )) = 0 if p = p ′ 1 if p = p
The split-width of a split-CBM M, denoted swd(M), is the minimum width of all split-terms s such that M ∈ s . For instance, both split-CBMs of Fig. 6 have split-width two since they are respectively in the semantics of s 1 = merge(((a, 1) ⊲ (b, 1)) ✁ ((b, 2) ⊲ (a, 1))) ✁ (a, 2) s 2 = ((a, 1) ⊲ (b, 1)) ✁ merge(((b, 2) ⊲ (a, 1)) ✁ (a, 2)).

We denote by k-CBM the set of split-CBMs whose split-width is bounded by k.

Remark 2. The split-width algebra over (Procs, Σ) can generate any CBM M = (E, λ, pid, →, ⊲) over (Procs, Σ). In fact a sequence of shuffles of basic split-terms will generate a split-CBM M 1 = (E, λ, pid, r -→ 1 = ∅, e -→ 1 = →, ⊲). This will then be followed by a sequence of merges to get the split-CBM

M 2 = (E, λ, pid, r - → 2 = →, e - → 2 = ∅, ⊲) = M.
Remark 3 (Split-width of Nested-Words). Nested words are MSCNs over an architecture with only one process and one stack. The split-width of any nestedword is at most two. This can be checked easily since a nested word is either the concatenation of two nested words, or of the form a w 1 b where w 1 is a nested word, or a basic nested word of the form a or a b .

Stacks and Queues Split-terms are easily extended to an architecture A by adding the data-structure label to terms denoting a matching edge: (a, p, d) ⊲ (a ′ , p ′ , d) means that data-structure d is accessed by the write event a on process p and the matching read event a ′ on process p ′ . The semantics of merge and shuffle is as above, restricting to MSCN(A, Σ).

Main Results

We are interested in various verification problems ( The same questions can be asked in the case of MSCNs as well (2',3',4',5'). The model checking problems on the other hand, check for the existence of a satisfying model in the language of a CPS [START_REF] Breveglieri | Multi-pushdown languages and grammars[END_REF][START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF][START_REF] Cyriac | MSO decidability of multipushdown systems via split-width[END_REF][START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] or respectively CPSQ (6',7',8',9'). As we will see soon, most of these problems are undecidable, and the decidable ones are of very high complexity. Hence we consider the parametrised (by split-width) version of the above problems (10-18, 10'-18'). The various verification problems are stated in Table 1. A main contribution of our paper is the decidability and complexity results of these problems:

Theorem 1. The decidability and complexity of the problems 1-18 and 1'-18' (Table 1) are as stated in Table 2.

In this section, we proceed to prove the results for problems (1-9) and (1'-9'). The results for the remaining problems are proved in the following sections.

First, we consider control state reachability or equivalently the (language) emptiness problem. For CPSQ the emptiness problem (1') is undecidable due to the presence of multiple stacks (and/or queues). The reachability problem for CPS (1) is equivalent to the reachability problem for vector addition systems (VAS) or Petri Nets, a problem whose decidability is known but highly non-trivial [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF][START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF].

Let L be a set of labels. A vector addition system V over L is a finite set of functions from the set {-1, 0, 1} L . Elements of V are called transitions. A marking of V is an element of N L .

We write v +w for the function defined as (v +w The reachability problem for VAS is the following: Given a VAS V and an initial marking u determine whether u -→ * 0 where 0 is the constant function returning 0. The reachability problem is known to be decidable [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF][START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF] but its precise complexity is not known.

)(i) = v(i)+w(i). A transition w is enabled at v if (v + w)(i) ≥ 0 for all i ∈ L. We write v w --→ v ′ for markings v, v ′ and a transition w ∈ V if w is enabled at v and v ′ = v + w. Let v - → v ′ if there is some w ∈ V such that v w --→ v ′ and
Remark 4. The classical definition of VAS permits transitions to come from the set Z L and further the reachability problem is often formulated as given u and v in N L whether u -→ * v. As is well known, as far as decidability goes, our version is equivalent to the general one.

As a first step we show that the emptiness problem for CPS can be reduced to the reachability problem for VAS.

Lemma 1. Given a CPS S = (Locs, (Trans p ) p∈Procs , ℓ in , Locs fin ) over the set of processes Procs and alphabet Σ, we can construct a VAS V S and an initial marking u ∈ V S such that the language of S is non-empty if and only if u -→ * 0.

Proof. Clearly, as far as the emptiness problem goes, one may assume that Σ is a singleton, by relabeling all transitions to use this single letter if necessary. So, we assume that Σ = {a} is singleton. V S is defined over the set of labels

L = Procs × Locs ⊎ Locs .
For each transition τ ∈ Trans p , we have an element v τ in V S given by

1. Case τ = (ℓ 1 , a, ℓ 2 ) ∈ Trans p,i : v τ (p, ℓ 1 ) = -1, v τ (p, ℓ 2 ) = 1 and v τ (x) = 0 for all other x ∈ L. 2. Case τ = (ℓ 1 , a, ℓ 3 , ℓ) ∈ Trans p! : v τ (p, ℓ 1 ) = -1, v τ (p, ℓ 2 ) = 1, v τ (ℓ) = 1 and v τ (x) = 0 for all other x ∈ L. 3. Case τ = (ℓ 1 , ℓ, a, ℓ 2 ): v τ (p, ℓ 1 ) = -1, v τ (p, ℓ 2 ) = 1, v τ (ℓ) = -1 and v τ (x) = 0
for all other x ∈ L.

In addition for each f = (f p ) p∈Procs ∈ Locs fin , we have a transition τ f given by 4) τ f (p, f p ) = -1 for p ∈ Procs and τ f (x) = 0 for all other x ∈ L.

We let u be the marking with u(p, ℓ in ) = 1 for all p ∈ Procs and u(x) = 0 for all other x ∈ L. Then, u -→ * 0 iff S accepts at least one CBM. ⊓ ⊔ Lemma 2. Let V be a VAS over the set of labels L and let u be a marking. Then there is a CPS S = (Locs, (Trans p ) p∈Procs , ℓ in , Locs fin ) with Procs = {p} a singleton and Σ = {a} a singleton such that u -→ * 0 if and only if the language of S is non-empty.

Proof. W.l.o.g we assume that u = 0. The idea is to use one location for each ℓ ∈ L and in the simulation keep c copies of ℓ in the store whenever the marking of the VAS assigns the value c to ℓ. Thus, to begin the simulation from the marking u we add we add u(ℓ) copies of ℓ to the store. Subsequently, each transition v is simulated using |L| transitions, one transition to modify the store content of each ℓ ∈ L as specified in v.

Let ≤ L be some linear order on L, ⋖ L be the covering relation of this linear order and let b and e be the minimum and maximum elements under ≤ L . The state space is

Locs = {(ℓ, i) | ℓ ∈ L, i ≤ u(ℓ)} ⊎ {(v, ℓ) | v ∈ V, ℓ ∈ L} ⊎ L with ℓ in = (b, u(b)) and Locs fin = {(e, 0)}.
States of the from (ℓ, i), i ≥ 1, are used to initialize the store to u (using the first 2 types of transitions below). The state (e, 0) has a special role, which is to initiate the simulation of the next transition (using transitions of type 3 given below). States of the form (v, ℓ) are used is to modify the number of copies of ℓ in the store as required by v (using transitions of types 4-9). Observe at the end of the simulation of a transition, the simulation reverts back to (e, 0) so that a new simulation may begin.

The set of transitions is as follows Next we consider decision problems for the logics described in Sec. 4. Given a sentence in such a logic we would like to check whether it is absurd. This amounts to asking whether there is at least one CBM which can model the given sentence, the so-called satisfiability problem for the logic. The satisfiability problems (2',5') for MSO and IPDL are undecidable over MSCNs, even when p = 1. Indeed, the set of runs of a multi-pushdown system or an automaton with queues is expressible in these logics and as a result the satisfiability problem for these logics is undecidable.

((ℓ, i), a, (ℓ, i -1), ℓ) ∈ Trans p! if i > 0. ((ℓ, 0), a, (ℓ ′ , u(ℓ ′ ))) ∈ Trans p,i if ℓ ⋖ L ℓ ′ . ((e, 0), a, (v, b) ∈ Trans p,i ∀v ∈ V. ((v, ℓ), a, (v, ℓ ′ ), ℓ) ∈ Trans p! if ℓ ⋖ L ℓ ′ and v(ℓ) = 1. ((v, ℓ), ℓ, a, (v, ℓ ′ )) ∈ Trans p? if ℓ ⋖ L ℓ ′ and v(ℓ) = -1. ((v, ℓ), a, (v, ℓ ′ )) ∈ Trans p,i if ℓ ⋖ L ℓ ′ and v(ℓ) = 0. ((v,
The satisfiability problems [START_REF] Faouzi Atig | Emptiness of multipushdown automata is 2ETIME-Complete[END_REF][START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF] for MSO and IPDL over CBMs are also undecidable. Recall, from Sec. 4, that MSO and IPDL can both express LIFO (as well as FIFO) restrictions. This can be used to show that the set of runs of a multi-pushdown system or an automaton with queues is also expressible in these logics over CBMs.

Another important verification problem is model checking of CPS (resp. CPSQ) against specifications given in some logic, that is, given a system and a formula, decide whether some CBM (resp. MSCN) accepted by the CPS (resp. CPSQ) satisfies the formula. As usual, the satisfiability problem reduces to the model checking problem since it is easy to describe a CPS (resp. CPSQ) accepting all CBMs (resp. MSCNs) over (Procs, Σ). Thus, due to the presence of multiple-stacks/queues in CPSQs, model-checking problems (6'-9') are all undecidable. Since MSO and IPDL can express LIFO or FIFO restrictions, the model checking problems [START_REF] Breveglieri | Multi-pushdown languages and grammars[END_REF][START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] are also undecidable.

For PDL and TL, both satisfiability (3) and model-checking for CPS ( 7) are decidable with high complexity. The solution presented below uses the classical tableaux construction. These problems remain open for PDL with converse.

To prove that the satisfiability problem for PDL sentences over CBMs is decidable, we consider an extended labeling of a CBM with maximal consistent subsets of the Fischer-Ladner closure of the formula [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. The proof is then done in two steps. In the first step, we describe consistency conditions on the labelings. These conditions essentially relate the labeling of a node with that of its neighbouring nodes. In the second step we argue that these conditions can be checked by a CPS. For the satisfiability of the PDL sentence, the CPS in addition needs to witness some nodes in which some state formulas hold. Thus, the satisfiability problem for PDL sentences can be reduced to the emptiness checking of CPS, which is decidable (with complexity equivalent to reachability in VAS).

First, consider a PDL formula π σ. This formula is equivalent to π • σ true. Hence, for the sake of notations, we may assume that if π σ appears as a subformula then σ is true. Furthermore, we simply denote it by π (which means π true).

Next, we describe the Fischer-Ladner closure of a PDL formula. The path expressions present some subtleties. We need to indicate the current "progress" of a path expression. Hence we first consider the automaton for a path expression seen as a regular expression.

Let π be a path expression. Let Tests(π) = {β 1 , . . . , β k } be the set of tests appearing in π. Now, π is a regular expression over the alphabet {→, ⊲}∪Tests(π). Let A π be a finite state automaton for π (obtained from any standard regular expressions to finite state automata translation). Now we are ready to describe the closure of a PDL state formula σ, denoted CL(σ).

-σ ∈ CL(σ). -If ¬σ 1 ∈ CL(σ) then σ 1 ∈ CL(σ). -If σ 1 ∈ CL(σ) and σ 1 is not a negation then ¬σ 1 ∈ CL(σ). -If σ 1 ∨ σ 2 ∈ CL(σ) then σ 1 , σ 2 ∈ CL(σ). -If π ∈ CL(σ) then • π@q ∈ CL(σ) for all states q of A π , • β ∈ CL(σ) for all β ∈ Tests(π).
Now we are ready to describe the first step of the proof. We consider the labeling of the events of a CBM by maximal consistent subsets of CL(σ). The labeling of an event is intended to describe the precise set of formulas in CL(σ) which hold true at that event. If π@q is present at an event, the intended meaning is that a run of the automaton A π from state q to a final state can be simulated as a walk on the CBM from the current event. We will now describe the consistency conditions on the labeling which ensure that the labeling indeed does what we want.

A set X ⊆ 2 CL(σ) can label an event labeled a on process p only if it agrees to the following static consistency:

-if b ∈ Σ ∩ CL(σ) then b ∈ X ⇔ b = a, -if q ∈ Procs ∩ CL(σ) then q ∈ X ⇔ q = p, -if ¬σ 1 ∈ CL(σ) then σ 1 ∈ X ⇔ ¬σ 1 / ∈ X, -if σ 1 ∨ σ 2 ∈ CL(σ) then σ 1 ∨ σ 2 ∈ X ⇔ σ 1 ∈ X or σ 2 ∈ X, -if π ∈ CL(σ) then
• π ∈ X ⇔ π@q ∈ X for some initial state q of A π ,

• π@q ′ ∈ X and β ∈ X and q

β -→ q ′ in A π implies π@q ∈ X, • q is a final state of A π implies π@q ∈ X.
Moreover the labeling of an event should be consistent with that of its → and ⊲ successors. Let e be an event of the CBM and let e ′ and e ′′ be events of the CBM such that e → e ′ and e ⊲ e ′′ if they exist. Let X, X ′ and X ′′ be their respective labelings. Then the following (local) dynamic consistency must also hold. If π ∈ CL(σ) and q is a state of A π then π@q ∈ X only if there is a path

q = q 0 β1 -→ q 1 β2 -→ q 2 . . . β k -→ q k in A π with k ≥ 0, β 1 , β 2 , . . . , β k ∈ X and -either q k is a final state of A π , -or q k → -→ q ′ in A π and π@q ′ ∈ X ′ , -or q k ⊲ -→ q ′ in A π and π@q ′ ∈ X ′′ .
Furthermore, for all π@q ′ ∈ CL(σ), if π@q ′ ∈ X ′ and q → -→ q ′ in A π then π@q ∈ X. Also, for all π@q ′′ ∈ CL(σ), if π@q ′′ ∈ X ′′ and q ⊲ -→ q ′′ in A π then π@q ∈ X.

Let χ : E → 2 CL(σ) be a labeling of the events. We say that χ is consistent if it respects the static and (local) dynamic consistency conditions described above. The consistency condition ensures the correctness of the labeling:

Lemma 3. χ is consistent if and only if χ(e) = {α ∈ CL(σ) | M, e |= α}.
The first step of the proof is complete. In the second step we argue that the above consitency conditions can be checked by a CPS. The CPS remembers a pair (X 1 , X 2 ) in its locations. X 1 is the labeling of the current event and X 2 is the expected labeling of the successor event. Then,

-((X 1 , X 2 ), a, (X 2 , X 3 ), X 4 ) ∈ Trans p! if (X, X ′ , X ′′ ) = (X 2 , X 3 , X 4 ) satisfies the consistency conditions, -((X 1 , X 2 ), a, (X 2 , X 3 )) ∈ Trans p,i if (X, X ′ , X ′′ ) = (X 2 , X 3 , ∅) satisfies the consistency conditions, -((X 1 , X 2 ), X 2 , a, (X 2 , X 3 )) ∈ Trans p? if (X, X ′ , X ′′ ) = (X 2 , X 3 , ∅) satisfies the consistency conditions.
From the initial state, there is a transition to a pair of static consistent subsets of CL(σ). That is, the pair (X 1 , X 2 ) may be replaced with ℓ in in the above paragraph to get the initial transitions.

A pair (X 2 , X 3 ) is a final state on a process if X 3 = ∅ and (X, X ′ , X ′′ ) = (X 2 , ∅, ∅) satisfies the consistency conditions.

In order to evaluate a PDL sentence φ, we add a flag bit ε σ for each subformula E σ of φ. The flag bit ε σ is set to 0 initially and it is set to 1 as soon as a transition (as described above) with σ ∈ X 2 is taken. The global final acceptance then permits all combinations of locations which are final states on respective processes and in addition, the formula φ evaluates to true when its subformulas E σ are replaced with their associated flag bits ε σ .

The construction is complete. The sentence φ is satisfiable if and only if the language accepted by the constructed CPS is non-empty.

Remark 5. The construction will not go through as such if we consider CPDL instead of PDL. However, if the path-expressions inside any iteration ( * ) are one-way then the above construction can be adapted to check its satisfiability. Thus, we see that most verification problems are undecidable. Moreover, the decidable cases have high complexity. However, if we restrict these decision problems to CBMs (or MSCNs) with split-width bounded by some parameter k, we obtain tractable decision procedures for almost all of them in a uniform manner (the only exception is in problems where the MSO formula is part of the input, where non-elementary lower bounds are known even for ordinary words, leave alone CBMs). The following sections describe this technique in detail.

Split-CBMs to Trees

Here, we show how to encode CBMs of bounded split-width with finite binary trees. This is a crucial step in all the decision procedures described in Sec. 10 that exploit the bound on split-width.

As it stands, each split-term s defines a set of split-CBMs s . In order to reason about each split-CBM we decorate split-terms with additional labels so that each such labeled term denotes a unique split-CBM. The reason s is a set is that the operations merge and ✁ are ambiguous. For instance, the merge operation replaces one elastic edge by a rigid edge, but does not specify which. By decorating each merge operation with the identity of this edge we resolve this ambiguity. The shuffle operation permits the interleaving of the components coming from its two operands in multiple ways and we disambiguate it by decorating each shuffle operation with the precise ordering of these components.

The key observation is that we only need a finite set of labels to disambiguate every split-term of width at most k. Our labels consist of a word per process, containing one letter per component indicating the origin of that component. At merge nodes we use letters m to denote that it is the result of a merge and i to indicate that it is inherited as it is from the operand. At a shuffle node we use letters ℓ to indicate it comes from the left operand and r to indicate it comes from the right. For instance, Fig. 7 and8 give the 3-DSTs corresponding to the split-CBMs in Fig. 6 arising from the split-term s from Ex. 5. A k-disambiguated split-tree or k-DST is a split-term s of width at most k, treated as a binary tree, labeled by L k+1 , and satisfying some validity conditions. Hence, each node n of t corresponds to a subterm s n of s, and we denote by (W p (n)) p∈Procs its labeling. We define simultaneously, the validity condition for the labeling at each node n and the unique split-CBM M n belonging to s n identified by this labeling.

merge (mi, ii) ✁ (ℓrℓ, rr) ⊲ (ℓℓ, ε) (a, 1) (ℓ, ε) (b, 1) (ℓ, ε) ✁ (ℓ, ℓr) ⊲ (ℓ, ℓ) (b, 2) (ε, ℓ) (a, 1) (ℓ, ε) (a, 2) (ε, ℓ)
1. If n is a leaf with associated split-term s n = (a, p) ∈ Σ × Procs, then M n is the unique split-CBM in s n and we set W p (n) = ℓ and

W p ′ (n) = ε if p ′ = p. 2.
If n is a ⊲ node then its children must be leaves n ′ and n ′′ and s n = s n ′ ⊲ s n ′′ .

Again, M n is the unique split-CBM in s n and we set Clearly, the validity conditions above for k-DSTs can be checked with a deterministic bottom-up tree automaton.

W p (n) = W p (n ′ ) • W p (n ′′ )
Lemma 4. The set of k-DSTs is a regular tree language recognized by a tree automaton A k-valid whose size is

2 O(k|Procs|) + O(|Σ| • |Procs|).
We write M t for the split-CBM described by the root of t. When a split-term s has width k, it is not difficult to see that, any split-CBM M ∈ s can be obtained as M t for some k-DST t with associated split-term s.

We can recover M t from t and hence reason about M t using t. Clearly the events in M t are in bijective correspondence with the leaves of t and we identify the two. If n and n ′ are leaves of t then n ⊲ n ′ in M t iff there is a ⊲ node in t whose left child is n and right child is n ′ .

When is n r -→ n ′ in M t ? The r -→ edge connecting them is to be found in some merge common ancestor of n and n ′ . We walk up the tree starting at leaf n tracking the identity of the component whose last event is n (this component may grow in size as previous components are merged with it), till a merge node x merging this component with the next is encountered. We also walk up the tree starting at the leaf n ′ tracking the identity of its component till a merge node x ′ merging this component with the previous one is encountered. These routes from n and n ′ are marked in red and blue in Fig. 8.

Clearly, n r -→ n ′ iff x = x ′ . It is easy to build a bottom-up tree automaton to carry out this tracking and to check if x = x ′ . This gives us the first part of the following Proposition. The second part follows from the observation that having found x one may walk down from there to the leaf n ′ . Proposition 1. -There is a deterministic bottom-up tree automaton with at most 3kp + 2 states which accepts the set of k-DSTs t having exactly two marked leaves n and n ′ such that n r -→ n ′ in the split-CBM M t . -There is a deterministic tree-walking automaton with at most 2kp states which has an accepting run on a k-DST t from leaf n to leaf n ′ iff n r -→ n ′ in the split-CBM M t . Remark 6. It is also possible to restrict Lemma 4 and Proposition 1 to k-DSTs that identify CBMs (as opposed to split-CBMs). An analogue of Proposition 1 can also be established for the relation r -→ -1 as well as e -→ and e -→ -1 .

10 Split-width and Decidability

Satisfiability

An easy consequence of Proposition 1 is that the satisfiability problem for MSO becomes decidable when restricted to CBMs of split-width at most k.

merge (mi, ii) ✁ (ℓrℓ, rr) ⊲ (ℓℓ, ε) (a, 1) (ℓ, ε) (b, 1) (ℓ, ε) ✁ (ℓ, ℓr) ⊲ (ℓ, ℓ) (b, 2) (ε, ℓ) (a, 1) (ℓ, ε) (a, 2) (ε, ℓ)
Fig. 8: Recovering a rigid edge in a 3-DST.

Theorem 2. From any MSO(Procs, Σ) formula ψ one can effectively construct a tree automaton A k ψ such that

L(A k ψ ) = {t | t is a k-DST, M t |= ψ} .
By Lemma 4 and Remark 6 we may assume that the input is a k-DST representing a CBM. The argument is quite standard: construct the automaton inductively, using closure under union, intersection, complement and projection to handle the boolean operators and quantifiers. This leaves the atomic formulas. The formula a(x) is translated to a tree automaton that verifies that x is a leaf and that it is labeled a and similarly for p(x). The formula x ∈ X is translated to a tree automaton that verifies that x is a leaf and belongs to the set of leaves labeled by X. x ⊲ y just requires us to verify that the leaves labeled x and y have a parent labeled ⊲. Finally, x → y is handled using Proposition 1, completing the proof. As always, the combination of projection and complementation means that the size of the constructed automaton grows as a non-elementary function.

Decidability for MSO immediately implies decidability for all the variants of PDL (and the Temporal Logics). However, we obtain more efficient decision procedures by working directly with these logics. Theorem 3. From any CPDL sentence ψ one can effectively construct a tree automaton A k ψ whose size is

2 O(p 2 .k 2 .|σ| 2 ) such that L(A k ψ ) = {t | t is a k-DST, M t |= ψ}.
The idea here is to use alternating 2-way tree automata (A2A). For a PDL sentence E σ the A2A walks down to a leaf and starts a single copy of the A2A that will verify the formula σ. For each σ we construct an automaton A σ such that A σ has an accepting run from a leaf n if and only if the event n in the associated CBM satisfies σ. The automata for the atomic formulas true, p and a are selfevident. For ∨ and ¬ we use the constructions for union and complementation for A2A. The case where σ = π σ ′ needs a little bit of work. Suppose π does not use any state formulas then we construct a finite automaton B π equivalent to the regular expression π (over the alphabet D = {→, → -1 , ⊲, ⊲ -1 }). We non-deterministically guess an accepting run of B π , simulating each move labeling this run using the tree-walking automata given by Proposition 1 and Remark 6. Notice that each such simulation of a move from D begins and ends at a leaf. Finally, when reaching a final state of B π , we start a copy of the automaton A ′ σ . Checking state formulas in π adds no complication due to the power of alternation. To verify the formula α we simply propagate a copy of the automaton A α at the current node (leaf). All this can be formalized to get an A2A A σ of size O(k • p • |σ|). We then use Vardi's result [START_REF] Vardi | The taming of converse: Reasoning about two-way computations[END_REF] to convert this into an ordinary tree automaton of size 2 O(k 2 •p 2 •|σ| 2 ) . Since temporal logic formulas can be translated into CPDL formulas with linear increase in size, it follows that Corollary 1. The satisfiability problem for TL(Procs, Σ) over k-split-width CBMs is decidable in ExpTime.

The intersection operator in IPDL adds an additional level of complexity, since path expression 1 ∩ π 2 requires that the tree walking automata propagated to handle π 1 and π 2 have to end up at the same leaf. However, the technique of [START_REF] Göller | Pdl with intersection and converse: satisfiability and infinite-state model checking[END_REF] to decide IPDL over trees can be adapted to our setting as well. As in [START_REF] Göller | Pdl with intersection and converse: satisfiability and infinite-state model checking[END_REF] this results in an additional exponential increase in size.

Theorem 4. From any ICPDL sentence ψ one can effectively construct a tree automaton A k ψ whose size is doubly exponential such that

L(A k ψ ) = {t | t is a k-DST, M t |= ψ}.
We explain the construction of alternating 2-way tree automata (A2A) for ICPDL. We have already explained the construction for CPDL in Sec. 10. The modification required to deal with intersection is borrowed from [START_REF] Göller | Pdl with intersection and converse: satisfiability and infinite-state model checking[END_REF] and explained below.

Recall, from Section 10, that from any state formula σ in CPDL, we construct by structural induction an A2A A σ such that A σ has an accepting run starting from some leaf n of a k-DST t if and only if M t , n |= σ. In this construction, to deal with any formula of the form π α, we construct an alternating A2A automaton with a specific structure: it consists of a tree-walking automaton which navigates a walk from a leaf n to another leaf n ′ (possibly going through many leaves on the way) in the given k-DST t (propagating state-formula checking automata on the way) and transfers control to the automaton for α at n ′ . Let us call this automaton A π . Then, A π has an accepting run starting at a leaf n in which its tree-walking component reaches the leaf n ′ iff M t , n, n ′ |= π.

Extending this to the case where π = π 1 ∩ π 2 , turns out to be a direct application of the technique of [START_REF] Göller | Pdl with intersection and converse: satisfiability and infinite-state model checking[END_REF], where an A2A construction for modelchecking ICPDL over trees is described. Consider any accepting walk w of the tree-walking component of A π1 from a leaf n to a leaf n ′ . This may be broken up as w 0 e 1 w 1 • • • e m where e 1 e 2 • • • e m is the (unique) shortest path from n to n ′ in the tree and further there is no occurrence of e i in w i e i+1 • • • e m . If w is an accepting walk of A π2 then we may write w ′ = w ′ 0 e 1 w ′ 1 • • • e m similarly. The idea is to synchronize the tree-walking part of the automata A π1 and A π2 on the edges along the path e 1 e 2 • • • e m while allowing them to evolve asynchronously along w i (w ′ i ). As shown in [START_REF] Göller | Pdl with intersection and converse: satisfiability and infinite-state model checking[END_REF], it is easy with an A2A to check, given a pair of states (q, q ′ ) of A π1 (resp. of A π2 ) whether there is a looping path in the tree starting from state q and ending in state q ′ . The states of the walking automaton part of A π1∩π2 are pairs of states, one each form the walking automaton part of A π1 and A π2 . At each step along the path e 1 e 2 • • • e m , this walking automaton from a state (q 1 , q 2 ) first guesses the existence of looping paths q 1 to q ′ 1 and q 2 to q ′ 2 in A π1 and A π2 respectively and propogates automata to verify the same. It then synchronises a pair of transitions, q ′ 1 to q ′′ 1 from A π1 and q ′ 2 to q ′′ 2 from A π2 to take one more step along the walk e 1 • • • e m and move to (q ′′ 1 , q ′′ 2 ). The details are easy to formalise and thus the construction extends to the case where intersection is permitted as part of path formulas.

For the complexity, we have already argued in Sec. 10 that the number of states of A σ is O(k • p • |σ|) when σ is a formula from CPDL. This is because a basic move along a linear edge → is simulated with O(k • p) states thanks to Prop. 1, and all constructs from CPDL only increase the size of the automata linearly. Now, intersection induces a quadratic increase in the number of states. Indeed, it requires pairs of states, either from A π1 or from A π2 to check the existence of looping paths, or from A π1 and A π2 to synchronously follow the shortest path between two leaves. Due to this, we can show that the size of the A2A A σ constructed from a formula σ in ICPDL is 2 poly(|σ|) , and we deduce that the size of the corresponding tree automaton is doubly exponential in |σ|. We refer to [START_REF] Göller | Pdl with intersection and converse: satisfiability and infinite-state model checking[END_REF]Section 3.3] for a more detailed study of the complexity, which can be further refined if we consider the intersection width of the ICPDL formula.

Emptiness and other Problems on CPS

We now show that the emptiness, universality and the containment problems for CPS w.r.t. CBMs with split-width bounded by k have reasonable complexity.

Lemma 5. Given a CPS S over (Procs, Σ) and any integer k, one can effectively construct a tree automaton A k S with |Locs| O(p.k) many states such that

L(A k S ) = {t | t is a k-DST, M t ∈ L (S)} .
Recall, from Sec. 3, that a run is just a labeling of the events by locations via two functions (ρ, ν) satisfying 3 requirements. Our aim is to construct a bottom-up tree automaton that simulates such runs on any k-DST.

Let t be a k-DST. The events of M t are the leaves of t. The bottom-up tree automaton guesses a possible labeling of the events (the leaves) and verifies that it defines a run as it walks up the DST. Actually, at each leaf e, the automaton guesses the location labels assigned to e as well as to e -, the reason for which will be clear soon. Due to this double labeling, if e is an internal event then conformance to requirement 3 in the definition of a run can be checked immediately. Similarly, if e ⊲ f then, by nondeterministically guessing the identity of the value that is placed and removed from the store by transitions at these two events, the automaton can verify the conformance to requirement 1 at e and to requirement 2 at f simultaneously. This is done as it visits the parent of these two nodes (labeled ⊲). We are almost done, except that all this assumes the correctness of the guess about the labeling of e -at each e. It remains to verify the correctness of these guesses.

The correctness of the guess at leaf e is verified at the unique merge node m e in the tree that adds the r -→ (or equivalently →) edge connecting e -and e. Thus, the guessed location labels of e -and e need to be carried in the state of the automaton till this node is reached. The key observation is that at every node in the path from e to m e , e is the left-most event in its component and similarly, e - is the right-most event in its component along the path from e -to m e . In other words, as the automaton walks up the tree, it only needs to keep the guesses for the first and last events in each component (in each process). The number of such events is bounded by p(k + 1), explaining the complexity stated in Lem. 5. (Actually, for the first event e in any component it suffices to keep the labels associated with e -and for the last event e it suffices to keep the labels for e.)

It is easy to maintain this information. At a merge node, apart from checking the correctness as explained above, the unnecessary labels (e/e -if they are not the first or last events of the merged component) are dropped and other labels are inherited. At a shuffle node, the labels for each component is simply inherited. Finally, when the automaton reaches the root, there is only one component per process. The entire run accepts if in each process the location labeling e -of the first event is ℓ in and the tuple of locations labeling the last events of each process is a final state in Locs fin . In all this we have assumed that the automaton reads a k-DST, but that can be arranged using Lemma 4, completing the proof. As an immediate application we have the following theorem. Emptiness problem for S reduces to the emptiness problem for A k S . Notice that a CBM M of split-width at most k is accepted by S iff all k-DSTs representing M are accepted by A k S . Hence, the universality problem reduces to checking whether A k S accepts all k-DSTs representing CBMs (as opposed to split-CBMs), which is just the equivalence problem of tree automata. Finally, the containment problem reduces to the containment problem for associated tree automata.

Example 1 .

 1 Fig. 1: A CBM M

Fig. 3 :Fig. 4 :

 34 Fig.3: Split-CBM M obtained by splitting M (Fig.1).

Fig. 5 :

 5 Fig. 5: Two shuffled split-CBMs.

Fig. 6 :

 6 Fig. 6: Two split-CBMs

  ′ , -elasticity(merge(s)) = elasticity(s) -1, and elasticity(s 1 ✁ s 2 ) = elasticity(s 1 ) + elasticity(s 2 ) + |Procs(s 1 ) ∩ Procs(s 2 )|.

  e), a, (e, 0), e) ∈ Trans p! if v(e) = 1. ((v, e), e, a, (e, 0)) ∈ Trans p? if v(e) = -1.((v, e), a, (e, 0)) ∈ Trans p,i if v(e) = 0. ⊓ ⊔

Fig. 7 :

 7 Fig. 7: A 3-DST for the split-term in Ex. 5.

Theorem 5 .

 5 The emptiness problem for CPS over (Procs, Σ) w.r.t. k-splitwidth CBMs is decidable in Exptime. The universality problem and inclusion problems w.r.t. k-split-width CBMs are decidable in 2-Exptime.

  Definition 3. A system of concurrent processes with store (CPS) over a set of processes Procs and actions Σ is a tuple S = (Locs, (Trans p ) p∈Procs , ℓ in , Locs fin ) where -Locs is the finite set of local control locations, -ℓ in ∈ Locs is local initial state of each process, -Locs fin ⊆ Locs Procs is the set of global final states, -Trans p = Trans p,i ⊎ Trans p! ⊎ Trans p? is the set of local transitions of process p where Trans p,i ⊆ Locs × Σ × Locs Trans p! ⊆ Locs × Σ × Locs × Locs Trans p? ⊆ Locs × Locs × Σ × Locs Trans p,i denotes the internal transitions of Process p, i.e., those that do not involve the store, Trans p! denotes the set of write transitions of Process p, i.e., transitions which write to the store and Trans p? are the transitions of p which read from the store.

Table 1 )

 1 for CPS/CBM and CPSQ/MSCN. The Emptiness Problem (1, resp. 1') asks whether a given CPS (resp. CPSQ) is empty. The satisfiability problems for MSO (2) and the different variants of PDL[START_REF] Faouzi | On the reachability analysis of acyclic networks of pushdown systems[END_REF][START_REF] Bollig | Propositional dynamic logic for messagepassing systems[END_REF][START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF] ask whether a given sentence is satisfied by any CBM.

Table 1 :

 1 Problems for CPS and CBM. Primed versions refer to the corresponding problems for CPSQ/MSCN.

	let -→ * be the reflexive-transitive

φ: MSO sentence Is there a CBM M ∈ L (S) ∩ k-CBM s.t. M |= φ? S: CPS k ∈ N 16,17,18 par-(ǫ,C,IC)PDL-MC φ: (ǫ,C,IC)PDL sentence S: CPS k ∈ N 2ExpTime in |φ| ExpTime in k 16,16', 17,17' ExpTime in k, |φ| PTime in |S| 18,18' 2ExpTime in |φ| ExpTime in k PTime in |S|

Table 2 :

 2 Decidability and complexities

  for all p ∈ Procs.3. If n is a merge node, then it has a single child n ′ and s n = merge(s n ′ ). In this case, there must be exactly one process p such that W p (n) ∈ i * mi * and |W p (n)| = |W p (n ′ )| -1 and for all other p ′ = p, we have W p ′ (n) ∈ i * and |W p ′ (n)| = |W p ′ (n ′ )|.Further, M n is the split-CBM obtained from M n ′ by merging on process p the component indicated by m in W p (n) with the next component. Clearly M n ∈ s n . 4. If n is a shuffle node, it has two children n ′ and n ′′ and s n = s n ′ ✁s n ′′ . Then, for each process p ∈ Procs, we have W p (n) ∈ {ℓ, r} ≤k and # ℓ (W p (n)) = |W p (n ′ )| and # r (W p (n)) = |W p (n ′′ )|. Moreover, M n is the unique split-CBM obtained by shuffling the components of M n ′ and M n ′′ as indicated by (W p (n)) p∈Procs and once again M n ∈ s n .

Model-checking

The k-split-width model-checking problem for a logic L determines, given a CPS and a formula ϕ in L, whether some CBM of split-width at most k accepted by the CPS satisfies ϕ. In all the cases, we use results from Sections 10.1 and 10.2, we first construct from the formula ϕ a tree automaton A k ¬ϕ that recognizes all k-DSTs representing CBMs that do not satisfy ϕ. The model-checking problem then reduces to the emptiness of the intersection of the tree automata A k ¬ϕ and A k S .

Discussions

Optimal complexities of the decision procedures Optimality of the reachability in CPS and of PDL satisfiability follows from the equivalence to (reduction from) VAS. The PTime hardness on the size of the system |S| for the problems 10, 16-18, 10', 16'-18' follow from the PTime hardness of the emptiness checking of nested-word automata, since nested-words have split-width bounded by 2 (cf.

Remark 3). The hardness of problems 14, 18, 12'-14', 16'-18' with respect to the size of the (ǫ,C,IC)PDL formula and more specifically with respect to the bound on split-width follow from the corresponding problems in the case of bounded phase multi-pushdown systems [START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF] and the bound on their split-width [START_REF] Cyriac | MSO decidability of multipushdown systems via split-width[END_REF].

Open problems In addition to problems 4 and 8 from Table 1 a number of interesting problems remain open (see [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF]). Given an architecture A, a set of actions Σ and an integer k, is it possible to design a CPSQ S univ k over A and Σ such that it accepts exactly the MSCNs whose split-width is bounded by k? If so, one can restrict any CPSQ to its (verified) k-bounded split-width behaviours by intersecting it with S univ k . This problem is open, however see [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF] for subclasses which can be easily implemented as CPSQs. These subclasses generalize many known decidable system restrictions, giving elementary decision procedures for various model-checking problems. Another open problem is whether we can construct the CPS (or CPSQ) corresponding to a regular language of k-DSTs. An affirmative answer would immediately yield a complementation procedure for CPS w.r.t. behaviours of split-width at most k.