Benedikt Bollig
email: bollig@lsv.ens-cachan.fr

Manuela-Lidia Grindei
email: grindei@lsv.ens-cachan.fr

Peter Habermehl

Realizability of Concurrent Recursive Programs ⋆

We define and study an automata model of concurrent recursive programs. An automaton consists of a finite number of pushdown systems running in parallel and communicating via shared actions. Actually, we combine multi-stack visibly pushdown automata and Zielonka's asynchronous automata towards a model with an undecidable emptiness problem. However, a reasonable restriction allows us to lift Zielonka's Theorem to this recursive setting and permits a logical characterization in terms of a suitable monadic second-order logic. Building on results from Mazurkiewicz trace theory and work by La Torre, Madhusudan, and Parlato, we thus develop a framework for the specification, synthesis, and verification of concurrent recursive processes.

Introduction

The analysis of a concurrent recursive program where several recursive threads access a shared memory is a difficult task due to the typically high complexity of interaction between its components. One general approach is to run a verification algorithm on a finite-state abstract model of the program. As the model usually preserves recursion, this amounts to verifying multi-stack pushdown automata. Unfortunately, even if we deal with a boolean abstraction of data, the controlstate reachability problem in this case is undecidable [START_REF] Ramalingam | Context-sensitive synchronization-sensitive analysis is undecidable[END_REF]. However, as proved in [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF], it becomes decidable if only those states are taken into consideration that can be reached within a bounded number of context switches. A context switch consists of a transfer of control from one process to another. This result allows for the discovery of many errors, since they typically manifest themselves after a few context switches [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]. Other approaches to analyzing multithreaded programs restrict the kind of communication between processes [START_REF] La Torre | Context-bounded analysis of concurrent queue systems[END_REF][START_REF] Sen | Model checking multithreaded programs with asynchronous atomic methods[END_REF], or compute overapproximations of the set of reachable states [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF].

All these works have in common that they restrict to the analysis of an already existing system. A fundamentally different approach would be to synthesize a concurrent recursive program from a requirements specification, preferably automatically, so that the inferred system can be considered "correct by construction". The general idea of synthesizing programs from specifications goes back to [START_REF] Emerson | Using branching time temporal logic to synthesize synchronization skeletons[END_REF]. The particular case of non-recursive distributed systems is, e.g., dealt with in [START_REF] Castellani | Synthesizing distributed transition systems from global specifications[END_REF][START_REF] Esparza | Synthesis of distributed algorithms using asynchronous automata[END_REF][START_REF] Morin | Decompositions of asynchronous systems[END_REF].

In this paper, we address the synthesis problem for finite-state concurrent recursive programs that communicate via shared actions. More precisely, we are interested in transforming a given global specification in terms of a contextsensitive language into a design model of a distributed implementation thereof. The first step is to provide an automata model that captures both asynchronous procedure calls and shared-variable communication. To this aim, we combine visibly pushdown automata [START_REF] Alur | Visibly pushdown languages[END_REF] and asynchronous automata [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF], which, seen individually, constitute robust automata classes with desirable closure properties and decidable verification problems.

Merging visibly pushdown automata and asynchronous automata, we obtain concurrent visibly pushdown automata (Cvpa), which are a special case of multi-stack visibly pushdown automata (Mvpa) [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]. For Mvpa, the reachability problem is again undecidable. To counteract this drawback, La Torre et al. restrict the domain of possible inputs to k-phase words. A k-phase word can be decomposed into k subwords where all processes are able to evolve in a subword but only one process can return from a procedure [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]. Note that this is less restrictive than the notion of bounded context switches that we mentioned above. When we restrict to k-phase words, Mvpa actually have a decidable emptiness problem and lead to a language class that is closed under boolean operations.

Let us turn to the main contributions of our paper. We consider Cvpa as a model of concurrent recursive programs and Mvpa as specifications. Thus, we are interested in transforming an Mvpa into an equivalent Cvpa, if possible. Indeed, one can lift Zielonka's Theorem to the recursive setting: For every Mvpa language L that is closed under permutation rewriting of independent actions, there is a Cvpa A such that L(A) = L. Unfortunately, it is in general undecidable if L is closed in this way. In the context of k-phase words, however, we can provide decidable sufficient criteria that guarantee that the closure of the specification can be recognized by a Cvpa. We will actually show that the closure of an Mvpa language that is represented (in a sense that will be made clear) by its k-phase executions can be realized as a Cvpa. The problem with Mvpa as specifications is that they do not necessarily possess the closure property that Cvpa naturally have. We therefore propose to use MSO logic as a specification language. Formulas from that logic are interpreted over nested traces, which are Mazurkiewicz traces equipped with multiple nesting relations. Under the assumption of a k-phase restriction, any MSO formula can be effectively transformed into a Cvpa. This constitutes an extension of the classical connection between asynchronous automata and MSO logic [START_REF] Thomas | On logical definability of trace languages[END_REF].

Organization Section 2 provides basic definitions and introduces Mvpa and Cvpa. Section 3 considers the task of synthesizing a distributed system in terms of a Cvpa from an Mvpa specification. In doing so, we give two extensions of Zielonka's Theorem to concurrent recursive programs. In Section 4, we provide a logical characterization of Cvpa in terms of MSO logic. We conclude with Section 5, in which we suggest several directions for future work.

Definitions

The set {1, 2, . . .} of positive natural numbers is denoted by N. We call any finite set an alphabet. Its elements are called letters or actions. For an alphabet Σ, Σ * is the set of finite words over Σ; the empty word is denoted by ε. The concatenation uv of words u, v ∈ Σ * is denoted by u • v. For a set X, we let |X| denote its size and 2 X its powerset.

Concurrent Pushdown Alphabets

The architecture of a system is constituted by a concurrent (visibly) pushdown alphabet. To define it formally, we fix a nonempty finite set Proc of process names or, simply, processes. Now consider a collection Σ = ((Σ c p , Σ r p , Σ int p )) p∈Proc of alphabets. The triple (Σ c p , Σ r p , Σ int p ) associated with process p contains the supplies of actions that can be executed by p. More precisely, the alphabets contain its call, return, and internal actions, respectively. We call Σ a concurrent pushdown alphabet (over Proc) if for every p ∈ Proc, the sets Σ c p , Σ r p , and Σ int p are pairwise disjoint, and for every p, q ∈ Proc with p = q, (Σ

c p ∪ Σ r p ) ∩ (Σ c q ∪ Σ r q ) = ∅. For p ∈ Proc, let Σ p refer to Σ c p ∪ Σ r p ∪ Σ int
p , the set of actions that are available to p. Thus, Σ = p∈Proc Σ p is the set of all the actions. Furthermore, for a ∈ Σ, let proc(a) = {p ∈ Proc | a ∈ Σ p }. The intuition behind a concurrent pushdown alphabet is as follows: An action a ∈ Σ is executed simultaneously by every process from proc(a). In doing so, a process p ∈ proc(a) can access the current state of any other process from proc(a). The only restriction is that p can access and modify only its own stack, provided a ∈ Σ c p ∪ Σ r p . However, in that case, the stack operation can be "observed" by some other process q if a ∈ Σ int q . We introduce further useful abbreviations and let Σ c = p∈Proc Σ c p , Σ r = p∈Proc Σ r p , and

Σ int = ( p∈Proc Σ int p ) \ (Σ c ∪ Σ r ).
Example 1. Let Proc = {p, q} and let Σ = (({a}, {a}, {b}), ({b}, {b}, ∅)) be a concurrent pushdown alphabet where the triple ({a}, {a}, {b}) refers to process p and ({b}, {b}, ∅) belongs to process q. Thus, Σ = {a, a, b, b}, Σ c = {a, b}, Σ r = {a, b}, and Σ int = ∅. Note also that proc(a) = {p} and proc(b) = {p, q}.

If not stated otherwise, Σ will henceforth be any concurrent pushdown alphabet.

Multi-Stack Visibly Pushdown Automata Before we introduce our new automata model, we recall multi-stack visibly pushdown automata, as recently introduced by La Torre, Madhusudan, and Parlato [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]. Though this model will be parametrized by Σ, it is not distributed yet. The concurrent pushdown alphabet only determines the number of stacks (which equals |Proc|) and the actions operating on them. In the next subsection, an element p ∈ Proc will then actually play the role of a process.

Definition 2. A multi-stack visibly pushdown automaton (Mvpa) over Σ is a tuple A = (S, Γ, δ, ι, F ) where S is its finite set of states, ι ∈ S is the initial state, F ⊆ S is the set of final states, Γ is the finite stack alphabet containing a special symbol ⊥, and δ ⊆ S × Σ × Γ × S is the set of transitions.

Consider a transition (s, a, A, s ′ ) ∈ δ. If a ∈ Σ c p , then we deal with a pushtransition meaning that, being in state s, the automaton can read a, push the symbol A ∈ Γ \ {⊥} onto the p-stack, and go over to state s ′ . Transitions (s, a, A, s ′ ) ∈ δ with a ∈ Σ c and A = ⊥ are discarded. If a ∈ Σ r p , then the transition allows us to pop A = ⊥ from the p-stack when reading a, while the control changes from state s to state s ′ ; if, however, A = ⊥, then the a can be executed provided the stack of p is empty, i.e., ⊥ is never popped. Finally, if a ∈ Σ int , then an internal action is applied, which does not involve a stack operation. In that case, the symbol A is simply ignored.

Let us formalize the behavior of the Mvpa A. A stack content is a nonempty finite sequence from Cont = (Γ \ {⊥}) * • {⊥}. The leftmost symbol is thus the top symbol of the stack content. A configuration of A consists of a state and a stack content for each process. Hence, it is an element of S × Cont Proc . Consider a word w = a 1 . . . a n ∈ Σ * . A run of A on w is a sequence ρ = (s 0 , (σ 0 p ) p∈Proc ) . . . (s n , (σ n p ) p∈Proc ) ∈ (S × Cont Proc ) * such that s 0 = ι, σ 0 p = ⊥ for all p ∈ Proc, and, for all i ∈ {1, . . . , n}, the following hold:

[Push] If a i ∈ Σ c p for p ∈ Proc, then there is a stack symbol A ∈ Γ \ {⊥} such that (s i-1 , a i , A, s i ) ∈ δ, σ i p = A • σ i-1 p , and σ i q = σ i-1 q for all q ∈ Proc \ {p}. [Pop] If a i ∈ Σ r p for p ∈ Proc, then there is a stack symbol A ∈ Γ such that (s i-1 , a i , A, s i ) ∈ δ, σ i q = σ i-1 q
for all q ∈ Proc \ {p}, and either A = ⊥ and

σ i-1 p = A • σ i p , or A = ⊥ and σ i p = σ i-1 p = ⊥. [Internal] If a i ∈ Σ int , then there is A ∈ Γ such that (s i-1 , a i , A, s i ) ∈ δ and σ i p = σ i-1 p for every p ∈ Proc.
The run ρ is accepting if s n ∈ F . The language of A, denoted by L(A), is the set of words w ∈ Σ * such that there is an accepting run of A on w. In the following, we denote by |A| the size |S| of the set of states of A.

Clearly, the emptiness problem for Mvpa is undecidable. Moreover, it was shown that Mvpa can in general not be complemented [START_REF] Bollig | On the expressive power of 2-stack visibly pushdown automata[END_REF]. We can remedy this situation by restricting our domain to k-phase words [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]. Let k ∈ N. A word w ∈ Σ * is called a k-phase word over Σ if it can be written as w 1 • . . . • w k where, for all i ∈ {1, . . . , k}, we have w i ∈ (Σ c ∪ Σ int ∪ Σ r p ) * for some p ∈ Proc. The set of k-phase words over Σ is denoted by W k ( Σ). Note that W k ( Σ) is regular. The language of the Mvpa A relative to k-phase words, denoted by L k (A), is defined to be L(A) ∩ W k ( Σ). Even if we restrict to k-phase words, a deterministic variant of Mvpa is strictly weaker, unless we have Σ = Σ int [START_REF] La Torre | A robust class of context-sensitive languages[END_REF][START_REF] Zielonka | Notes on finite asynchronous automata[END_REF].

In this paper, we will exploit the following two theorems concerning Mvpa:

Theorem 3 (La Torre-Madhusudan-Parlato [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]). The following problem is decidable in doubly exponential time wrt. |A|, |Proc|, and k:

Input: Concurrent pushdown alphabet Σ; k ∈ N; Mvpa A over Σ. Question: Does L k (A) = ∅ hold?
Theorem 4 (La Torre-Madhusudan-Parlato [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]). Let k ∈ N and let A be an Mvpa over Σ. One can effectively construct an Mvpa A ′ over Σ such that To make local states and their transition relations explicit, we may consider a Cvpa to be a structure ((S p ) p∈Proc , Γ, (δ a ) a∈Σ , ι, F ).

L(A ′ ) = L k (A), where L k (A) is defined to be Σ * \ L k (A).
Note that, if Σ = Σ int (i.e., Σ = ((∅, ∅, Σ p )) p∈Proc ), then a Cvpa can be seen as a simple asynchronous automaton [START_REF] Esparza | Synthesis of distributed algorithms using asynchronous automata[END_REF][START_REF] Zielonka | Notes on finite asynchronous automata[END_REF]. It is easy to show that the language

L(C) of a Cvpa C is ∼ e Σ -closed meaning that L(C) = [L(C)] ∼ e Σ .
Example 6. Consider the concurrent pushdown alphabet Σ from Example 1. Assume C = (S, Γ, δ, ι, F ) to be the Cvpa depicted in Figure 1 where S is the cartesian product of S p = {s 0 , . . . , s 4 , r 0 , r 2 } and S q = {t 0 , . . . , t 3 }. Actions from {a, a, b} are exclusive to a single process so that corresponding transitions are local. For example, the relation δ a , as required in Definition 5, is given by {(s 0 , A, r 0 ), (s 0 , A, s 1 ), (s 2 , A, r 2 )}. Thus, ((s 0 , t i ), a, A, (r 0 , t i )) ∈ δ for all i ∈ {0, . . . , 3}. In contrast, executing b involves both processes, which is indicated by the dashed lines depicting δ b . For example, ((s 1 , t 0 ), B, (s 2 , t 1 )) ∈ δ b . Furthermore, ((r 0 , t 0 ), b, B, (s 0 , t 0 )), ((s 1 , t 0 ), b, B, (s 2 , t 1 )), and ((r 2 , t 1 ), b, B, (s 2 , t 1 )) are the global b-transitions contained in δ. Note that L 1 (C) = ∅, since at least two phases are needed to reach the final state (s 4 , t 3 ). Moreover,

-L 2 (C) = {(ab) n w | n ≥ 2, w ∈ {a m b m , b m a m } for some m ∈ {2, . . . , n}} and -L(C) = {(ab) n w | n ≥ 2, w ∈ {a, b} * , |w| a = |w| b ∈ {2, . . . , n}} = [L 2 (C)] ∼ e Σ
where |w| a and |w| b denote the number of occurrences of a and b in w. Note that L 2 (C) can be viewed as an incomplete description or representation of L(C).

Realizability of Concurrent Recursive Programs

From now on, we consider an Mvpa A to be a specification of a system, and we are looking for a realization or implementation of A, which is provided by a Cvpa C such that L(C) = L(A). Actually, specifications often have a "global" view of the system, and the difficult task is to distribute the state space onto the processes, which henceforth communicate in a restricted manner that conforms to the predefined system architecture Σ. If, on the other hand, A is not closed under ∼ e Σ , it might yet be considered as an incomplete specification so that we ask for a Cvpa C such that L(C) = [L(A)] ∼ e Σ . We now recall two well-known theorems from Mazurkiewicz trace theory. The first one, Zielonka's celebrated theorem, applies to simple concurrent pushdown alphabets. It will later be lifted to general concurrent pushdown alphabets.

Theorem 7 (Zielonka [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF]). Suppose Σ = Σ int . For every regular language L ⊆ Σ * that is ∼ e Σ -closed, there is a Cvpa C over Σ such that L(C) = L. We fix a strict total order < lex on Σ. It naturally induces a (strict) lexicographic order on Σ * , which we denote by < lex as well. We say that w ∈ Σ * is in (lexicographic) normal form wrt. < lex if it is minimal wrt. < lex among all words in [w] ∼ e Σ . There is exactly one word in [w] ∼ e Σ that is in normal form. For L ⊆ Σ * , we write nf < lex (L) to denote the set of words from L that are in normal form wrt. < lex . In particular, w ∈ Σ * is in normal form iff w ∈ nf < lex ([w] ∼ e Σ ). Theorem 8 (Ochmański [20]). If L ⊆ Σ * is a regular set of words in lexicographic normal form wrt. < lex , then [L] ∼ e Σ is regular. It will turn out to be useful to consider an Mvpa A = (S, Γ, δ, ι, F ) over Σ as a finite automaton reading letters over the alphabet Σ × Γ . Recall that δ is a subset of S ×Σ ×Γ ×S. We will now simply interpret a transition (s, a, A, s ′ ) ∈ δ as the transition (s, (a, A), s ′ ) of a finite automaton with state space S, reading the single letter (a, A) ∈ Σ × Γ . In this manner, we obtain from A a finite automaton, denoted by F A , which recognizes a regular word language L(F A ) over Σ × Γ . Though L(A) is in general not even context-free, we can provide a link between L(A) and L(F A ). Indeed, L(A) contains the projections of words from L(F A ) onto their first component if we restrict to well-formed words.

In a well-formed word, we take into account that the stack symbols from Γ must obey a pushdown-stack policy. Towards the definition of a well-formed word, we first call a word from Σ * p-well-matched (wrt. Σ), for some process p ∈ Proc, if it is generated by the grammar N :

:= a N b | N N | ε | c where a ranges over Σ c
p , b over Σ r p , and c over Σ \ (Σ c p ∪ Σ r p ). Now suppose w = a 1 . . . a n ∈ Σ * . For i, j ∈ {1, . . . , n}, we call (i, j) a matching pair in w if i < j and there is p ∈ Proc such that a i ∈ Σ c p , a j ∈ Σ r p , and a i+1 . . . a j-1 is p-well-matched. A position i ∈ {1, . . . , n} is called unmatched in w if, for every j ∈ {1, . . . , n}, neither (i, j) nor (j, i) is a matching pair. We call a word (a 1 , A 1 ) . . . (a n , A n ) ∈ (Σ × Γ ) * well-formed if (i) for each matching pair (i, j) in a 1 . . . a n , we have A i = A j , (ii) for all i ∈ {1, . . . , n} such that a i ∈ Σ c , we have A i = ⊥, and (iii) for all i ∈ {1, . . . , n} such that a i ∈ Σ r and i is unmatched in a 1 . . . a n , we have A i = ⊥. We provide a projection mapping π : 2 (Σ×Γ ) * → 2 Σ * , which filters from an argument L ⊆ (Σ × Γ ) * all the well-formed words and then abstracts away the symbols from Γ . Formally, π(L) = {w | (w, W ) ∈ L is well-formed} (here and in the following, we may write a word (a 1 , A 1 ) . . . (a n , A n ) ∈ (Σ × Γ ) * as the pair (a 1 . . . a n , A 1 . . . A n )). Though the notion of a well-formed word and the map π actually depend on a given Mvpa, we will omit a corresponding index.

Next, we establish a link between an Mvpa and its finite automaton. The subsequent lemma then extends Theorem 8 to our recursive setting. Proposition 9. For every Mvpa A over Σ, we have

L(A) = π(L(F A )). Lemma 10. Let A be an Mvpa over Σ satisfying nf < lex ([L(A)] ∼ e Σ ) ⊆ L(A). There is a Cvpa C = ((S p ) p∈Proc , Γ, (δ a ) a∈Σ , ι, F ) over Σ such that L(C) = [L(A)] ∼ e Σ .
For all p ∈ Proc, |S p | is doubly exponential in |A| and triply exponential in |Σ|.

Proof. We will basically interpret a given Mvpa over Σ as an Mvpa over a simplified concurrent pushdown alphabet so that Theorems 7 and 8 can be applied. In turn, the resulting automaton will be considered as a Cvpa over Σ and will indeed have the desired property.

So let A = (S, Γ, δ, ι, F ) be an Mvpa over Σ such that nf < lex ([L(A)] ∼ e Σ ) ⊆ L(A). We define a concurrent pushdown alphabet Ω = ((∅, ∅, Σ p × Γ )) p∈Proc . In particular, we have Ω = Σ × Γ . Note that, for every (a, A), (b, B) ∈ Ω, ((a, A), (b, B)) ∈ I e Ω iff (a, b) ∈ I e Σ . Now consider any lexicographic order < ′ lex ⊆ Ω * ×Ω * such that, for every (a, A), (b, B) ∈ Ω, a < lex b implies (a, A) < ′ lex (b, B). Let NF denote the set of all words x ∈ Ω * that are in lexicographic normal form wrt. < ′ lex , i.e., such that

x ∈ nf < ′ lex ([x] ∼ e Ω )
. This set forms a regular word language (cf. [START_REF] Kuske | Weighted asynchronous cellular automata[END_REF]) so that the intersection L(F A ) ∩ NF is regular, too.

According to Theorem 8, [L(F A ) ∩ NF] ∼ e Ω is regular, and Theorem 7 tells us that there is a Cvpa C over the concurrent pushdown alphabet

Ω such that L(C) = [L(F A ) ∩ NF] ∼ e Ω .
From C, we obtain an Mvpa C ′ over Σ with stack alphabet Γ by transforming a transition (s, (a, A), B, s ′ ) into a transition (s, a, A, s ′ ) (recall that (a, A) is necessarily contained in Ω int so that B can indeed be neglected). Observe that C ′ is actually a Cvpa. As L(F C ′ ) = L(C) and, by Proposition 9, π(L(F

C ′ )) = L(C ′ ), we deduce L(C ′ ) = π(L(C)). So it remains to show that [L(A)] ∼ e Σ = π(L(C)). Suppose w ∈ [L(A)] ∼ e Σ .
We chose the word w ′ ∈ [w] ∼ e Σ that is in lexicographic normal form wrt. < lex . As nf < lex ([L(A)] ∼ e Σ ) ⊆ L(A), we have w ′ ∈ L(A). Thus, there must be W ′ ∈ Γ * such that (w ′ , W ′ ) is well-formed and contained in L(F A ) (Proposition 9). As w ′ is in lexicographic normal form wrt. < lex and as < ′ lex is an extension of < lex , (w ′ , W ′ ) is in lexicographic normal form wrt. < ′ lex so that (w ′ , W ′ ) ∈ NF. We can now reorder (w ′ , W ′ ) in such a way that its first component becomes w. Formally, there is W ∈ Γ * such that (w, W ) ∼ e Ω (w ′ , W ′ ). As every word from [(w ′ , W ′ )] ∼ e Ω is well-formed, so is (w, W ), and we conclude

w ∈ π([L(F A ) ∩ NF] ∼ e Ω ). Now suppose w ∈ π([L(F A ) ∩ NF] ∼ e Ω ).
We can find an extension W ∈ Γ * of w such that (w, W ) is well-formed and contained in [L(F A ) ∩ NF] ∼ e Ω . Thus, there is (w ′ , W ′ ) ∈ L(F A ) ∩ NF such that (w ′ , W ′ ) ∼ e Ω (w, W ). The latter implies w ′ ∼ e Σ w. Note that (w ′ , W ′ ) is well-formed, too, so that, by Proposition 9,

w ′ ∈ L(A). We conclude w ∈ [L(A)] ∼ e Σ .
Let us analyze the size of C ′ . For this, we need to introduce two notions concerning finite automata over Ω. A finite automaton is called loop-connected if, for every nonempty word α 1 . . . α n ∈ Ω * labeling a path from a state s back to state s, the graph (V, E) is connected, where → t for some state s ′ . From [START_REF] Kuske | Weighted asynchronous cellular automata[END_REF], we know that there is a deterministic loop-connected finite automaton B 1 over Ω with (|Σ| + 1)! many states that recognizes the set NF. The set of states of F A is the same as that of A so that we obtain, as the product of F A and B 1 , a finite automaton B 2 of size n := |A| • (|Σ| + 1)! recognizing L(F A ) ∩ NF. As B 1 is loop-connected, so is B 2 . According to [START_REF] Kuske | Weighted asynchronous cellular automata[END_REF][START_REF] Muscholl | Message sequence graphs and decision problems on Mazurkiewicz traces[END_REF], there is an I-diamond finite automaton B 3 over Ω with at most N := (n 2 • 2 |Σ| ) (n-1)(|Σ|+1)+1 many states that recognizes [L(B 2 )] ∼ e Ω . In the next step, we constructed, from B 3 , a Cvpa C = ((S ′ p ) p∈Proc , Γ ′ , (δ ′ α ) α∈Ω , ι ′ , F ′ ) over Ω such that L(C) = L(B 3 ). From [START_REF] Genest | Constructing exponential-size deterministic Zielonka automata[END_REF], we know that, for all p ∈ Proc, |S ′ p | can be bounded by 2 N 2 •(|Σ| 2 +|Σ|)+2|Σ| 4 . As C ′ and C have the same local states, we conclude that the number of local states of C ′ is doubly exponential in |A| and triply exponential in |Σ|.

V = {α i | i ∈ {1, . . . , n}} and E = (V × V ) \ I ∼ e Ω . It
Alternatively, we can apply the construction from [START_REF] Baudru | Unfolding synthesis of asynchronous automata[END_REF] to the I-diamond finite automaton B 3 . Then, C ′ has more nondeterminism, and its number of local states is exponential in |S| and doubly exponential in |Σ| and |Γ |.

⊓ ⊔

Since L = [L] ∼ e Σ implies nf < lex ([L] ∼ e Σ )
⊆ L, we obtain, by Lemma 10, the following extension of Zielonka's Theorem. This result demonstrates that Mvpa recognizing a ∼ e Σ -closed language are suitable specifications for Cvpa. Unfortunately, it is in general undecidable if an Mvpa has this property, which can be easily shown by a reduction from the undecidable emptiness problem. However, a restriction to k-phase words allows us to define decidable sufficient criteria for the transformation of an Mvpa into a Cvpa. We will state a Zielonka-like theorem that is tailored to this restriction. There, we require that an Mvpa represents the k-phase words of a system, while the final implementation can produce non-k-phase executions.

Definition 12. For k ∈ N, we call a language L ⊆ W k ( Σ) a k-phase represen- tation if, for all u, v ∈ Σ * and (a, b) ∈ I e Σ with {uabv, ubav} ⊆ W k ( Σ), we have uabv ∈ L iff ubav ∈ L.
Next, we show that the closure of a k-phase representation that is given by an Mvpa can be realized as a Cvpa. Proof. Again, we exploit Lemma 10. Unlike in Theorem 11, we cannot apply it directly, as it is in general impossible to define the lexicographic order < lex in such a way that nf

< lex ([L k (A)] ∼ e Σ ) ⊆ L k (A) if L k (A) is a k-phase representation.
Our trick is to extend Σ by a component that indicates the current phase of a letter. An appropriate definition of a normal form over this extended alphabet will then allow us to apply Lemma 10.

So let k ∈ N and let A = (S, Γ, δ, ι, F ) be an Mvpa over Σ such that L k (A) is a k-phase representation. Based on Σ, we define a new concurrent pushdown alphabet Ω by Ω c p = Σ c p × {1, . . . , k}, Ω r p = Σ r p × {1, . . . , k}, and Ω int p = Σ int p × {1, . . . , k} for all p ∈ Proc. From A, one can construct an Mvpa B over Ω accepting the words (a 1 , ph 1 ) . . . (a n , ph n ) such that both a 1 . . . a n ∈ L k (A) and, for all i ∈ {1, . . . , n}, ph i = min{j ∈ {1, . . . , k} | a 1 . . . a i is a j-phase word}. Intuitively, the additional components ph i give rise to a unique tight factorization of a 1 . . . a n into phases (cf. [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]). Now consider any lexicographic order < ′ lex ⊆ Ω * × Ω * such that i < j implies (a, i) < ′ lex (b, j) and, moreover, a < lex b implies (a, i) < ′ lex (b, i). We claim that L(B) contains, for every word x ∈ L(B), the normal form of x wrt. < ′ lex . Indeed x ∈ L(B) can be written as a concatenation x 1 • . . . • x k with x i ∈ (Σ × {i}) * for all i ∈ {1, . . . , k}. I.e., for two letters α and β occurring in x i and, respectively, x j with i < j, we have α < ′ lex β. In particular, the normal form of x can be obtained by reordering letters within the factors x i , i.e., nf

< ′ lex ([x] ∼ e Ω ) ⊆ nf < ′ lex ([x 1 ] ∼ e Ω )•. . .•nf < ′ lex ([x k ] ∼ e Ω )
. Note that the reordering does not increase the number of phases. As L k (A) is a k-phase representation, the reordering also preserves containment in L(B) and we have nf

< ′ lex ([x] ∼ e Ω ) ⊆ L(B). By Lemma 10, there is a Cvpa C over Ω with L(C) = [L(B)] ∼ e Ω .
Consider the projection from Ω to Σ that is induced by the function f : Ω → Σ given by f ((a, i)) = a. It is easy to see that applying the projection to a Cvpa language over Ω yields a Cvpa language over Σ (this was is associated to executing a in A 2 , must be applied together with reading a so that (A 1 , A 2 ) acts as the stack symbol. Since a corresponding local transition (s ′ 2 , a, A 2 , s ′′ 2 ) has to follow in A 2 , the stack symbol A 2 needs to be stored as well. The formal description of this step can be found below [START_REF] Alur | Visibly pushdown languages[END_REF]. Now, being in the global state (s ′ 1 , s ′ 2 , ((a, b), B 2 , A 2 )), A will, according to the local transition (s ′ 1 , b, B 1 , s ′′ 1 ), perform a b and apply (B 1 , B 2 ) to the designated stack. Again, A 2 will only change its local state into s ′′ 2 . However, the local transition has to conform to the symbol A 2 that had been stored. This step corresponds to rule (3) below. We are now in a global state of the form (s ′′ 1 , s ′′ 2 , 1). In states with 1 in the third position, A 1 and A 2 again act simultaneously (rule (1)).

Formally, A = (S, Γ, δ, ι, F ) is given by

S = S 1 ×S 2 ×({0, 1} ∪ (I e Σ ×Γ 2 ×Γ 2 )), Γ = Γ 1 ×Γ 2 , ι = (ι 1 , ι 2 , 0), and F = F 1 ×F 2 ×{1}. Let (s 1 , s 2 , σ), (s ′ 1 , s ′ 2 , σ ′ ) ∈ S, a ∈ Σ, and (A 1 , A 2 ) ∈ Γ . Then, ((s 1 , s 2 , σ), a, (A 1 , A 2 ), (s ′ 1 , s ′ 2 , σ ′ )) ∈ δ if there are (B 1 , B 2 ) ∈ Γ and b ∈ Σ such that one of the following holds: (1) (σ = σ ′ = 0 or σ = σ ′ = 1), (s 1 , a, A 1 , s ′ 1 ) ∈ δ 1 , and (s 2 , a, A 2 , s ′ 2 ) ∈ δ 2 , or (2) σ = 0, σ ′ = ((a, b), B 2 , A 2 ), (s 1 , a, A 1 , s ′ 1 ) ∈ δ 1 , and (s 2 , b, B 2 , s ′ 2 ) ∈ δ 2 , or (3) σ ′ = 1, σ = ((b, a), A 2 , B 2 ), (s 1 , a, A 1 , s ′ 1 ) ∈ δ 1 , and (s 2 , b, B 2 , s ′ 2 ) ∈ δ 2 .
The only difference in the decision procedure for Question 2 is that

A 2 is such that L(A 2 ) = L k (A 2 ) = L k (A 1 ) ∩ W k ( Σ).
An inspection of the constructions from [START_REF] La Torre | A robust class of context-sensitive languages[END_REF] tells us that the size of A 2 is in both cases triply exponential in |A 1 |, k, and |Proc|. As emptiness of Mvpa wrt. k-phase words is decidable in doubly exponential time, we obtain elementary decision procedures for Question 1 and Question 2.

⊓ ⊔

Specifying Programs in MSO Logic

In Section 3, we considered the language L of an Mvpa to be a specification, and our aim was to find a Cvpa C such that L(C) = [L] ∼ e Σ . Unfortunately, one cannot always find such a Cvpa (consider, e.g., L = (ab) * with (a, b) ∈ I e Σ ). We now present a specification language that operates directly on equivalence classes of ∼ e Σ so that, provided that we restrict to k-phase executions, any specification can be realized as a Cvpa. In doing so, we extend the classical connection between monadic second-order (MSO) logic and finite automata. The study of relations between logical formalisms that may serve as a specification language and automata has had many generalizations, including Mvpa [START_REF] La Torre | A robust class of context-sensitive languages[END_REF].

Actually, we present an MSO logic that is interpreted over partial orders, which arise naturally from words in the presence of a concurrent pushdown alphabet and the induced independence relation. Any such partial order represents one equivalence class of words so that a formula defines a set of equivalence classes or, in other words, a set of words that is ∼ e Σ -closed. Let w = a 1 . . . a n ∈ Σ * . To w, we associate the labeled structure T e Σ (w) = (E, , µ, λ), where E = {1, . . . , n} is the set of events, λ : E → Σ assigns to any event i ∈ E the action λ(i) = a i it executes, and µ ⊆ E×E contains the matching pairs in w (i.e., (i, j) ∈ µ iff (i, j) is a matching pair). Finally, ⊆ E × E is a Fig. 2. A nested trace partial-order relation (i.e., it is reflexive, transitive, and antisymmetric), which is defined to be the transitive closure of {(i, j) ∈ E × E | i ≤ j and (a i , a j ) ∈ I e Σ }. We call the structure T e Σ (w) that arises from a word w ∈ Σ * a nested trace over Σ. The set of nested traces over Σ is denoted by Tr( Σ). It is standard to prove that T e Σ (w) = T e Σ (w ′ ) iff w ∼ e Σ w ′ where we consider equality of nested traces up to isomorphism. In other words, there is a one-to-one correspondence between nested traces and equivalence classes of ∼ e Σ . We remark that nested traces are a merge of Mazurkiewicz traces [START_REF] Diekert | The Book of Traces[END_REF] and nested words [START_REF] Alur | Adding nesting structure to words[END_REF], which, in turn, generalize themselves the notion of a word. Fixing supplies of first-order variables x, y, . . . and second-order variables X, Y, . . ., the syntax of our MSO logic complies with the signature of a nested trace. Formally, formulas from MSO( Σ) are given by the grammar

ϕ ::= x y | (x, y) ∈ µ | λ(x) = a | x ∈ X | ¬ϕ | ϕ 1 ∨ ϕ 2 | ∃xϕ | ∃Xϕ
where x and y are first-order variables, X is a second-order variable, and a ∈ Σ. Moreover, one may use the usual abbreviations such as ϕ 1 ∧ ϕ 2 , ϕ 1 → ϕ 2 , and ∀xϕ. To determine the semantics, let T = (E, , µ, λ) be a nested trace over Σ and I be an interpretation function, which assigns to a first-order variable an element from E and to a second-order variable a subset of E. Let us define when T, I |= ϕ for ϕ ∈ MSO( Σ). Namely, T, I |= x y if I(x) I(y), T, I |= (x, y) ∈ µ if (I(x), I(y)) ∈ µ, and T, I |= λ(x) = a if λ(I(x)) = a. The rest of the semantics is classical for MSO logics. If ϕ is a sentence, i.e., a formula without free variables, we can write T |= ϕ if T, I |= ϕ for some interpretation function I. Now, given a sentence ϕ ∈ MSO( Σ), we set

L (ϕ) = {T ∈ Tr( Σ) | T |= ϕ}.
As the language of a Cvpa C is closed under ∼ e Σ , it is legitimate to assign to C a set of nested traces, too, letting L (C) = {T e Σ (w) | w ∈ L(C)}. Example 17. Suppose T to be the nested trace given in Figure 2 and consider the sentences ϕ 1 = ∀x ((λ(x) = a ∨ λ(x) = b) → ∃y (x, y) ∈ µ) expressing that there is no pending call, and ϕ 2 = ∀x ((λ(x) = a ∨ λ(x) = b) → ∃y (y, x) ∈ µ), which expresses that there is no pending return. We have T ∈ L (ϕ 1 ) but T ∈ L (ϕ 2 ). Note also that T ∈ L (C) for the Cvpa C from Example 6 (Figure 1).

Before we look at a logical characterization of general Cvpa, let us recall a result that has already been found in the context of asynchronous automata, i.e., of Cvpa over simple concurrent pushdown alphabets.

Theorem 18 (Thomas [26]). Suppose Σ = Σ int and let L ⊆ Tr( Σ). Then, L = L (C) for some Cvpa C over Σ iff L = L (ϕ) for some ϕ ∈ MSO( Σ). Now let us turn towards Cvpa over general concurrent pushdown alphabets. It has been shown in [START_REF] Bollig | On the expressive power of 2-stack visibly pushdown automata[END_REF] that MSO logic is in general strictly more expressive than Cvpa. We will therefore extend the notion of k-phase words to nested traces. For k ∈ N, a nested trace T ∈ Tr( Σ) is called a k-phase trace if there is w ∈ W k ( Σ) such that T e Σ (w) = T . The set of k-phase traces over Σ is denoted by Tr k ( Σ). For example, the nested trace T from Figure 2 For a logical characterization of Cvpa, we will need the following lemma.

Lemma 19. Let k ∈ N and let C be a Cvpa over Σ such that L (C) ⊆ Tr k ( Σ). There is a Cvpa C ′ over Σ such that L (C ′ ) = L (C) ∩ Tr k ( Σ), where L (C) = Tr( Σ) \ L (C). Proof. Let k ∈ N and let C be a Cvpa over Σ satisfying L (C) ⊆ Tr k ( Σ). Due to Theorem 4, there is an Mvpa A over Σ such that L k (A) = L k (C) ∩ W k ( Σ).
Observe that L k (A) is a k-phase representation. Thus, by Theorem 13, there is a Cvpa C

′ over Σ such that L(C ′ ) = [L k (A)] ∼ e Σ .
One easily verifies that we actually have L (

C ′ ) = L (C) ∩ Tr k ( Σ). ⊓ ⊔
As a corollary, we obtain that, for every k ∈ N, there is a Cvpa C with L (C) = Tr k ( Σ). This is an important fact in the proof of Theorem 21. Indeed, the following two theorems constitute a logical characterization of Cvpa (restricted to k-phase traces). Both transformations are effective. Hereby, Theorem 20 has a standard proof (see [START_REF] Thomas | On logical definability of trace languages[END_REF] for a similar instance of that problem).

Theorem 20. For every Cvpa C over Σ, there is a sentence ϕ ∈ MSO( Σ) such that L (ϕ) = L (C). Proof (sketch). As usual, one proceeds by induction on the structure of an MSO formula. However, treating negation is less obvious than in classical settings such as words and trees. To get a Cvpa for ¬ϕ, let k ∈ N and suppose that we already have a Cvpa C over Σ such that L (C) = L (ϕ) ∩ Tr k ( Σ) (actually, we need to consider extended concurrent pushdown alphabets to cope with free variables during the inductive translation). By Lemma 19, there is a Cvpa C ′ such that L (C ′ ) = L (C) ∩ Tr k ( Σ). The latter equals L (¬ϕ) ∩ Tr k ( Σ) so that we are done. The translations of atomic formulas, disjunction, and existential quantification exploit the fact that Tr k ( Σ) is recognizable by some Cvpa and that Cvpa are closed under union, intersection, and projection. ⊓ ⊔

Future Directions

Though the results in this paper are of rather theoretical nature, due to the high complexity of our constructions, Cvpa and the related notion of a nested trace may open a new line of research in Mazurkiewciz trace theory and the analysis of multithreaded recursive programs. We mention here some future directions:

We excluded an important question from our study: For k ∈ N and an Mvpa A, when can we decide whether [L k (A)] ∼ e Σ is the language of some Mvpa and, hence, of some Cvpa? If Σ = Σ int , we know that this is the case iff I e Σ ∪ id Σ is transitive [START_REF] Sakarovitch | The "last" decision problem for rational trace languages[END_REF]. In the general setting, the question remains open.

Given an Mvpa A, one may ask if A is already a Cvpa such that its local state spaces and transition relations can be computed effectively. Those questions are addressed and answered positively in [START_REF] Esparza | Synthesis of distributed algorithms using asynchronous automata[END_REF][START_REF] Morin | Decompositions of asynchronous systems[END_REF] for asynchronous automata.

In Cvpa, processes communicate via shared memory. It will be interesting to study extensions of communicating finite-state machines (CFMs), where processes communicate via first-in first-out channels, by visibly pushdown stacks. While Cvpa recognize sets of nested traces, a visibly pushdown CFM would give rise to the notion of a nested message sequence chart. Interestingly, there are theorems for CFMs that constitute counterparts of Zielonka's Theorem [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF][START_REF] Henriksen | A theory of regular MSC languages[END_REF].

For both Mazurkiewicz traces [START_REF] Diekert | LTL is expressively complete for Mazurkiewicz traces[END_REF] and nested words [START_REF] Alur | Firstorder and temporal logics for nested words[END_REF], temporal logics were studied. We raise the question if these logics can be combined towards specification formalisms with decidable satisfiability and model-checking problems.

In a distributed setting, deadlock-free systems are particularly important. The paper [START_REF] Esparza | Synthesis of distributed algorithms using asynchronous automata[END_REF] addresses the problem of synthesizing deadlock-free asynchronous automata from regular specifications. It remains to define a notion of deadlockfreeness for our setting and to study if the ideas from [START_REF] Esparza | Synthesis of distributed algorithms using asynchronous automata[END_REF] can be adopted.

Fig. 1 .Definition 5 .

 15 Fig. 1. A concurrent visibly pushdown automaton

  is said to be I-diamond if, for all pairs (α, β) ∈ I ∼ e Ω and all transitions r α → s β → t, we have transitions r β → s ′ α

Theorem 11 .

 11 Let A be an Mvpa over Σ such that L(A) is ∼ e Σ -closed. There is a Cvpa C = ((S p ) p∈Proc , Γ, (δ a ) a∈Σ , ι, F ) over Σ satisfying L(C) = L(A).For all p ∈ Proc, |S p | is doubly exponential in |A| and triply exponential in |Σ|.

Theorem 13 .

 13 Let k ∈ N and let A be an Mvpa over Σ such that L k (A) is a k-phase representation. There is a Cvpa C = ((S p ) p∈Proc , Γ, (δ a ) a∈Σ , ι, F ) over Σ such that L(C) = [L k (A)] ∼ e Σ .For all p ∈ Proc, |S p | is doubly exponential in |A| and k, and triply exponential in |Σ|.

Example 16 .

 16 Figure 2 depicts T = T e Σ (a b a b a b a a b b) = T e Σ (a b a b a b b b a a) where Σ is taken from Example 1. Hereby, the straight edges form the cover relation ≺ \ ≺ 2 of the underlying partial-order relation , and the curved edges represent µ, i.e., the matching pairs. There are two unmatched events in T .

  is a 2-phase trace, even though we have T = T e Σ (w) for w = a b a b a b a b a b ∈ W 2 ( Σ). The domain of k-phase traces is particularly interesting, because it is decidable whether L (C) ∩ Tr k ( Σ) = ∅ holds for a Cvpa C. To see this, observe that the latter holds iff L(C) ∩ W k ( Σ) = ∅, which is decidable according to Theorem 3.

Theorem 21 .

 21 Let k ∈ N. For every sentence ϕ ∈ MSO( Σ), there is a Cvpa C over Σ such that L (C) = L (ϕ) ∩ Tr k ( Σ).

⋆ Partially supported by ARCUS, DOTS (ANR-06-SETIN-003), and P2R MODISTE-COVER/RNP Timed-DISCOVERI.

shown for Mvpa in [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]). Thus, there is a Cvpa C ′ over Σ such that L(C ′ ) = f ([L(B)] ∼ e Ω ) (where f is canonically extended to words and, then, to languages). As When we restrict to k-phase words, it is actually decidable whether the previous theorems are applicable to a given Mvpa: Theorem 15. The following problems are decidable in elementary time:

Proof. Our proof is inspired by [START_REF] Peled | An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages[END_REF] where similar problems are addressed in the finite setting. The main difficulty, however, arises from the presence of stacks.

We first show decidability of Question 1. Let k ∈ N and let furthermore

). We will now construct an Mvpa A over Σ recognizing words of the form uabv with u, v ∈ Σ * , (a, b) ∈ I e Σ , and both uabv ∈ L(A 1 ) and ubav ∈ L(A 2 ). Thus, if L(A) contains a k-phase word uabv, then uabv is contained in L k (A 1 ) and ubav (which is a (k + 2)-phase word) is equivalent to uabv, but not contained in L k (A 1 ). Indeed,

The latter question is decidable (Theorem 3).

The set of states of A is S 1 ×S 2 ×({0, 1} ∪ (I e Σ ×Γ 2 ×Γ 2 )). The first component of a state is used to simulate A 1 , while the second component simulates A 2 . The third component starts in 0. In states of the form (s 1 , s 2 , 0), both automata proceed synchronously: Reading a ∈ Σ, A applies a-transitions (s 1 , a, A 1 , s ′ 1 ) ∈ δ 1 and (s 2 , a, A 2 , s ′

2 ) ∈ δ 2 to the first and the second component, respectively, resulting in a global step ((s 1 , s 2 , 0), a, (A 1 , A 2 ), (s ′ 1 , s ′ 2 , 0)). The stack alphabet is extended to Γ 1 × Γ 2 to take into account that A 1 and A 2 can be different.

When reading an input word, A 1 should eventually perform an action sequence ab with (a, b) ∈ I e Σ , while A 2 executes ba. So suppose A is about to simulate transitions (s 1 , a, A 1 , s ′ 1 ) followed by (s

The global automaton A will produce this transition sequence "crosswise". It will first read the a and apply the transition involving A 1 ∈ Γ 1 to the first component. At the same time, the second component only changes its local state into s ′ 2 . As the stack symbol B 2 cannot be applied directly, it is stored in the third component of the subsequent global state of A, which is of the form (s ′ 1 , s ′ 2 , ((a, b), B 2 , A 2 )). Observe that A 2 , which