Realizability of concurrent recursive programs

Abstract

We study the realizability problem for concurrent recursive programs: given a distributed system architecture and a sequential specification over words, find a distributed automata implementation that is equivalent to the specification. This problem is well-studied as far as finite-state processes are concerned, and it has a solution in terms of Zielonka’s Theorem. We lift Zielonka’s Theorem to the case where processes are recursive and modeled as visibly pushdown (or, equivalently, nested-word) automata. However, contrarily to the finite-state case, it is undecidable whether a specification is realizable or not. Therefore, we also consider suitable underapproximation techniques from the literature developed for multi-pushdown systems, and we show that they lead to a realizability framework with effective algorithms.

1 Introduction

The realizability problem arises when we are given a specification that we would like to transform into an implementation in terms of an automaton model. So, the first question to ask is if there is such an implementation at all. Famous instances of that problem are the Kleene Theorem and the Büchi–Elgot–Trakhtenbrot Theorem saying that, roughly speaking, all regular specifications are realizable. In Fig. 1, three equivalent specifications are given (from top to bottom: an LTL formula, a regular expression, a first-order formula) as well as an implementation in terms of a finite automaton.

Fig. 1

Realizability of sequential finite-state systems

While, as far as regular languages and their various representations are concerned, any specification has an implementation, the situation is more difficult when we move to a concurrent setting. Let us look at a well-studied model of concurrent shared-memory systems with finite-state processes, which we later refer to as Zielonka automata [46]. Suppose that we have two processes, 1 and 2, where 1 executes action a, and 2 executes action b. Consider Fig. 2. Is it justified to say that the concurrent automaton on the right-hand side, with no communication between processes 1 and 2, is an implementation of the regular expression $\alpha = ab(ab)^*$ ? There are (at least) two arguments against it. Expression $\alpha$ implies that any execution performs as many a’s as b’s. But this is not realizable under the architecture that we consider (recall that 1 and 2 do not communicate). Moreover, b’s have to be preceded by a’s, which is not realizable for the same reason. Note that these problems are inherent to the specifications and will not vanish with a more clever implementation. So, what is the “right” formalism for the specification of such systems? Or, put differently, what are the specifications that, unlike $ab(ab)^*$, are realizable?

Fig. 2

(Non-)realizability of concurrent finite-state systems

Fig. 3

Realizability of concurrent finite-state systems

Consider Fig. 3, and suppose that the system provides a third action, call it c, that is executed simultaneously by both processes. The concurrent automaton on the right-hand side might then be seen as an implementation of the regular expression on the left. First, the action c allows both processes to synchronize after each a-step (b-step, respectively), so that, in particular, there are as many a’s as b’s in any execution. Second, the order of executing a and b is not fixed anymore by the specification. Indeed, a classical result of Mazurkiewicz trace theory due to Zielonka states that regular specifications that are closed under permutation of such independent actions can be effectively translated into a concurrent automaton [46]. Note that the specification from Fig. 2 is actually not closed in that sense (it contains ab, but not ba), while the specification from Fig. 3 is closed. Similar results were obtained in the static message-passing setting [11, 17, 21, 22] for finite-state processes communicating via (existentially or universally) bounded FIFO channels.

In this paper, we obtain a generalization of Zielonka’s theorem for concurrent recursive (as opposed to finite-state) programs. A system is recursive if a process may suspend its activity and invoke (or, call) a subtask, before proceeding (or, returning). A stack is used to store the current configuration of the process, and to recover it once the subtask has been completed. The programs we consider are boolean, i.e., possible variables range over a finite domain. This implies that the set of states and the alphabet of stack symbols are finite. Boolean programs, in turn, may arise as abstractions from programs with infinite-domain variables. Such an extension is interesting from a theoretical but also from a practical point of view. Zielonka’s theorem allows for automatic implementations of sequential specifications such as mutual exclusion properties, which are easy to specify in a sequential, linearization-based language, but hard to transfer to a distributed setting. These properties are, of course, not restricted to finite-state processes but may involve recursive procedures. It would be interesting to extend the case-studies from [42] in that respect.

In fact, recursive processes may be defined in several equivalent ways. The classical definition is in terms of a pushdown automaton with explicit stacks. A run is then a sequence of configurations that keep track of the current stack contents. Alternatively, automata may run on words enriched with nesting relations [5], one for each process. A nesting relation connects a call position with the corresponding return position. In that case, a transition of the automaton that performs a return will depend on the state/stack symbol associated with the corresponding call position. It is then sufficient to define a run as a sequence of states, without explicitly mentioning the stack contents. This is the approach adopted in this paper. Note that automata over words (or partial orders) that include one or several nesting relations are equivalent to visibly pushdown automata (cf. again [5]) where each action is associated with a unique stack operation. Generally, nested-word automata/visibly pushdown automata are more robust than classical pushdown automata (they are complementable and closed under intersection), and our results crucially rely on this robustness.

Since the realizability question amounts to asking whether a specification can be translated into an automaton at all, we would like to distinguish, algorithmically, between the specifications from Fig. 2 (not realizable) and Fig. 3 (realizable). The question is decidable for finite-state systems [37, 40], but, unfortunately, it is undecidable in the recursive case, which follows from the undecidability of the nonemptiness problem. We will, therefore, identify sufficient decidable criteria that still guarantee realizability.

A fruitful approach to recover decidability in the realm of verification has been to restrict the possible system executions, for example by imposing a bound on the number of context switches, a notion introduced in [41]. There, each context allows only one dedicated process to perform calls or returns. This amounts to underapproximating the complete system behavior. However, as calls and returns from different processes are possibly independent, the final implementation may still exhibit executions that do not fit into this restriction anymore. The notion of context switches has been relaxed in several orthogonal ways. Phase-bounded systems only restrict the number of switches between returns from different processes [25]. Scope-bounded systems, on the other hand, restrict the number of contexts that separate a call and its return [28]. Finally, ordered systems impose an ordering on the processes and allow only the first process with a pending call to perform a return [6]. All these underapproximations render basic verification and model-checking questions decidable, though with varying complexity. Interestingly, it was later shown that they all induce classes of graphs that have bounded tree-width, which yields a unifying proof technique [31, 36]. Relying on the corresponding decidability results, we show that realizability becomes decidable for context- and phase-bounded systems.

We then look at monadic second-order (MSO) logic, a specification formalism that does not distinguish between equivalent linearizations (like ab and ba) but is interpreted directly on the partial order induced by a system execution. The partial order induced by ab with a and b independent has two incomparable elements with labels a and b, respectively. Though an MSO specification does not necessarily guarantee realizability, it already rules out design errors that can a priori be avoided. Under the above-mentioned restrictions, we provide results in the spirit of the Büchi–Elgot–Trakhtenbrot Theorem, showing an effective equivalence between automata and MSO logic. This actually generalizes a result by Thomas for finite-state processes [44].

Outline The paper is organized as follows: Sect. 2 introduces nested-trace automata (NTAs), our model of concurrent recursive programs. Section 3 focuses on sequential specifications in terms of nested-word languages, and it presents the corresponding automata model of nested-word automata (NWAs). In Sect. 4, we consider realizability, i.e., the task of synthesizing an NTA from a given NWA specification. In doing so, we extend Zielonka’s Theorem to concurrent recursive programs. Section 5 first reviews known results on NWAs based on restrictions that render basic decision problems decidable and that will then be used to obtain decidable criteria for realizability. In Sect. 6, we provide a logical characterization of NTAs in terms of MSO logic. We conclude with Sect. 7, in which we suggest several directions for future work.

This is a revised and extended version of the FOSSACS’09 paper [9]. The presentation, however, is quite different, presenting the framework in terms of nested words and traces rather than classical words. Note that both views are, in a sense, equivalent, and proofs are not immediately affected. However, the current presentation simplifies some definitions and corresponds to nested-word automata as presented in the standard reference [5]. Since structures exhibit explicit nesting relations, it is also closer to the MSO characterization presented in Sect. 6. Finally, we extended some results to context-bounded behaviors, and some others to scope-bounded and ordered structures.

2 Nested traces and their automata

In this section, we present our model of a concurrent recursive program, where a fixed finite set of processes communicate via shared memory. As a single process is recursive and involves function calls and returns, its executions are not just words, but rather nested words [5]. A nested word extends a word over a finite alphabet by a nesting relation, connecting function calls with their respective returns. An execution of the whole program, which we call a nested trace, involves several processes. It can, thus, be described as a collection of nested words. Some of the word positions are “shared” by several nested words, which models the shared memory. Note that nested traces combine nested words and Mazurkiewicz traces [15, 33] in a straightforward manner. An example nested trace is depicted in Fig. 4.

Before we can define nested traces formally, we will have to fix an architecture, which determines the actions and processes of a system, the type of an action (call, return, or internal), and the attribution of an action to one or more processes. Fixing the type of an action implies that the nesting relations are uniquely determined by the underlying strings.

Definition 1

(Distributed call-return alphabet) A distributed call-return alphabet is a tuple $\tilde{\varSigma }= (\varSigma ,P, type , dom )$ where

• $\varSigma$ is the nonempty finite set of actions,

• $P$ is the nonempty finite set of processes,

• $type : \varSigma \rightarrow \{{\textsf {call}},{\textsf {ret}},{\textsf {int}}\}$ indicates the type of an action (for a given type $\tau \in \{{\textsf {call}},{\textsf {ret}},{\textsf {int}}\}$, we let $\varSigma _\tau \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}} type ^{-1}(\tau )$), and

• $dom : \varSigma \rightarrow 2^P$ associates with every action its domain, i.e., the set of processes that are involved in its execution.

We require that $dom (a) \ne \emptyset$ for all $a \in \varSigma$, and $| dom (a)| = 1$ for all $a \in \varSigma _{\textsf {call}}\mathrel {\cup } \varSigma _{\textsf {ret}}$. The latter condition will imply that synchronization is achieved via internal actions only.

Fig. 4

Nested trace $\mathsf {T}$

When $\varSigma = \varSigma _{\textsf {int}}$, then we say distributed alphabet instead of distributed call-return alphabet.

Definition 2

(Nested trace) A nested trace over the distributed call-return alphabet $\tilde{\varSigma }$ is a tuple $(E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda )$ where

• 1. $E$ is a finite set of events,

• 2. $\lambda : E\rightarrow \varSigma$ is the event-labeling function (given $\tau \in \{{\textsf {call}},{\textsf {ret}},{\textsf {int}}\}$ and $p \in P$, we let $E_\tau \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{e \in E \mid \lambda (e) \in \varSigma _\tau \}$ and $E_p \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{e \in E \mid p \in dom (\lambda (e))\}$),

• 3. for all $p \in P$, ${\lhd _p} \subseteq E_p \times E_p$ is the direct-sucessor relation of some (unique) total order on $E_p$, which we denote by $\mathord {\leqslant }_p$ (with strict part $<_p$), and

• 4. $\mathord {\lhd _{\textsf {cr}}} \subseteq E \times E$ is the call-return relation satisfying the following:

  • (a) $\mathord {\lhd _{\textsf {cr}}}$ induces a bijection between $E_{\textsf {call}}$ and $E_{\textsf {ret}}$,

  • (b) for all $(e,f) \in \mathord {\lhd _{\textsf {cr}}}$, there is $p \in P$ such that $e <_p f$,

  • (c) for all $(e_1,f_1),(e_2,f_2) \in \mathord {\lhd _{\textsf {cr}}}$ and $p \in P$ such that $e_1 \in E_p$, $e_2 \in E_p$, and $e_1<_p e_2 <_p f_1$, we have $f_2 <_p f_1$.

In addition, we require that ${\le } \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}({\lhd _{\textsf {cr}}} \cup \bigcup _{p \in P} \lhd _p)^*$ is a partial order.

Condition 4(a) implies that there are no pending calls or returns.¹ Condition 4(b) says that a call-return pair belongs to a unique process and that a call takes always place before its return. By Condition 4(c), the call-return relation of each process is well-nested.

The set of nested traces over $\tilde{\varSigma }$ is denoted by $\mathsf {NTr}(\tilde{\varSigma })$. We do not distinguish between isomorphic nested traces.

Example 1

Consider the distributed call-return alphabet $\tilde{\varSigma }= (\varSigma ,P, type , dom )$ given by $\varSigma = \{a_1,b_1,a_2,b_2,c\}$, $P= \{1,2\}$, $type (a_1) = type (a_2) = {\textsf {call}}$, $type (b_1) = type (b_2) = {\textsf {ret}}$, and $type (c) = {\textsf {int}}$, as well as $dom (a_1) = dom (b_1) = \{1\}$, $dom (a_2) = dom (b_2) = \{2\}$, and $dom (c) = \{1,2\}$. A nested trace over $\tilde{\varSigma }$ is depicted in Fig. 4. Curved edges represent the relation $\lhd _{\textsf {cr}}$. Moreover, straight edges with label $p \in P$ represent the process-successor relation $\lhd _p$.

Next, we define a distributed automata model running on nested traces, which is a mix of nested-word automata and Zielonka automata. Here, the term distributed reflects the fact that every process has its own local state space and transition relation. Actually, there is a transition relation for every action $a \in \varSigma$. A transition involving a can access the local state of any process from $dom (a)$, and modify it. Therefore, since $a \in \varSigma _{\textsf {call}}\mathrel {\cup } \varSigma _{\textsf {ret}}$ implies $| dom (a)| = 1$, executing a call or return action updates the local state of only one single component.

Definition 3

(NTA) A nested-trace automaton (NTA) over $\tilde{\varSigma }$ is a tuple $\mathcal {C}= ((S_p)_{p \in P},\varGamma ,\Delta ,\iota ,F)$ where

• the $S_p$ are disjoint finite sets of local states (for ${P'}\subseteq P$, we define $S_{P'}\mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\prod _{p \in {P'}} S_p$),

• $\varGamma$ is the nonempty finite set of stack symbols,

• $\iota \in S_P$ is the global initial state,

• $F \subseteq S_P$ is the set of global final states, and

• $\Delta = \Delta _{\textsf {call}}\uplus \Delta _{\textsf {ret}}\uplus \Delta _{\textsf {int}}$ is the transition relation, partitioned into

  • $\Delta _{\textsf {call}}\subseteq \bigcup _{p \in P} (S_p \times \varSigma _{\textsf {call}}\times \varGamma \times S_p)$,

  • $\Delta _{\textsf {ret}}\subseteq \bigcup _{p \in P} (S_p \times \varSigma _{\textsf {ret}}\times \varGamma \times S_p)$, and

  • $\Delta _{\textsf {int}}\subseteq \bigcup _{a \in \varSigma _{\textsf {int}}} (S_{ dom (a)} \times \{a\} \times S_{ dom (a)})$.

Let $\mathbb {S} = \bigcup _{{P'}\subseteq P} S_{P'}$. For $s \in \mathbb {S}$ and $p\in P$, we let $s_p$ be the p-th component of s (if it exists).

Suppose the automaton is about to read an event e of a nested trace with label $\lambda (e) = a$. If $a \in \varSigma _{\textsf {int}}$, a transition of the form $(s,a,s') \in \Delta _{\textsf {int}}$ lets process p move on from $s_p$ to $s_p'$, for all $p \in dom (a)$. Only one process is involved when $a \in \varSigma _{\textsf {call}}\cup \varSigma _{\textsf {ret}}$ and a transition of the form $(s,a,A,s') \in \Delta _{\textsf {call}}\cup \Delta _{\textsf {ret}}$ is applied. In addition, if $a \in \varSigma _{\textsf {call}}$, the call event e will be tagged with stack symbol A. The latter can be retrieved at the corresponding return position. More precisely, we require that, whenever $e \lhd _{\textsf {cr}}f$, the stack symbol chosen at e is the same as the stack symbol employed by the transition that is taken at position f. In a sense, this is equivalent to reading a stack symbol previously pushed onto a stack.

Fig. 5

Nested-trace automaton $\mathsf {C}$

A run of the NTA $\mathcal {C}$ on a nested trace $T= (E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NTr}(\tilde{\varSigma })$ will include a mapping $\rho : E \rightarrow \mathbb {S}$ such that $\rho (e) \in S_{ dom (\lambda (e))}$ for all $e \in E$. Intuitively, for process $p \in dom (\lambda (e))$, the component $\rho (e)_p$ is the state that p reaches after executing e. Before we specify when $\rho$ is actually part of a run, let us define another mapping $\rho ^-: E \rightarrow \mathbb {S}$ that also satisfies $\rho ^-(e) \in S_{ dom (\lambda (e))}$ for all $e \in E$. Here, the intuition is that $\rho ^-(e)$ collects the current source states of all processes that are involved in executing e. We let $\rho ^-(e) =(s_p)_{p \,\in \, dom (\lambda (e))}$ where

$$\begin{aligned} s_p = {\left\{ \begin{array}{ll} \iota _p &{} \mathrm{if }\, e \,\mathrm{is}\, \lhd _p\mathrm{-minimal}\\ \rho (f)_p &{} \mathrm{if }\, f \lhd _p e\,. \end{array}\right. } \end{aligned}$$

Recall that, hereby, $\rho (f)_p$ denotes the p-th component of $\rho (f) \in S_{ dom (\lambda (f))}$. This component indeed exists since $p \in dom (\lambda (f))$. Moreover, e is called $\lhd _p$-minimal ($\lhd _p$-maximal) if there is no $e' \in E_p$ such that $e' \lhd _p e$ (respectively, $e \lhd _p e'$). Now, we call the pair $(\rho ,\sigma )$, with $\sigma : E_{\textsf {call}}\cup E_{\textsf {ret}}\rightarrow \varGamma$, a run of $\mathcal {C}$ on $T$ if,

• for all $(e,f) \in \mathord {\lhd _{\textsf {cr}}}$, we have $\sigma (e) = \sigma (f)$, and

• for all $e \in E$, it holds²

  $$\begin{aligned} {\left\{ \begin{array}{ll} \big (\rho ^-(e)_p,\lambda (e),\sigma (e),\rho (e)_p\big )\in \Delta _{\textsf {call}}&{} \text { if } e \in E_{\textsf {call}}\cap E_p\\ \big (\rho ^-(e)_p,\lambda (e),\sigma (e),\rho (e)_p\big )\in \Delta _{\textsf {ret}}&{} \text { if } e \in E_{\textsf {ret}}\cap E_p\\ \big (\rho ^-(e),\lambda (e),\rho (e)\big )\in \Delta _{\textsf {int}}&{} \text { if } e \in E_{\textsf {int}}\,. \end{array}\right. }\end{aligned}$$

To determine if run $(\rho ,\sigma )$ is accepting, we look at the global final state reached at the end of a run. It collects, for all $p \in P$, the local state associated with the $\lhd _p$-maximal event, or $\iota _p$ if $E_p = \emptyset$. Formally, let $f = (f_p)_{p \in P} \in S_P$ be given by

$$\begin{aligned}f_p = {\left\{ \begin{array}{ll} \rho (e)_p &{} \,\mathrm{if}\, e \,\mathrm{is}\, \lhd _p\mathrm{-maximal}\\ \iota _p &{} \, {\mathrm{if}}\, E_p = \emptyset \,. \end{array}\right. } \end{aligned}$$

With this, we call $(\rho ,\sigma )$ accepting if $f \in F$. Finally, we denote by $L(\mathcal {C})$ the set of nested traces over $\tilde{\varSigma }$ that have an accepting run of $\mathcal {C}$.

Example 2

Again, we assume the distributed call-return alphabet $\tilde{\varSigma }$ from Example 1, with $P= \{1,2\}$. Consider the NTA $\mathsf {C}= ((S_p)_{p \in P},\{\$\},\Delta ,\iota ,F)$ over $\tilde{\varSigma }$ depicted in Fig. 5. Its components are given by $S_1 = \{s_0,s_1,s_2\}$, $S_2 = \{t_0,t_1,t_2\}$, $\iota = (s_0,t_0)$, $F = \{(s_2,t_2)\}$. The new feature compared to sequential automata are the synchronizing transitions from $\Delta _{\textsf {int}}$, which include $((s_i,t_i),c,(s_i,t_i))$ for all $i \in \{0,1,2\}$ as well as $((s_1,t_1),c,(s_2,t_2))$. Note that $\mathsf {C}$ is eventually forced to execute “concurrent” occurrences of $a_1$ and $a_2$: when one process moves on to $s_1$ or $t_1$, then executing c is no longer possible unless the other process catches up. The nested trace $\mathsf {T}$ from Fig. 4 is accepted by $\mathsf {C}$. Note that there are indeed concurrent occurrences of $a_1$ and $a_2$.

A special case of NTAs is given in the case of a distributed alphabet, i.e., when $\varSigma = \varSigma _{\textsf {int}}$. Then, an NTA is precisely an asynchronous automaton (also Zielonka automaton) [46], and a nested trace is actually a Mazurkiewicz trace. However, following our terminology, we rather call it a trace automaton. Since, in that case, all actions from $\varSigma$ have type ${\textsf {int}}$, the language of a trace automaton may indeed be seen as a set of Mazurkiewicz traces.

3 Multiply nested words and their automata

An NTA can be seen as a model of a concurrent system, with physically distributed processes, each of which has a local state space. On the specification side, on the other hand, it is natural to allow for some global view of the system, which facilitates the specification of what the system is supposed to do as a whole. This leads us to define nested-word automata. As opposed to NTAs, nested-word automata have one single state space, albeit preserving several stacks. Their behavior can be described as a set of nested words with multiple nesting relations. In fact, a nested word can be defined as a total order, or linearization, put on top of a given nested trace. Thus, it interleaves concurrent events performed by distinct processes.

Again, we fix a distributed call-return alphabet $\tilde{\varSigma }= (\varSigma ,P, type , dom )$. However, note that the concrete distribution of internal actions in terms of $dom$ only matters when we consider nested traces.

Definition 4

(Linearization) Let $T= (E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NTr}(\tilde{\varSigma })$. A linearization of $T$ is any structure of the form $W=(E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$ where $\lhd _\mathsf {+1}$ is the direct-successor relation of some total order on E such that $\bigcup _{p \in P} \lhd _p \subseteq {(\lhd _\mathsf {+1})}^*$. In particular, $W$ and $T$ share the same call-return relation.

By $lin (T)$, we denote the set of all linearizations of $T$. Extending this to languages $L \subseteq \mathsf {NTr}(\tilde{\varSigma })$, we let $lin (L) \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\bigcup _{T\in L} lin (T)$.

Now, the linearizations of nested traces are precisely what we call nested words. Formally, the set of nested words is given by $\mathsf {NW}(\tilde{\varSigma }) \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}} lin (\mathsf {NTr}(\tilde{\varSigma }))$. We do not distinguish isomorphic linearizations/nested words.

Example 3

Consider the distributed call-return alphabet $\tilde{\varSigma }$ from Example 1. Figure 6 shows a nested word over $\tilde{\varSigma }$. It is a linearization of the nested trace from Fig. 4. Straight edges represent the relation $\lhd _{\mathsf {+1}}$, whereas curved edges represent $\lhd _{\textsf {cr}}$.

Fig. 6

Nested word $\mathsf {W}$

Now, we consider automata that are suitable to represent global specifications of multi-threaded recursive programs. Though these automata use a set of stack symbols, they run, similarly to NTAs, directly on nested words so that stacks are implicitly given and not referred to explicitly (cf. [5]).

Definition 5

(NWA) A nested-word automaton (NWA) over $\tilde{\varSigma }$ is a tuple $\mathcal {A} = (S,\varGamma ,\Delta ,\iota ,F)$ where

• S is the nonempty finite set of states,

• $\varGamma$ is the nonempty finite set of stack symbols,

• $\iota \in S$ is the initial state,

• $F \subseteq S$ is the set of final states, and

• $\Delta = \Delta _{\textsf {call}}\uplus \Delta _{\textsf {ret}}\uplus \Delta _{\textsf {int}}$ is the transition relation, partitioned into

  • $\Delta _{\textsf {call}}\subseteq S \times \varSigma _{\textsf {call}}\times \varGamma \times S$,

  • $\Delta _{\textsf {ret}}\subseteq S \times \varSigma _{\textsf {ret}}\times \varGamma \times S$, and

  • $\Delta _{\textsf {int}}\subseteq S \times \varSigma _{\textsf {int}}\times S$.

The behavior of an NWA is defined similarly to the behavior of an NTA. Let $W=(E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$ be a nested word. Assume that $E= \{e_1,\ldots ,e_n\}$ with $e_1 \mathrel {\lhd _{\mathsf {+1}}} e_2 \mathrel {\lhd _{\mathsf {+1}}} \ldots \mathrel {\lhd _{\mathsf {+1}}} e_n$. A run of $\mathcal {A}$ on $W$ is a pair $(\rho ,\sigma )$ of mappings $\rho :E\rightarrow S$ and $\sigma : E_{\textsf {call}}\cup E_{\textsf {ret}}\rightarrow \varGamma$ such that,

• for all $(e,f) \in \mathord {\lhd _{\textsf {cr}}}$, we have $\sigma (e) = \sigma (f)$, and

• for every $i\in \{1,\ldots ,n\}$ (letting $\rho (e_0) = \iota$),

  $$\begin{aligned} {\left\{ \begin{array}{ll} \big (\rho (e_{i-1}),\lambda (e_i),\rho (e_i)\big )\in \Delta _{\textsf {int}}&{} \text { if } e_i \in E_{\textsf {int}}\\ \big (\rho (e_{i-1}),\lambda (e_i),\sigma (e_i),\rho (e_i)\big )\in \Delta _{\textsf {call}}\cup \Delta _{\textsf {ret}}&{} \text { if } e_i \in E_{\textsf {call}}\cup E_{\textsf {ret}}\,. \end{array}\right. } \end{aligned}$$

The run $(\rho ,\sigma )$ is accepting if $\rho (e_n) \in F$ (in particular, $\iota \in F$ if $n = 0$). The set of nested words over $\tilde{\varSigma }$ for which there is an accepting run is denoted by $L(\mathcal {A})$.

Example 4

An NWA $\mathsf {A}= (\{s_0,\ldots ,s_5\},\{\$\},\Delta ,s_0,\{s_5\})$ over the distributed call-return alphabet $\tilde{\varSigma }$ from Examples 1 and 3 is given in Fig. 7. The transitions are self-explanatory. For example, the set $\Delta _{\textsf {int}}$ contains $(s_3,c,s_4)$, and $\Delta _{\textsf {ret}}$ contains $(s_4,b_2,\$,s_5)$, which is indicated by the edge from $s_4$ to $s_5$ with label ${b_2}_{|\$}$. Note that $\mathsf {A}$ accepts those nested words that (i) contain an infix $a_1a_2$ or $a_2a_1$, (ii) have a call and a subsequent return phase, separated by some action c, and (iii) schedule returns of process 1 before those of process 2. The nested word over $\tilde{\varSigma }$ from Fig. 6 is accepted by $\mathsf {A}$.

Fig. 7

Nested-word automaton $\mathsf {A}$

It is easy to see that NWAs (and NTAs) are closed under union and intersection. This has to be seen in contrast to the fact that the class of context-free languages (CFLs) is not closed under intersection. The intuitive reason for this is that, in CFLs, actions are no longer “visibly”. Indeed, augmenting words by the nesting structure makes sure that, while simulating two NWAs, the automaton for intersection performs push and pop operations at the same positions of the input word.

Unfortunately, in the presence of at least two processes/stacks, most basic verification problems for NWAs are undecidable, such as nonemptiness. The following result is folklore (and, of course, carries over to NTAs):

Theorem 1

The following problem is undecidable:

In fact, one can easily simulate a two-counter machine based on two stacks, choosing $\tilde{\varSigma }$ such that $|P| = 2$. Note that the problem is decidable when $|P| = 1$, as then we deal with (visibly) context-free languages.

4 Realizability of NWA specifications

We will now start studying the realizability problem. Given an NWA, we would like to construct an NTA that represents the language of the NWA, but in a distributed environment. Of course, we have to define what “represents” means here, and we will also have to identify conditions under which a given NWA is realizable as an NTA at all.

Now, NTAs are a truly concurrent model as processes may evolve independently unless they perform synchronizing actions from $\varSigma _{\textsf {int}}$. NWAs, on the other hand, possess one single state space, and the global control may enforce an order even on a priori independent actions. Yet, there are tight connections between NTAs and NWAs. In Sect. 4.1, we will formalize that relation. Then, in Sect. 4.2, we consider realizability in a restricted, but well-known setting, namely without calls and returns. Finally, in Sects. 4.3 and 4.4, we study the realizability problem in full generality.

4.1 From traces to linearizations and back

Let $W=(E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$ be a nested word over $\tilde{\varSigma }$. The call-return relation $\lhd _{\textsf {cr}}$ is uniquely determined by the other ingredients of $W$. Let us formalize this and assume that $E= \{e_1,\ldots ,e_n\}$ with $e_1 \mathrel {\lhd _{\mathsf {+1}}} e_2 \mathrel {\lhd _{\mathsf {+1}}} \ldots \mathrel {\lhd _{\mathsf {+1}}} e_n$. The string of $W$ is defined as $string (W) \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\lambda (e_1) \ldots \lambda (e_n) \in \varSigma ^*$. For example, for the nested word $\mathsf {W}$ from Fig. 6, we have $string (\mathsf {W}) = a_1ca_2a_1ca_2cb_1cb_1b_2b_2$. Now, given any word $w \in \varSigma ^*$, there is at most one (up to isomorphism) nested word $W$ over $\tilde{\varSigma }$ such that $string (W) = w$. If it exists, then we denote it by $nested (w)$. Note that, for any nested word W, we have $nested ( string (W)) = W$. For languages $L \subseteq \mathsf {NW}(\tilde{\varSigma })$, we set $string (L) = \{ string (W) \mid W \in L\}$.

Given $W\in \mathsf {NW}(\tilde{\varSigma })$, there is a unique nested trace $T\in \mathsf {NTr}(\tilde{\varSigma })$ such that $W\in lin (T)$. We denote this trace by $trace (W)$. Again, this is extended to languages $L \subseteq \mathsf {NW}(\tilde{\varSigma })$, and we set $trace (L) = \{ trace (W) \mid W \in L\}$. The relation between the mappings $string$ and $nested$ as well as $lin$ and $trace$ is illustrated in Fig. 8.

Fig. 8

Relation between strings, nested words, and nested traces

Since $nested ( string (W)) = W$ for any nested word W, we may consider the set of linearizations of $T$ as a string language over $\varSigma$. This will facilitate some definitions when we consider languages up to a congruence relation taking into account that some actions are independent (those that do not share processes), while others are not (those that have at least one process in common).

Independence relation Given $\tilde{\varSigma }$, we consider the classical independence relation $I_{\tilde{\varSigma }} \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{(a,b) \in \varSigma \times \varSigma \mid dom (a) \cap dom (b) = \emptyset \}$. Note that $I_{\tilde{\varSigma }}$ is irreflexive and symmetric. Its complement is the dependence relation $D_{\tilde{\varSigma }} \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}(\varSigma \times \varSigma ) {\setminus } I_{\tilde{\varSigma }}$, which is then reflexive and symmetric. With this, let $\mathord {\sim _{\tilde{\varSigma }}} \subseteq \varSigma ^*\times \varSigma ^*$ be the least congruence relation that satisfies $ab \sim _{\tilde{\varSigma }} ba$ for all $(a,b) \in I_{\tilde{\varSigma }}$.

For instance, if $\tilde{\varSigma }$ is the distributed call-return alphabet from Example 3, then the set $\{a_1a_2cb_1b_2\,,\,a_2a_1cb_1b_2\,,\,a_1a_2cb_2b_1\,,\,a_2a_1cb_2b_1\}$ is an equivalence class of $\sim _{\tilde{\varSigma }}$.

The equivalence relation $\sim _{\tilde{\varSigma }}$ is lifted in the natural way to nested words: we let $W\sim _{\tilde{\varSigma }} W'$ if $string (W) \sim _{\tilde{\varSigma }} string (W')$. Moreover, we say that $L \subseteq \mathsf {NW}(\tilde{\varSigma })$ is $\sim _{\tilde{\varSigma }}$ -closed if we have $L = [L]_{\tilde{\varSigma }} \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{W\in \mathsf {NW}(\tilde{\varSigma }) \mid W\sim _{\tilde{\varSigma }} W'$ for some $W' \in L\}$.

Realizability We will consider an NWA $\mathcal {A}$ to be a specification of a system, and we are looking for a realization or implementation of $\mathcal {A}$, which is provided by an NTA $\mathcal {C}$ such that $L(\mathcal {C}) = trace (L(\mathcal {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 according to the predefined system architecture $\tilde{\varSigma }$. Note that, unlike $lin (L(\mathcal {C}))$, the language $L(\mathcal {A})$ of an NWA $\mathcal {A}$ is not necessarily $\sim _{\tilde{\varSigma }}$-closed. However, $\mathcal {A}$ may yet be considered as an incomplete specification so that we can still ask for an NTA $\mathcal {C}$ such that $L(\mathcal {C}) = trace (L(\mathcal {A}))$.

Observe that it is easy to come up with an NWA recognizing the linearizations of the nested traces recognized by a given NTA. Essentially, the state space of the NWA is the Cartesian product of the local state spaces.

Lemma 1

Let $\mathcal {C}$ be an NTA over $\tilde{\varSigma }$. There is an NWA $\mathcal {A}$ over $\tilde{\varSigma }$ such that $L(\mathcal {A}) = lin (L(\mathcal {C}))$.

4.2 Realizability in the absence of stacks: well-known facts

We are, however, interested in the other direction, i.e., to transform a given NWA into an NTA. As a preparation, we now recall two well-known theorems from Mazurkiewicz trace theory. The first one, Zielonka’s celebrated theorem, applies to distributed call-return alphabets such that $\varSigma = \varSigma _{\textsf {int}}$. Below, it will be lifted to general distributed call-return alphabets.

Theorem 2

([46]) Suppose $\varSigma = \varSigma _{\textsf {int}}$. Let $\mathcal {A}$ be an NWA over $\tilde{\varSigma }$ such that $L(\mathcal {A})$ is $\sim _{\tilde{\varSigma }}$-closed. Then, there is an NTA $\mathcal {C}$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}) = trace (L(\mathcal {A}))$.

Note that the theorem actually yields a deterministic automaton $\mathcal {C}$ (we omit the definition of “deterministic”). The doubly exponential complexity (in the number of processes) of Zielonka’s construction has later been reduced to singly exponential [16, 19].

Moreover, again under the assumption $\varSigma = \varSigma _{\textsf {int}}$, closure of a word language under $\sim _{\tilde{\varSigma }}$ is a decidable criterion:

Theorem 3

([37, 40]) The following decision problem is Pspace-complete:

4.3 Realizability in the presence of stacks

In Theorems 2 and 3, the given NWA and the NTA do not employ any stack so that we actually deal with a finite and a Zielonka automaton, respectively. We can lift Zielonka’s theorem to distributed call-return alphabets:

Theorem 4

Let $\mathcal {A}$ be an NWA over $\tilde{\varSigma }$ such that the language $L(\mathcal {A})$ is $\sim _{\tilde{\varSigma }}$-closed. There is an NTA $\mathcal {C}$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}) = trace (L(\mathcal {A}))$.

Remark 1

The size of $\mathcal {C}$ is at most doubly exponential in $|\mathcal {A}|$ and triply exponential in $|\varSigma |$.

The proof is postponed to the next subsection. Theorem 4 demonstrates that NWAs, though they have a global view of the system in terms of one single state space, are suitable specifications for NTAs provided they recognize a $\sim _{\tilde{\varSigma }}$-closed language. Unfortunately, it is in general undecidable if the language of a given NWA is $\sim _{\tilde{\varSigma }}$-closed.

Theorem 5

The following problem is undecidable:

Proof

We proceed by a reduction from the undecidable emptiness problem (cf. Theorem 1). Let $\tilde{\varSigma }=(\varSigma ,P, type , dom )$ be the given distributed call-return alphabet and $\mathcal {A}= (S,\varGamma ,\Delta ,\iota ,F)$ be the given NWA over $\tilde{\varSigma }$. We assume $P = \{1,2\}$, as Theorem 1 already holds when we restrict to two processes. Moreover, we assume that $\mathcal {A}$ has a single final state f.

From the given $\tilde{\varSigma }$, we first define a new distributed call-return alphabet $\tilde{\varSigma }'=(\varSigma ',P, type ', dom ')$ where we simply add two independent internal actions a and b that do not occur in $\varSigma$. That is, $\varSigma ' = \varSigma \uplus \{a,b\}$, $type '(a) = type '(b) = {\textsf {int}}$, $dom '(a) = \{1\}$, and $dom '(b) = \{2\}$. On letters from $\varSigma$, $type '$ and $dom '$ behave like $type$ and $dom$, respectively.

Building on $\mathcal {A}$, we then define an NWA $\mathcal {A}'$ over $\tilde{\varSigma }'$. Essentially, $\mathcal {A}'$ coincides with $\mathcal {A}$. However, being in f, we allow $\mathcal {A}'$ to read ab and to then go into a new final state, while f is no longer final. Formally, $\mathcal {A}' = (S \uplus \{s_1,s_2\},\varGamma ,\Delta ',\iota ,\{s_2\})$ where $\Delta ' = \Delta \cup \{(f,a,s_1),(s_1,b,s_2)\}$.

We will show that $L(\mathcal {A}')$ is not $\sim _{\tilde{\varSigma }'}$-closed iff $L(\mathcal {A}) \ne \emptyset$. As the latter is undecidable by Theorem 1, this will conclude the proof. Of course, $L(\mathcal {A}) = \emptyset$ implies $L(\mathcal {A}') = \emptyset$ so that $L(\mathcal {A}')$ is trivially $\sim _{\tilde{\varSigma }'}$-closed. If, on the other hand, $L(\mathcal {A}) \ne \emptyset$, then f is reachable in $\mathcal {A}$ (formally, there is a nested word with an accepting run that ends in f). Thus, $\mathcal {A}'$ accepts some nested word whose associated string ends in ab. Since a and b do not occur elsewhere in $\mathcal {A}'$, the language $L(\mathcal {A}')$ cannot be $\sim _{\tilde{\varSigma }'}$-closed. $\square$

Interestingly, closure of a context-free language is undecidable, too [43, Theorem 4.32]. This result is orthogonal to ours, as the problem is again decidable for visibly pushdown languages (which can be shown by a simple adaptation of the proof from [37, 40]).

4.4 Proof of Theorem 4

We now develop the proof of Theorem 4. The theorem is actually a corollary of the more general Lemma 2 below, which uses the notion of a lexicographic normal form and is also used to prove a different result on NWA realizability based on underapproximations (Theorem 12 in Sect. 5 below).

Let us fix a strict total order $<_{{\textsf {lex}}}$ on $\varSigma$. Then, $<_{{\textsf {lex}}}$ naturally induces a strict lexicographic order on $\varSigma ^*$, which will also be denoted by $<_{{\textsf {lex}}}$.

We say that a nested word $W\in \mathsf {NW}(\tilde{\varSigma })$ is minimal if, for all nested words $W' \ne W$ that are equivalent to $W$ wrt. $\smash {\sim _{\tilde{\varSigma }}}$, we have $string (W) <_{{\textsf {lex}}} string (W')$. Given $W\in \mathsf {NW}(\tilde{\varSigma })$, let $nf _{\!{\textsf {lex}}}(W)$ denote its normal form, i.e., the unique minimal nested word $W' \in \mathsf {NW}(\tilde{\varSigma })$ such that $W \mathrel {\smash {\sim _{\tilde{\varSigma }}}} W'$. We extend the mapping $nf _{\!{\textsf {lex}}}$ to languages $L \subseteq \mathsf {NW}(\tilde{\varSigma })$ as expected and let $nf _{\!{\textsf {lex}}}(L) = \{ nf _{\!{\textsf {lex}}}(W) \mid W\in L\}$.

Theorem 6

([38]) Suppose $\varSigma = \varSigma _\mathrm{int}$ and let $L \subseteq \mathsf {NW}(\tilde{\varSigma })$ such that $string (L) \subseteq \varSigma ^*$ is regular and $nf _\mathrm{lex}(L) = L$. Then, there is an NWA $\mathcal {A}$ over $\tilde{\varSigma }$ such that $L(\mathcal {A}) = [L]_{\tilde{\varSigma }}$ (in other words, $[L]_{\tilde{\varSigma }}$ is a regular word language over the alphabet $\varSigma$).

We will use Theorems 2 and 6 to show the following crucial lemma:

Lemma 2

Let $\mathcal {A}$ be an NWA over $\tilde{\varSigma }$ such that $nf _\mathrm{lex}(L(\mathcal {A})) \subseteq L(\mathcal {A})$. Then, there is an NTA $\mathcal {C}$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}) = trace (L(\mathcal {A}))$.

Proof

We proceed in several steps. In a nutshell, we first interpret $\mathcal {A}$ as an NWA over a distributed alphabet (without any call or return actions). This allows us to apply the Theorems by Zielonka and Ochmański. Reinterpreting the resulting NTA over the modified alphabet as an NTA over the original alphabet, gives the desired automaton.

Let $\mathcal {A}= (S,\varGamma ,\Delta ,\iota ,F)$ be the given NWA with $nf _{\!{\textsf {lex}}}(L(\mathcal {A})) \subseteq L(\mathcal {A})$. We define the distributed alphabet as $\tilde{\varOmega } = (\varOmega ,P, type ', dom ')$ where $\varOmega = \varSigma \times \varGamma$ and, for all $(a,A) \in \varSigma \times \varGamma$, $type '((a,A)) = {\textsf {int}}$ and $dom '((a,A)) = dom (a)$. Note that $\varOmega = \varOmega _{\textsf {int}}$. Now, we proceed in several steps.

• 1. From the NWA $\mathcal {A}$ over $\tilde{\varSigma }$, we build an NWA $\mathcal {B}$ over $\tilde{\varOmega }$ as follows. A transition $(s,a,A,s') \in \Delta _{\textsf {call}}\mathrel {\cup } \Delta _{\textsf {ret}}$ in $\mathcal {A}$ is considered as a transition $(s,(a,A),s')$ in the new NWA $\mathcal {B}$, and a transition $(s,a,s') \in \Delta _{\textsf {int}}$ is translated to $(s,(a,A_a),s')$ with $A_a \in \varGamma$ arbitrary but fixed. The other components remain unchanged. Note that $\sim _{\tilde{\varSigma }}$-closure of $L(\mathcal {A})$ does not imply $\sim _{\tilde{\varOmega }}$-closure of $L(\mathcal {B})$, since, in $\mathcal {B}$, two transitions executing the same call/return action do not necessarily use the same stack symbol. To overcome this problem, we will go through lexicographic normal forms.

• 2. Fix any strict total order $<_{{\textsf {lex}}}'$ such that $a <_{{\textsf {lex}}}b$ implies $(a,A) <_{{\textsf {lex}}}' (b,B)$, for all $A,B \in \varGamma$. We know that $nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))$ is recognized by some finite automaton/NWA [38]. Thus, using a product construction, we find an NWA $\mathcal {B}'$ over $\tilde{\varOmega }$ such that

  $$\begin{aligned}L(\mathcal {B}') = L(\mathcal {B}) \cap nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega })). \end{aligned}$$

• 3. Since $\varOmega = \varOmega _{\textsf {int}}$, we can now apply Theorem 6 to obtain, from $\mathcal {B}'$, an NWA $\mathcal {B}''$ over $\tilde{\varOmega }$ such that

  $$\begin{aligned} L(\mathcal {B}'') = [L(\mathcal {B}) \cap nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))]_{\tilde{\varOmega }}. \end{aligned}$$

• 4. Next, we apply Theorem 2 to $\mathcal {B}''$ and get an NTA $\widehat{\mathcal {C}}$ over $\tilde{\varOmega }$ such that

  $$\begin{aligned} L(\widehat{\mathcal {C}}) = trace ([L(\mathcal {B}) \cap nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))]_{\tilde{\varOmega }}). \end{aligned}$$

• 5. The final step is to reinterpret $\widehat{\mathcal {C}}$ as an NTA $\mathcal {C}$ over the original alphabet $\tilde{\varSigma }$: Call or return transition $(s,(a,A),s')$ becomes $(s,a,A,s')$, and an internal transition $(s,(a,A_a),s')$ becomes $(s,a,s')$.

We show that $L(\mathcal {C}) = trace (L(\mathcal {A}))$.

To prove the inclusion from left to right, let $T= (E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda ) \in L(\mathcal {C})$. There is an accepting run $(\rho ,\sigma )$ of $\mathcal {C}$ on $T$. Recall that $\sigma : E_{\textsf {call}}\cup E_{\textsf {ret}}\rightarrow \varGamma$. Let $\widehat{\lambda }: E\rightarrow \varOmega$ be given by $\widehat{\lambda }(e) = (\lambda (e),\sigma (e))$ if $e \in E_{\textsf {call}}\cup E_{\textsf {ret}}$, and $\widehat{\lambda }(e) = (\lambda (e),A_{\lambda (e)})$ if $e \in E_{\textsf {int}}$. By the definition of $\mathcal {C}$, the (un)nested trace $\smash {\widehat{T}} = (E,(\lhd _p)_{p \in P},\emptyset ,\smash {\widehat{\lambda }})$ over $\smash {\tilde{\varOmega }}$ is contained in $L(\widehat{\mathcal {C}})$.

Since $L(\widehat{\mathcal {C}}) = trace ([L(\mathcal {B}) \cap nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))]_{\tilde{\varOmega }})$, there is a linearization $\widehat{W}= (E,\lhd _\mathsf {+1},\emptyset ,\widehat{\lambda })$ of $\widehat{T}$ such that $\widehat{W}\in L(\mathcal {B})$. Note that, as $\widehat{T}$ and $T$ share the same underlying partial order, $(E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NW}(\tilde{\varSigma })$ (with $\lhd _{\textsf {cr}}$ and $\lambda$ taken from T) is a linearization of T. Let $\rho '$ be an accepting run of the NWA $\mathcal {B}$ on $\widehat{W}$ (as there are only internal actions, a run does not need to map events to stack symbols). Since $\sigma$ is part of a run of the NTA $\mathcal {C}$ on $T$, we have $\sigma (e) = \sigma (f)$ for all $(e,f) \in {\lhd _{\textsf {cr}}}$. Moreover, $(\rho '(e),\widehat{\lambda }(f),\rho '(f))$ is a transition of $\mathcal {B}$, for all $(e,f) \in {\lhd _\mathsf {+1}}$. We deduce that $(\rho ',\sigma )$ is an accepting run of $\mathcal {A}$ on $(E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$. We conclude that $T=(E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda ) \in trace (L(\mathcal {A}))$.

For the converse direction, let $T= (E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda ) \in trace (L(\mathcal {A}))$. Let $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ) \in L(\mathcal {A})$ be the minimal linearization of $T$. Due to $nf _{\!{\textsf {lex}}}(L(\mathcal {A})) \subseteq L(\mathcal {A})$, we have $W\in L(\mathcal {A})$. Let $(\rho ,\sigma )$ be an accepting run of $\mathcal {A}$ on $W$ and suppose $\sigma '$ is the extension of $\sigma$ that maps every $e \in E_{\textsf {int}}$ to $A_{\lambda (e)}$. As $W$ is in lexicographic normal form wrt. $<_{{\textsf {lex}}}$ and $<_{{\textsf {lex}}}'$ is a conservative extension of $<_{{\textsf {lex}}}$, we have that $W' = (E,\lhd _\mathsf {+1},\emptyset ,(\lambda ,\sigma '))$ is in lexicographic normal form wrt. $<_{{\textsf {lex}}}'$. By the definition of $\mathcal {B}$, we have $W' \in L(\mathcal {B})$. Thus, we obtain $W' \in L(\mathcal {B}') = L(\mathcal {B}) \cap nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))$.

This implies $trace (W') = (E,(\lhd _p)_{p \in P},\emptyset ,(\lambda ,\sigma ')) \in trace (L(\mathcal {B}')) = L(\widehat{\mathcal {C}})$. Let $\rho '$ be an accepting run of $\widehat{\mathcal {C}}$ on $trace (W')$. As $\sigma '(e) = \sigma '(f)$ for all $(e,f) \in {\lhd }_{\textsf {cr}}$ and, moreover, $\sigma$ and $\sigma '$ coincide on $E_{\textsf {call}}\cup E_{\textsf {ret}}$, $(\rho ',\sigma )$ is an accepting run of $\mathcal {C}$ on $T=(E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda )$. We conclude $T \in L(\mathcal {C})$. $\square$

Remark 2

We will now argue that the size of $\mathcal {C}$ is at most doubly exponential in the size $|\mathcal {A}|$ of $\mathcal {A}$, and triply exponential in $|\varSigma |$. Hereby, we define $|\mathcal {A}|$ as $|S| + |\varGamma |$.

First, according to [23], there is an NWA with at most $(|\varSigma | + 1)!$-many states recognizing $nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))$. Thus, $\mathcal {B}'$ is of size $n \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}|\mathcal {A}| \cdot (|\varSigma | + 1)!$. Note that the size of the construction in [23] actually depends on $|\varSigma |$ rather than $|\varOmega |$.

The NWA for $nf _{\!{\textsf {lex}}}(\mathsf {NW}(\tilde{\varOmega }))$ and, therefore, $\mathcal {B}'$ have the property of being loop-connected [38]. The size of $\mathcal {B}''$ can therefore be bounded by $N \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}(n^2 \cdot 2^{|\varSigma |})^{(n-1)(|\varSigma | + 1) + 1}$ [23, 35]. From [19], we know that the size of $\widehat{\mathcal {C}}$ can be bounded by $2^{N^2 \cdot (|\varSigma |^2 + |\varSigma |) + 2|\varSigma |^4}$. As $\widehat{\mathcal {C}}$ and $\mathcal {C}$ have the same states, we conclude that the size of $\mathcal {C}$ is doubly exponential in $|\mathcal {A}|$ and triply exponential in $|\varSigma |$.

Note that this upper bound is obtained via a series of reductions that all assume a worst-case complexity without any optimization. It is unlikely that, in practice, each of these worst-cases is encountered at the same time.

Now, Theorem 4 is a corollary from Lemma 2, since we have $nf _{\!{\textsf {lex}}}(L(\mathcal {A})) \subseteq L(\mathcal {A})$ whenever $L(\mathcal {A})$ is $\sim _{\tilde{\varSigma }}$-closed.

5 Realizability of restricted specifications

Despite the extension of Zielonka’s theorem that we obtained in terms of Theorem 4, the undecidability result stated in Theorem 5 is unsatisfactory. In this section, we will impose restrictions on NWA specifications that allow us to combine a Zielonka-like theorem with decidable criteria for realizability.

5.1 Contexts, phases, scopes, and ordered stacks

In their seminal paper [41], Qadeer and Rehof exploited the fact that errors of recursive programs typically occur already within a few contexts where a context refers to an execution involving only one process. Imposing a bound on the number of contexts indeed renders many verification problems decidable. In other words, instead of looking at all possible executions, we consider an underapproximation of the actual system behavior. This view is particularly suitable when checking positive specifications: If a system $\mathcal {A}$ is required to exhibit all behaviors given by a set $Good$, then it is sufficient to show that $Good \subseteq L(\mathcal {U})$ is true for a restricted version $\mathcal {U}$ of $\mathcal {A}$ such that $L(\mathcal {U}) \subseteq L(\mathcal {A})$. Thus, we are interested in restrictions $\mathcal {U}$ of $\mathcal {A}$ such that the inclusion problem $Good \subseteq L(\mathcal {U})$ is decidable and that we may adjust incrementally so as to converge to $L(\mathcal {A})$. On the other hand, given a negative specification (or, safety property) $Bad$, we can also draw conclusions from $L(\mathcal {U}) \cap Bad \ne \emptyset$, while showing complete absence of bad behaviors would require an overapproximation of the system behavior.

Next, we recall the notion of a context as well as similar notions that have been defined in the literature. Let $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NW}(\tilde{\varSigma })$ be a nested word, and let ${\le } \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}(\lhd _\mathsf {+1})^*$, with strict part <. An interval of $W$ is a set $I \subseteq E$ such that $I = \emptyset$ or $I = [e,f] \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{g \in E \mid e \le g \le f\}$ for some $e,f \in E$. In a context, only one designated process is allowed to call or return, while a phase only restricts return operations:

• A context of $W$ is an interval I such that $I \cap (E_{\textsf {call}}\cup E_{\textsf {ret}}) \subseteq E_p$ for some $p \in P$.

• A phase of $W$ is an interval I such that $I \cap E_{\textsf {ret}}\subseteq E_p$ for some $p \in P$.

Definition 6

($k$-context word [41] and $k$-phase word [25]) Let $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$ be a nested word and $k\ge 1$. We say that $W$ is a $k$ -context word ($k$-phase word) if there are contexts (phases, respectively) $I_1,\ldots ,I_k$ of $W$ such that $E = I_1 \cup \ldots \cup I_k$.

Note that every context is a phase, while the converse does not hold in general. Therefore, every $k$-context word is a $k$-phase word, but not the other way around. Two orthogonal restrictions have been defined in terms of bounded scopes and ordered nested words, which we consider next. A scope-bounded word restricts the number of contexts between a push and the corresponding pop operation.

Definition 7

($k$-scope word [28]) Let $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$ be a nested word and $k\ge 1$. We call $W$ a $k$ -scope word if, for all $(e,f) \in \mathord {\lhd _{\textsf {cr}}}$, there exist contexts $I_1,\ldots ,I_k$ of $W$ such that $[e,f] = I_1 \cup \ldots \cup I_k$.

Finally, in an ordered word, we refer to a fixed total ordering $\preceq$ on $P$ (with irreflexive part $\prec$). Then, a pop operation can only be performed by the process that is minimal among all processes with a nonempty stack.

Definition 8

(Ordered word [6]) Let $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda )$ be a nested word. We call $W$ an ordered word (wrt. $\preceq$) if, for all $p,p' \in P$, $e,f \in E_p$, and $f' \in E_{\textsf {ret}}\cap E_{p'}$ such that $e \lhd _{\textsf {cr}}f$ and $e< f' < f$, we have $p' \preceq p$.

Example 5

(Continues Example 3) Figure 9 illustrates the concepts introduced above by means of the nested word $\mathsf {W}$ from Fig. 6. The shadowed areas are dedicated to process 2. Thus, $\mathsf {W}$ is a 6-context word, a 5-scope word, and a 2-phase word. All these bounds are optimal. Moreover, $\mathsf {W}$ is an ordered word under the assumption $1 \prec 2$ (but not for $2 \prec 1$).

Fig. 9

Illustration of context, phase, and scope

Let $\mathfrak {R}\mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{k\hbox {-}\mathsf {cnt}\,,\,k\hbox {-}\mathsf {ph}\,,\,k\hbox {-}\mathsf {scp} \mid k\ge 1\} \cup \{\mathsf {ord}\}$ be the set of possible “restrictions”. For $\theta \in \mathfrak {R}$, the set of $\theta$-words is denoted by $\mathsf {NW}_\theta (\tilde{\varSigma })$. In particular, by $\mathsf {NW}_\mathsf {ord}(\tilde{\varSigma })$, we denote the set of ordered words, silently assuming a total order on $P$. Moreover, for an NWA $\mathcal {A}$ over $\tilde{\varSigma }$, we let $L_\theta (\mathcal {A}) \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}L(\mathcal {A}) \cap \mathsf {NW}_\theta (\tilde{\varSigma })$.

Example 6

Consider the sample NWA $\mathsf {A}$ from Fig. 7. We have that $L(\mathsf {A}) = L_{2\hbox {-}\mathsf {ph}}(\mathsf {A}) = L_\mathsf {ord}(\mathsf {A})$. On the other hand, $L_{k\hbox {-}\mathsf {cnt}}(\mathsf {A})$ and $L_{k\hbox {-}\mathsf {scp}}(\mathsf {A})$ are strictly included in $L(\mathsf {A})$, for all $k\ge 1$.

Let us consider the respective nonemptiness problems, given in Table 1. In all cases, we assume that the parameter k is given in unary. Indeed, all problems are decidable, with varying complexities. For a comparison between the effects of a unary and a binary encoding of k, see [8].

Theorem 7

([32, 41]) Context-Nonemptiness is NP-complete.

Theorem 8

([25, 27]) Phase-Nonemptiness is $2$-Exptime-complete.

Theorem 9

([28]) Scope-Nonemptiness is Pspace-complete.

Theorem 10

([1]) Ord-Nonemptiness is $2$-Exptime-complete.

In [36], Madhusudan and Parlato give a uniform argument for decidability of the above problems: For $\theta \in \{k\hbox {-}\mathsf {cnt}\,,\,k\hbox {-}\mathsf {ph} \mid k\ge 1\} \mathrel {\cup } \{\mathsf {ord}\}$, the class of $\theta$-words has bounded tree-width. By Courcelle’s theorem, this implies that nonemptiness of NWAs and even model-checking of NWAs against MSO properties is decidable. It was then shown that scope-bounded words have bounded tree-width, too [31].

Table 1 Underapproximate decision problems

An alternative unifying approach is given in [13] in terms of the notion of split-width. Originally introduced for multiply nested words, split-width has also produced generalizations of the above-mentioned classes and other existing work on recursive message-passing systems [4, 14].

We have seen that restricting the domain of nested words appropriately renders the nonemptiness problem for NWAs decidable. These restrictions produce robust classes of languages. The next theorem states that, under any of the restrictions introduced above, NWAs are complementable:

Theorem 11

([25, 29, 30]) Let $\theta \in \mathfrak {R}$. For all NWAs $\mathcal {A}$ over $\tilde{\varSigma }$, the following hold:

• 1. There exists an NWA $\mathcal {A}'$ over $\tilde{\varSigma }$ such that $L(\mathcal {A}') = \mathsf {NW}_\theta (\tilde{\varSigma }) {\setminus } L(\mathcal {A})$.

• 2. There exists an NWA $\mathcal {A}'$ over $\tilde{\varSigma }$ such that $L(\mathcal {A}') = \mathsf {NW}(\tilde{\varSigma }) {\setminus } L_\theta (\mathcal {A})$.

5.2 Realizability of restricted specifications

In view of the undecidability result stated in Theorem 5, we will now consider realizability modulo restrictions to $\theta$-words, for suitable $\theta \in \mathfrak {R}$. This will allow us to define decidable sufficient criteria for the transformation of an NWA into an NTA. Moreover, there is a Zielonka-like theorem that is tailored to underapproximations. In that theorem, we require that an NWA represents the $\theta$-words of a system, while the final implementation can produce executions that do not fit into the $\theta$-restriction.

A $\theta$-representation is a set of nested words that does not distinguish between locally equivalent $\theta$-words. Here, two nested words $W,W' \in \mathsf {NW}({\tilde{\varSigma }})$ are said to be locally equivalent, written $W\sim _{\tilde{\varSigma }}^\mathrm{loc}W'$, if there are $u,v \in \varSigma ^*$ and $(a,b)\in I_{\tilde{\varSigma }}$ such that $string (W) = uabv$ and $string (W') = ubav$.

Definition 9

Let $\theta \in \mathfrak {R}$ and $L \subseteq \mathsf {NW}({\tilde{\varSigma }})$. We call L a $\theta$ -representation if $L \subseteq \mathsf {NW}_{\theta }({\tilde{\varSigma }})$ and, for all $W,W' \in \mathsf {NW}_\theta (\tilde{\varSigma })$ such that $W \sim _{\tilde{\varSigma }}^\mathrm{loc}W'$, we have $W\in L$ iff $W' \in L$.

We do not know whether the decidability result presented below (Theorem 13) still holds when considering a language L to be a $\theta$-representation if $L = [L]_{\tilde{\varSigma }} \cap \mathsf {NW}_\theta (\tilde{\varSigma })$.

Next, we present our Zielonka theorem suited to $\theta$-representations. Hereby, we require that $\theta$ be a member of the set $\mathfrak {R}^-\mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\{k\hbox {-}\mathsf {cnt}\,,\,k\hbox {-}\mathsf {ph} \mid k\ge 1\}$. The result relies on the definition of a lexicographic normal form that allows one to apply Ochmański’s Theorem [38]. The crux is that reordering independent events in order to obtain the lexicographic normal form shall not affect membership in the given $\theta$-representation. This, however, requires an extension of the underlying distributed call-return alphabet. While we do this for context- and phase-bounded executions, it is unclear whether it is possible for bounded-scope or ordered representations and if the following results holds for these classes as well.

Theorem 12

Let $\theta \in \mathfrak {R}^-$ be a restriction and let $\mathcal {A}$ be an NWA over $\tilde{\varSigma }$ such that $L_\theta (\mathcal {A})$ is a $\theta$-representation. Then, there is an NTA $\mathcal {C}$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}) = trace (L_\theta (\mathcal {A}))$.

Proof

Like in the proof of Theorem 4, we use Lemma 2. However, we cannot apply it directly, as it is in general not possible to define $<_{{\textsf {lex}}}$ in such a way that $nf _{\!{\textsf {lex}}}(L(\mathcal {A})) \subseteq L(\mathcal {A})$ when $L(\mathcal {A})$ is a $\theta$-representation, with $\theta \in \mathfrak {R}^-= \{k\hbox {-}\mathsf {cnt}\,,\,k\hbox {-}\mathsf {ph} \mid k\ge 1\}$. Our trick is to extend the given distributed call-return alphabet $\tilde{\varSigma }$ by a component that indicates the current context or phase of a word position. An appropriate definition of a lexicographic ordering over this extended alphabet will then allow us to apply Lemma 2.

Suppose $\tilde{\varSigma }=(\varSigma ,P, type , dom )$. For any restriction $\theta \in \mathfrak {R}^-$, we define a new distributed call-return alphabet $\tilde{\varOmega }_{\theta }=(\varOmega ,P, type ', dom ')$ as well as a lexicographic order in terms of a total order $\mathord {<_{{\textsf {lex}}}^\theta }$ on $\varOmega$.

• $\tilde{\varOmega }_{k\hbox {-}\mathsf {cnt}}$ is given as follows: Let $\varOmega = \varSigma _{\textsf {int}}\cup ((\varSigma _{\textsf {call}}\cup \varSigma _{\textsf {ret}}) \times \{1,\ldots ,k\})$. Intuitively, the additional component will keep track of the current context in a nested word. For $a \in \varSigma _{\textsf {int}}$, we set $type '(a) = type (a) = {\textsf {int}}$ and $dom '(a) = dom (a)$. For $a \in \varSigma _{\textsf {call}}\cup \varSigma _{\textsf {ret}}$ and $i \in \{1,\ldots ,k\}$, we let $type '((a,i)) = type (a)$ and $dom '((a,i)) = dom (a)$. Finally, let ${<_{{\textsf {lex}}}^{k\hbox {-}\mathsf {cnt}}} \subseteq \varOmega \times \varOmega$ be any strict total order such that $(a,i) <_{{\textsf {lex}}}^{k\hbox {-}\mathsf {cnt}}(b,j)$ whenever $i < j$.

• $\tilde{\varOmega }_{k\hbox {-}\mathsf {ph}}$ is given as follows: Let $\varOmega = \varSigma _{\textsf {call}}\cup \varSigma _{\textsf {int}}\cup (\varSigma _{\textsf {ret}}\times \{1,\ldots ,k\})$. Here, the additional component will keep track of the current phase. Therefore, it is only recorded for return events. For $a \in \varSigma _{\textsf {call}}\cup \varSigma _{\textsf {int}}$, we set $type '(a) = type (a)$ and $dom '(a) = dom (a)$. For $a \in \varSigma _{\textsf {ret}}$ and $i \in \{1,\ldots ,k\}$, we set $type '((a,i)) = type (a)$ and $dom '((a,i)) = dom (a)$. Again, let ${<_{{\textsf {lex}}}^{k\hbox {-}\mathsf {ph}}} \subseteq \varOmega \times \varOmega$ be any strict total order such that $(a,i) <_{{\textsf {lex}}}^{k\hbox {-}\mathsf {ph}}(b,j)$ whenever $i < j$.

For contexts and phases, we will now define the canonical, “greedy” division of a nested word into intervals. Given $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NW}(\tilde{\varSigma })$, we define a mapping $ph _W: E \rightarrow \mathbb {N}$ inductively as follows: If e is the minimal event of $W$ (wrt. $\le$), then we let $ph _W(e) = 1$ and we set $I_e = \{e\}$. Suppose $e \lhd _\mathsf {+1}f$. If $I_e \cup \{f\}$ is a phase, then let $ph _W(f) = ph _W(e)$ and $I_f = I_e \mathrel {\cup } \{f\}$. Otherwise, set $ph _W(f) = ph _W(e)+1$ and $I_f = \{f\}$. The mapping $ct _W: E \rightarrow \mathbb {N}$ for contexts is defined accordingly. Note that $W$ with maximal event e is a k-phase word iff $ph _W(e) \le k$. The corresponding statement holds for contexts.

Next, we define a mapping $h_{\theta }: \mathsf {NW}_\theta (\tilde{\varSigma }) \rightarrow \mathsf {NW}_\theta (\tilde{\varOmega }_{\theta })$. This mapping will add to a nested word additional information in terms of the extended alphabet (i.e., the context/phase).

• For a nested word $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NW}_{k\hbox {-}\mathsf {cnt}}(\tilde{\varSigma })$, we define $h_{k\hbox {-}\mathsf {cnt}}(W)$ as $(E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ')$ where $\lambda '(e) = \lambda (e)$ for all $e \in E_{\textsf {int}}$, and $\lambda '(e) = (\lambda (e), ct _W(e))$ for all $e \in E_{\textsf {call}}\cup E_{\textsf {ret}}$. Note that $h_{k\hbox {-}\mathsf {cnt}}(W)$ is indeed a $k$-context word over $\tilde{\varOmega }_{k\hbox {-}\mathsf {cnt}}$.

• Accordingly, for $W= (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NW}_{k\hbox {-}\mathsf {ph}}(\tilde{\varSigma })$, we let $h_{k\hbox {-}\mathsf {ph}}(W) = (E,\lhd _\mathsf {+1},\lhd _{\textsf {cr}},\lambda ')$ where $\lambda '(e) = \lambda (e)$ for all $e \in E_{\textsf {call}}\cup E_{\textsf {int}}$, and $\lambda '(e) = (\lambda (e), ph _W(e))$ for all $e \in E_{\textsf {ret}}$. Clearly, $h_{k\hbox {-}\mathsf {ph}}(W)$ is a $k$-phase word over $\tilde{\varOmega }_{k\hbox {-}\mathsf {ph}}$.

In the remainder of the proof, we proceed uniformly for all restrictions $\theta \in \mathfrak {R}^-$. Let $\mathcal {A}= (S,\varGamma ,\Delta ,\iota ,F)$ be the given NWA over $\tilde{\varSigma }$ such that $L_\theta (\mathcal {A})$ is a $\theta$-representation. One can easily construct an NWA $\mathcal {B}$ over $\tilde{\varOmega }_{\theta }$ such that $L(\mathcal {B}) = \{h_{\theta }(W) \mid W \in L_\theta (\mathcal {A})\} \subseteq \mathsf {NW}_\theta (\tilde{\varOmega }_{\theta })$. To do so, we just remember the current context/phase and its “type”. When reading a letter that does not correspond to the current type, the context/phase counter is increased.

We claim that $nf _{\!{\textsf {lex}}}(L(\mathcal {B})) \subseteq L(\mathcal {B})$ (where the mapping $nf _{\!{\textsf {lex}}}$ refers to $\mathord {<_{{\textsf {lex}}}^\theta }$). In other words, $L(\mathcal {B})$ contains, for every $W\in L(\mathcal {B})$, the normal form of $W$ wrt. $\mathord {<_{{\textsf {lex}}}^\theta }$. Let $g_\theta : \varOmega \rightarrow \varSigma$ define the projection that removes any additional labeling if it exists (i.e., $g_\theta ((a,i)) = a$) and which is canonically extended to nested words/traces and languages. Now, $\mathord {<_{{\textsf {lex}}}^\theta }$ has been chosen in such a way that the following holds, for all $W \in L(\mathcal {B})$. We obtain the normal form $W' \in \mathsf {NW}(\tilde{\varOmega }_{\theta })$ of W by successively reordering two independent neighboring events, without swapping the order of events with labels (a, i) and (b, j) such that $i < j$. Note that this implies $W' \in \mathsf {NW}_\theta (\tilde{\varOmega }_{\theta })$ and $h_\theta (g_\theta (W')) = W'$. Since $L_\theta (\mathcal {A})$ is a $\theta$-representation, the reordering also preserves containment in $L(\mathcal {B})$. Thus, $nf _{\!{\textsf {lex}}}(L(\mathcal {B})) \subseteq L(\mathcal {B})$.

By Lemma 2, there is an NTA $\mathcal {C}$ over $\tilde{\varOmega }_{\theta }$ such that $L(\mathcal {C}) = trace (L(\mathcal {B}))$. It is easily seen that NTAs are closed under projection (which was shown in [25] for NWAs). In particular, applying $g_\theta$ to an NTA language over $\tilde{\varOmega }_{\theta }$ yields an NTA language over $\tilde{\varSigma }$. Thus, there is an NTA $\mathcal {C}'$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}') = g_\theta ( trace (L(\mathcal {B})))$. As we have $g_\theta ( trace (L(\mathcal {B}))) = trace (g_\theta (L(\mathcal {B}))) = trace (L_\theta (\mathcal {A}))$, we are done. $\square$

5.3 Deciding realizability

To complete this section, we show that, given an NWA $\mathcal {A}$ over $\tilde{\varSigma }$ and a restriction $\theta \in \mathfrak {R}$ (now including “bounded scope” and “ordered”), we can decide both whether $L_\theta (\mathcal {A})$ is $\sim _{\tilde{\varSigma }}$-closed and whether $L_\theta (\mathcal {A})$ is a $\theta$-representation.

Theorem 13

The following problems are decidable in elementary time:

Proof

The proof is inspired by [37, 40] where analogous problems are addressed in a finite-state setting.

Consider first Question 1. Using Theorem 11, we first transform the given NWA $\mathcal {A}= (S_1,\varGamma _1,\Delta _1,\iota _1,F_1)$ into an NWA $\mathcal {A}' = (S_2,\varGamma _2,\Delta _2,\iota _2,F_2)$ for the complement, i.e., such that $L(\mathcal {A}') = \mathsf {NW}(\tilde{\varSigma }) {\setminus } L_\theta (\mathcal {A})$. Now, we build an NWA $\mathcal {B}$ recognizing all nested words $W\in L(\mathcal {A})$ where $string (W)$ is of the form uabv such that $(a,b) \in I_{\tilde{\varSigma }}$ and $ubav = string (W')$ for some $W' \in L(\mathcal {A}')$. Then, $L_\theta (\mathcal {A})$ is not $\sim _{\tilde{\varSigma }}$-closed iff $L_\theta (\mathcal {B}) \ne \emptyset$. The latter is decidable due to Theorems 7–10. To solve Question 2, the only difference is that we build $\mathcal {A}'$ such that $L(\mathcal {A}') = \mathsf {NW}_\theta (\tilde{\varSigma }) {\setminus } L(\mathcal {A})$ (again, using Theorem 11). In that case, $L_\theta (\mathcal {A})$ is not a $\theta$-representation iff $L_\theta (\mathcal {B}) \ne \emptyset$.

For convenience, we will write an internal transition $(s,a,s') \in \Delta _i$, $i \in \{1,2\}$, as $(s,a,A_a^i,s')$ where $A_a^i \in \varGamma _i$ is an arbitrary fixed stack symbol. The set of states of $\mathcal {B}$ is $S_1 \times S_2 \times (\{0,1\} \mathrel {\cup } (I_{\tilde{\varSigma }}\times \varGamma _2 \times \varGamma _2))$. The first two components of a state are used to simulate $\mathcal {A}$ and $\mathcal {A}'$, respectively. The third component starts in 0. In states of the form $(s_1,s_2,0)$, both automata proceed synchronously: Reading $a \in \varSigma$, $\mathcal {B}$ applies a-transitions $(s_1,a,A_1,s_1') \in \Delta _1$ and $(s_2,a,A_2,s_2') \in \Delta _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))$. Note that the stack alphabet is extended to $\varGamma _1 \times \varGamma _2$ to take into account that $A_1$ and $A_2$ are in general distinct.

When reading an input word, $\mathcal {A}$ should eventually perform an action sequence ab with $(a,b) \in I_{\tilde{\varSigma }}$, while $\mathcal {A}'$ executes ba. So suppose $\mathcal {B}$ is about to simulate transitions $(s_1,a,A_1,s_1')$ followed by $(s_1',b,B_1,s_1'')$ in $\mathcal {A}$ and transition $(s_2,b,B_2,s_2')$ followed by $(s_2',a,A_2,s_2'')$ in $\mathcal {A}'$. The global automaton $\mathcal {B}$ will produce this transition sequence “crosswise”. It will first read the a and apply the transition involving $A_1 \in \varGamma _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 $\mathcal {B}$, which is of the form $(s_1',s_2',((a,b),B_2,A_2))$. Observe that $A_2$, which is associated to executing a in $\mathcal {A}'$, must be applied together with reading a so that $(A_1,A_2)$ acts as the stack symbol. In fact, since a corresponding local transition $(s_2',a,A_2,s_2'')$ has to follow in $\mathcal {A}'$, the stack symbol $A_2$ needs to be stored as well. The formal description of this step can be found below (2). Now, being in the global state $(s_1',s_2',((a,b),B_2,A_2))$, $\mathcal {B}$ 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, $\mathcal {A}'$ will only change its local state into $s_2''$. However, the local transition has to conform to action a and 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, $\mathcal {A}$ and $\mathcal {A}'$ are again simulated in sync (rule (1)).

Formally, $\mathcal {B}= (S,\varGamma ,\Delta ,\iota ,F)$ is given by $S = S_1 \times S_2 \times (\{0,1\} \mathrel {\cup } (I_{\tilde{\varSigma }}\times \varGamma _2 \times \varGamma _2))$, $\varGamma = \varGamma _1 \times \varGamma _2$, $\iota = (\iota _1,\iota _2,0)$, and $F = F_1 \times F_2 \times \{1\}$.

Towards the transition relation $\Delta$, we first define a relation $\Delta ' \subseteq S \times \varSigma \times (\varGamma _1 \times \varGamma _2) \times S$. To obtain $\Delta$ from $\Delta '$, we then simply replace every transition of the form $(s,a,(A_1,A_2),s')$, $a \in \varSigma _{\textsf {int}}$, by $(s,a,s')$.

• (1) For $(s_1,a,A_1,s_1') \in \Delta _1$, $(s_2,a,A_2,s_2') \in \Delta _2$, and $\beta \in \{0,1\}$, the relation $\Delta '$ contains

  $$\begin{aligned} ((s_1,s_2,\beta ),a,(A_1,A_2),(s_1',s_2',\beta ))\,. \end{aligned}$$

• (2) For $(a,b) \in I_{\tilde{\varSigma }}$, $(s_1,a,A_1,s_1') \in \Delta _1$, $(s_2,b,B_2,s_2') \in \Delta _2$, and $A_2 \in \varGamma _2$, the relation $\Delta '$ contains

  $$\begin{aligned} ((s_1,s_2,0),a,(A_1,A_2),(s_1',s_2',((a,b),B_2,A_2)))\,. \end{aligned}$$

• (3) For $(a,b) \in I_{\tilde{\varSigma }}$, $(s_1,b,B_1,s_1') \in \Delta _1$, $(s_2,a,A_2,s_2') \in \Delta _2$, and $B_2 \in \varGamma _2$, the relation $\Delta '$ contains

  $$\begin{aligned} ((s_1,s_2,((a,b),B_2,A_2)),b,(B_1,B_2),(s_1',s_2',1))\,. \end{aligned}$$

Finally, we obtain $\Delta$ from $\Delta '$ as described above.

Since the constructions from Theorem 11 can be done in at most doubly exponential time, and since the decision problems from Theorems 7–10 are at most doubly exponential, too, we obtain elementary procedures for both Question 1 and Question 2. $\square$

6 Realizability of MSO specifications

In this section, we give a short introduction into monadic second-order (MSO) logic over nested traces. The logic is built over countably infinite supplies $\{x,y,x_1,x_2,\ldots \}$ of first-order and $\{X,Y,X_1,X_2,\ldots \}$ of second-order variables. First-order variables are interpreted as events, second-order variables as sets of events. As usual, the predicates available in MSO logic depend on the signature of a structure, which is given in terms of the distributed call-return alphabet $\tilde{\varSigma }= (\varSigma ,P, type , dom )$.

Definition 10

The formulas from ${\text {ntMSO}} (\tilde{\varSigma })$ are built according to the following grammar:

$$\begin{aligned} \begin{array}{rcl} &{}&{} \varphi \,{::=}\, a(x) ~\mid ~ x \mathrel {\lhd _p} y ~\mid ~ x \mathrel {\lhd _{\textsf {cr}}} y ~\mid ~ x = y ~\mid ~ x \in X ~\mid \\ &{}&{} \quad \qquad \lnot \varphi ~\mid ~ \varphi _1 \vee \varphi _2 ~\mid ~ \exists x. \varphi ~\mid ~ \exists X. \varphi \end{array} \end{aligned}$$

where $a \in \varSigma$, $p \in P$, x, y are first-order variables, and X is a second-order variable.

A formula $\varphi$ from the logic ${\text {ntMSO}} (\tilde{\varSigma })$ is interpreted over a nested trace $T=(E,(\lhd _p)_{p \in P},\lhd _{\textsf {cr}},\lambda ) \in \mathsf {NTr}(\tilde{\varSigma })$ wrt. a mapping $\mathcal {I}$. The purpose of the latter is to interpret free variables. It maps any first-order variable x to an event $\mathcal {I}(x) \in E$ and any second-order variable X to a set of events $\mathcal {I}(X) \subseteq E$. We write $T\models _\mathcal {I}\varphi$ if formula $\varphi$ is evaluated to true when the free variables of $\varphi$ are interpreted according to $\mathcal {I}$. In particular, we have $T\models _\mathcal {I}a(x)$ if $\lambda (\mathcal {I}(x)) = a$, $T\models _\mathcal {I}x \mathrel {\lhd _p} y$ if $\mathcal {I}(x) \mathrel {\lhd _p} \mathcal {I}(y)$, and $T\models _\mathcal {I}x \mathrel {\lhd _{\textsf {cr}}} y$ if $\mathcal {I}(x) \mathrel {\lhd _{\textsf {cr}}} \mathcal {I}(y)$. The remaining operators are interpreted as usual. When $\varphi$ is a sentence, i.e., a formula without free variables, we omit the index $\mathcal {I}$ and simply write $T\models \varphi$. The language $L(\varphi )$ is then defined as $\{T\in \mathsf {NTr}(\tilde{\varSigma }) \mid T\models \varphi \}$.

For a thorough introduction to MSO logic on (classical) words and its semantics, we refer the reader to [45].

Again, we will recall a well-known result for concurrent programs without stacks, and then lift it to the recursive setting.

Theorem 14

([44]) Suppose $\tilde{\varSigma }$ satisfies $\varSigma = \varSigma _{\textsf {int}}$, and let $L \subseteq \mathsf {NTr}(\tilde{\varSigma })$. The following statements are effectively equivalent:

• 1. There is an NTA $\mathcal {C}$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}) = L$.

• 2. There is a sentence $\varphi \in \mathrm{ntMSO}(\tilde{\varSigma })$ such that $L(\varphi ) = L$.

Note that this theorem cannot be lifted to nested traces without imposing any restriction. This is due to the fact that NWAs (and, therefore, NTAs) are not complementable [12], while MSO logic is closed under negation. However, it will turn out that restricting to $k$-context/$k$-phase traces also helps in this case.

Of course, given a restriction $\theta \in \mathfrak {R}$, we first have to clarify what we mean by a $\theta$ -trace. There are at least two reasonable possibilities. For example, we may call a nested trace $T$ a $\theta$-trace if all linearizations of $T$ are $\theta$-words. Alternatively, we may require that some linearization of T is a $\theta$-word. We will choose the latter, existential, definition, as it captures more nested traces. Note that there are similar options and definitions in the setting of message sequence charts under channel bounds [18, 24].

Formally, we call $T\in \mathsf {NTr}(\tilde{\varSigma })$ a $\theta$ -trace if $lin (T) \cap \mathsf {NW}_\theta (\tilde{\varSigma }) \ne \emptyset$. We adopt other notations from nested words and let $\mathsf {NTr}_\theta (\tilde{\varSigma })$ be the set of $\theta$-traces. Moreover, for an NTA $\mathcal {C}$, we let $L_\theta (\mathcal {C}) \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}L(\mathcal {C}) \mathrel {\cap } \mathsf {NTr}_\theta (\tilde{\varSigma })$. For a sentence $\varphi \in {\text {ntMSO}} (\tilde{\varSigma })$, the set $L_\theta (\varphi )$ is defined accordingly.

Example 7

The nested trace $\mathsf {T}$ from Fig. 4 is a 2-phase trace (it admits the 2-phase linearization $\mathsf {W}$ from Fig. 6), a 4-context trace, a 3-scope trace, and an ordered trace (since its linearization $\mathsf {W}$ is ordered).

As a preparation of a logical characterization of NTAs, we show that they are complementable for some restrictions of nested traces. This is an analogue of Theorem 11 for NWAs. As we rely on Theorem 12, we have to restrict to the set $\mathfrak {R}^-= \{k\hbox {-}\mathsf {cnt}\,,\,k\hbox {-}\mathsf {ph} \mid k\ge 1\}$, i.e., to boundedly many contexts or phases.

Lemma 3

Let $\theta \in \mathfrak {R}^-$ and let $\mathcal {C}$ be an NTA over $\tilde{\varSigma }$. Then, there is an NTA $\mathcal {C}'$ such that $L(\mathcal {C}') = \mathsf {NTr}_\theta (\tilde{\varSigma }) {\setminus } L(\mathcal {C})$.

Proof

From the given NTA $\mathcal {C}$, we get, using Lemma 1 and Theorem 11, an NWA $\mathcal {A}$ over ${\tilde{\varSigma }}$ such that $L(\mathcal {A}) = \mathsf {NW}_\theta (\tilde{\varSigma }) {\setminus } lin (L(\mathcal {C}))$. Observe that $L(\mathcal {A})$ is a $\theta$-representation. By Theorem 12, there is an NTA $\mathcal {C}'$ over ${\tilde{\varSigma }}$ such that $L(\mathcal {C}') = trace (L(\mathcal {A}))$. One easily verifies that $L(\mathcal {C}') = \mathsf {NTr}_\theta (\tilde{\varSigma }) {\setminus } L(\mathcal {C})$. $\square$

In particular, Lemma 3 implies that there is an NTA recognizing the set $\mathsf {NTr}_\theta (\tilde{\varSigma })$. The following theorem constitutes a generalization of Theorem 14 adapted to $\theta$-traces, where $\theta \in \mathfrak {R}^-$.

Theorem 15

The following implications are effective:

• 1. For every NTA $\mathcal {C}$ over $\tilde{\varSigma }$, there is a sentence $\varphi \in \mathrm{ntMSO}(\tilde{\varSigma })$ such that $L(\varphi ) = L(\mathcal {C})$.

• 2. Let $\theta \in \mathfrak {R}^-$. For every sentence $\varphi \in \mathrm{ntMSO}(\tilde{\varSigma })$, there is an NTA $\mathcal {C}$ over $\tilde{\varSigma }$ such that $L(\mathcal {C}) = L_\theta (\varphi )$.

Proof

The proof of 1. follows the standard construction for the translation of automata into logic. One guesses an assignment of states and stack symbols to events in terms of existentially quantified second-order variables. Then, a first-order kernel checks if the assignments actually correspond to an accepting run.

For the proof of 2., we proceed by structural induction. Hereby, the only critical case is negation, which will be taken care of by Lemma 3. For simplicity, we suppose that there are no free variables. To get an automaton for $\lnot \varphi$, suppose that we already have an NTA $\mathcal {C}$ such that $L(\mathcal {C}) = L_\theta (\varphi )$. By Lemma 3, there is an NTA $\mathcal {C}'$ such that $L(\mathcal {C}') = \mathsf {NTr}_\theta (\tilde{\varSigma }) {\setminus } L(\mathcal {C})$. We have $L(\mathcal {C}') = L_\theta (\lnot \varphi )$ so that we are done. $\square$

We conclude this section stating that model checking NTAs against MSO properties is decidable (albeit of inherently nonelementary complexity):

Theorem 16

The following problem is decidable:

Proof

The proof does not rely on Theorem 15, since this would only allows us to show the result for restrictions from $\mathfrak {R}^-$. Instead, we give a direct reduction to linearizations, i.e., to the case of nested words, where underapproximate model checking is decidable.

By Lemma 1, we can construct an NWA $\mathcal {A}$ over $\tilde{\varSigma }$ such that $L(\mathcal {A}) = lin (L(\mathcal {C}))$. Secondly, we translate the sentence $\varphi \in {\text {ntMSO}} (\tilde{\varSigma })$, inductively, into an MSO formula $\tilde{\varphi }$ over nested words such that $L(\tilde{\varphi }) = lin (L(\varphi ))$. We omit the formal definition of MSO over nested words. The only interesting case is $x \mathrel {\lhd _p} y$, which is translated to $p(x) \wedge p(y) \wedge x< y \wedge \lnot \exists z(p(z) \wedge x< z < y)$ where $p(x) \mathrel {\smash {\mathop {=}\limits ^{\scriptscriptstyle {\text {def}}}}}\bigvee _{a \in \varSigma _p} a(x)$ and < refers to the (MSO-definable) total order induced by a nested word.

Now, we have $L_\theta (\mathcal {C}) \subseteq L(\varphi )$ iff $L_\theta (\mathcal {A}) \subseteq L(\tilde{\varphi })$. The latter problem is decidable, which follows from Theorems 7–10 and the MSO characterizations of NWAs given in [25, 29, 30]. $\square$

The model-checking problem has been addressed in [7] for the phase-restriction and propositional dynamic logic (PDL) as specification language. Its complexity drops to EXPTIME when the bound on the number of phases is fixed. MSO-definable temporal logics have been considered in [10, 34] for various restrictions in a sequential setting. It is shown that the model-checking problem is still elementary even when the restriction (e.g., the bound on the number of phases) is part of the input.

7 Conclusion

Most results presented in this paper rely on specific restrictions of the domain of nested words. It will be worthwhile to study a more generic setting by bounding the tree-width or split-width. The model-checking question has been well-studied in [4, 13, 34], but not much is known about realizability.

Note that some realizable specifications will inevitably yield implementations in terms of NWAs that are nondeterministic and suffer from deadlocks. One should, therefore, study classes of NWAs that are arguably more “realistic” meaning, in particular, that they are deterministic and/or deadlock-free [2, 11, 42]. A natural question is then to ask for a specification formalism that guarantees such realistic implementations.

It also remains to study realizability in the realm of recursive processes communicating through FIFO channels [20, 26]. Here, the model-checking question is by now well understood, in particular thanks to the split-width technique [4, 14]. To the best of our knowledge, realizability questions for such communicating recursive processes have not been considered yet. The quest for controllers, whose study has been initiated in [3], seems to be closely related.

Recently, visibly pushdown trace languages have been characterized in terms of certain cooperating distributed systems (CD-systems) [39]. There, the dependence relation is independent of any partitioning into call, return, and internal actions. It would actually be interesting to see to which extent more general distributed call-return alphabets can be adopted in our setting.