key: cord-0060372-d9b07d9o
authors: Dixon, Alex; Lazić, Ranko; Murawski, Andrzej S.; Walukiewicz, Igor
title: Leafy automata for higher-order concurrency
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_10
sha: 6d37c4e33d234d8a5d4441b8f0f1f9648c51fc6a
doc_id: 60372
cord_uid: d9b07d9o

Finitary Idealized Concurrent Algol ([Formula: see text] ) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of [Formula: see text] , which in principle can be used to prove equivalence and safety of [Formula: see text] programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of [Formula: see text] . The automata use an infinite alphabet with a tree structure. We show that the game semantics of any [Formula: see text] term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a [Formula: see text] term. Because of the close match with [Formula: see text] , we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation. Moreover, we identify a fragment of [Formula: see text] that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability.

Game semantics is a versatile paradigm for giving semantics to a wide spectrum of programming languages [3, 35] . It is well-suited for studying the observational equivalence of programs and, more generally, the behaviour of a program in an arbitrary context. About 20 years ago, it was discovered that the game semantics of a program can sometimes be expressed by a finite automaton or another simple computational model [20] . This led to algorithmic uses of game semantics for program analysis and verification [1, 15, 21, 5, 27, 26, 28, 34, 16, 17] . Thus far, these advances concerned mostly languages without concurrency.

In this work, we consider Finitary Idealized Concurrent Algol (FICA) and its fully abstract game semantics [22] . It is a call-by-name language with higherorder features, side-effects, and concurrency implemented by a parallel composition operator and semaphores. It is finitary since, as it is common in this context, base types are restricted to finite domains. Quite surprisingly, the game semantics of this language is arguably simpler than that for the language without concurrency. The challenge comes from algorithmic considerations.

Following the successful approach from the sequential case [20, 37, 33, 36, 11] , the first step is to find an automaton model abstracting the phenomena appearing in the semantics. The second step is to obtain program fragments from structural restrictions on the automaton model. In this paper we take both steps.

We propose leafy automata: an automaton model working on nested data. Data are used to represent pointers in plays, while the nesting of data reflects structural dependencies in the use of pointers. Interestingly, the structural dependencies in plays boil down to imposing a tree structure on the data. We show a close correspondence between the automaton model and the game semantics of FICA. For every program, there is a leafy automaton whose traces (data words) represent precisely the plays in the semantics of the program (Theorem 3). Conversely, for every leafy automaton, there is a program whose semantics consists of plays representing the traces of the automaton (Theorem 5). (The latter result holds modulo a saturation condition we explain later.) This equivalence shows that leafy automata are a suitable model for studying decidability questions for FICA.

Not surprisingly, due to their close connection to FICA, leafy automata turn out to have an undecidable emptiness problem. We use the undecidability argument to identify the source, namely communication across several unbounded levels, i.e., levels in which nodes can produce an unbounded number of children during the lifetime of the automaton. To eliminate the problem, we introduce a restricted variant of leafy automata, called local, in which every other level is bounded and communication is allowed to cross only one unbounded node. Emptiness for such automata can be decided via reduction to a number of instances of Petri net reachability problem.

We also identify a fragment of FICA, dubbed local FICA (LFICA), which maps onto local leafy automata. It is based on restricting the distance between semaphore and variable declarations and their uses inside the term. This is a first non-rudimentary fragment of FICA for which some verification tasks are decidable. Overall, this makes it possible to use local leafy automata to analyse LFICA terms and decide associated verification tasks.

Related work Concurrency, even with only first-order recursion, leads to undecidability [39] . Intuitively, one can encode the intersection of languages of two pushdown automata. From the automata side, much research on decidable cases has concentrated on bounding interactions between stacks representing different threads of the program [38, 30, 4] . From the game semantics side, the only known decidable fragment of FICA is Syntactic Control of Concurrency (SCC) [23] , which imposes bounds on the number of threads in which arguments can be used. This restriction makes it possible to represent the game semantics of programs by finite automata. In our work, we propose automata models that correspond to unbounded interactions with arbitrary FICA contexts, and importantly that remains true also when we restrict the terms to LFICA. Leafy automata are a model of computation over an infinite alphabet. This area has been explored extensively, partly motivated by applications to database theory, notably XML [41] . In this context, nested data first appeared in [7] , where the authors considered shuffle expressions as the defining formalism. Later on, data automata [9] and class memory automata [8] have been adapted to nested data in [14, 12] . They are similar to leafy automata in that the automaton is allowed to access states related to previous uses of data values at various depths. What distinguishes leafy automata is that the lifetime of a data value is precisely defined and follows a question and answer discipline in correspondence with game semantics. Leafy automata also feature run-time "zero-tests", activated when reading answers.

For most models over nested data, the emptiness problem is undecidable. To achieve decidability, the authors in [14, 12] relax the acceptance conditions so that the emptiness problem can eventually be recast as a coverability problem for a well-structured transition system. In [10] , this result was used to show decidability of equivalence for a first-order (sequential) fragment of Reduced ML. On the other hand, in [7] the authors relax the order of letters in words, which leads to an analysis based on semi-linear sets. Both of these restrictions are too strong to permit the semantics of FICA, because of the game-semantic WAIT condition, which corresponds to waiting until all sub-processes terminate.

Another orthogonal strand of work on concurrent higher-order programs is based on higher-order recursion schemes [24, 29] . Unlike FICA, they feature recursion but the computation is purely functional over a single atomic type o.

Structure of the paper: In the next two sections we recall FICA and its game semantics from [22] . The following sections introduce leafy automata (LA) and their local variant (LLA), where we also analyse the associated decision problems and, in particular, show that the non-emptiness problem for LLA is decidable. Subsequently, we give a translation from FICA to LA (and back) and define a fragment LFICA of FICA which can be translated into LLA. We will occasionally refer the reader to the full paper [18] which includes appendices with proof details and worked examples.

Idealized Concurrent Algol [22] is a paradigmatic language combining higherorder with imperative computation in the style of Reynolds [40] , extended to concurrency with parallel composition (||) and binary semaphores. We consider its finitary variant FICA over the finite datatype {0, . . . , max } (max ≥ 0) with loops but no recursion. Its types θ are generated by the grammar where com is the type of commands; exp that of {0, . . . , max }-valued expressions; var that of assignable variables; and sem that of semaphores. The typing judgments are displayed in Figure 1 . skip and div θ are constants representing termination and divergence respectively, i ranges over {0, · · · , max }, and op represents unary arithmetic operations, such as successor or predecessor (since we work over a finite datatype, operations of bigger arity can be defined using conditionals). Variables and semaphores can be declared locally via newvar and newsem. Variables are dereferenced using !M , and semaphores are manipulated using two (blocking) primitives, grab(s) and release(s), which grab and release the semaphore respectively. The small-step operational semantics of FICA is reproduced in the full paper [18, Appendix A]. We shall write div for div com .

We are interested in contextual equivalence of terms. Two terms are contextually equivalent if there is no context that can distinguish them with respect to may-termination. More formally, a term ⊢ M : com is said to terminate, written M ⇓, if there exists a terminating evaluation sequence from M to skip. Then

The force of this notion is quantification over all contexts.

Since contextual equivalence becomes undecidable for FICA very quickly [23] , we will look at the special case of testing equivalence with terms that always diverge, e.g. given Γ ⊢ M : θ, is it the case that Γ ⊢ M ∼ = div θ ? Intuitively, equivalence with an always-divergent term means that C[M ] will never converge (must diverge) if C uses M . At the level of automata, this will turn out to correspond to the emptiness problem.

In verification tasks, with the above equivalence test, we can check whether uses of M can ever lead to undesirable states. For example, for a given term x : var ⊢ M : θ, the term f : θ → com ⊢ newvar x := 0 in (f (M ) || if !x = 13 then skip else div) will be equivalent to div only when x is never set to 13 during a terminating execution. Note that, because of quantification over all contexts, f may use M an arbitrary number of times, also concurrently or in nested fashion, which is a very expressive form of quantification.

Game semantics for programming languages involves two players, called Opponent (O) and Proponent (P), and the sequences of moves made by them can be viewed as interactions between a program (P) and a surrounding context (O). In this section, we briefly present the fully abstract game model for FICA from [22] , which we rely on in the paper. The games are defined using an auxiliary concept of an arena.

whether it is an Opponent or a Proponent move, and a question or an answer; we write λ OP A , λ QA A for the composite of λ A with respectively the first and second projections; -⊢ A is a binary relation on M A , called enabling, satisfying: if m ⊢ A n for no m then λ A (n) = (O, Q), if m ⊢ A n then λ OP A (m) = λ OP A (n), and if m ⊢ A n then λ QA A (m) = Q. We shall write I A for the set of all moves of A which have no enabler; such moves are called initial. Note that an initial move must be an Opponent question. In arenas used to interpret base types all questions are initial and P-moves answering them are detailed in the table below, where i ∈ {0, · · · , max }. 

We write θ for the arena corresponding to type θ. Below we draw (the enabling relations of) A 1 = com → com → com and A 2 = (var → com) → com respectively, using superscripts to distinguish copies of the same move (the use of superscripts is consistent with our future use of tags in Definition 9) .

Given an arena A, we specify next what it means to be a legal play in A. For a start, the moves that players exchange will have to form a justified sequence, which is a finite sequence of moves of A equipped with pointers. Its first move is always initial and has no pointer, but each subsequent move n must have a unique pointer to an earlier occurrence of a move m such that m ⊢ A n. We say that n is (explicitly) justified by m or, when n is an answer, that n answers m. If a question does not have an answer in a justified sequence, we say that it is pending in that sequence. Below we give two justified sequences from A 1 and A 2 respectively. run run 1 run 2 done 1 done 2 done run run 1 read 11 0 11 write(1) 11 ok 11 read 11 1 11 Not all justified sequences are valid. In order to constitute a legal play, a justified sequence must satisfy a well-formedness condition that reflects the "static" style of concurrency of our programming language: any started sub-processes must end before the parent process terminates. This is formalised as follows, where the letters q and a to refer to question-and answer-moves respectively, while m denotes arbitrary moves.

Definition 2. The set P A of plays over A consists of the justified sequences s over A that satisfy the two conditions below.

FORK : In any prefix s ′ = · · · q · · · m of s, the question q must be pending when m is played. WAIT : In any prefix s ′ = · · · q · · · a of s, all questions justified by q must be answered.

It is easy to check that the justified sequences given above are plays. A subset σ of P A is O-complete if s ∈ σ and so ∈ P A imply so ∈ σ, when o is an O-move.

Suppose Γ = {x 1 : θ 1 , · · · , x l : θ l } and Γ ⊢ M : θ is a FICA-term. Let us write Γ ⊢ θ for the arena θ 1 × · · · × θ l ⇒ θ . In [22] it is shown how to assign a strategy on Γ ⊢ θ to any FICA-term Γ ⊢ M : θ. We write Γ ⊢ M to refer to that strategy. For example, Γ ⊢ div = {ǫ, run} and Γ ⊢ skip = {ǫ, run, run done}. Given a strategy σ, we denote by comp(σ) the set of nonempty complete plays of σ, i.e. those in which all questions have been answered. The game-semantic interpretation · · · turns out to provide a fully abstract model in the following sense.

In particular, since we have

We would like to be able to represent the game semantics of FICA using automata.

To that end, we introduce leafy automata (LA). They are a variant of automata over nested data, i.e. a type of automata that read finite sequences of letters of the form (t,

In our case, D will have the structure of a countably infinite forest and the sequences d 0 · · · d j will correspond to branches of a tree. Thus, instead of d 0 · · · d j , we can simply write d j , because d j uniquely determines its ancestors: d 0 , . . . , d j−1 . The following definition captures the technical assumptions on D. such that pred i+1 (d) = ⊥. Level-0 data values will be called roots.

In order to define configurations of leafy automata, we will rely on finite subtrees of D, whose nodes will be labelled with states. We say that T ⊆ D is a subtree of D iff T is closed (∀x ∈ T : pred (x) ∈ T ∪{⊥}) and rooted (∃!x ∈ T : pred (x) = ⊥).

Next we give the formal definition of a level-k leafy automaton. Its set of states Q will be divided into layers, written Q (i) (0 ≤ i ≤ k), which will be used to label level-i nodes. We will write

is a finite set of states, partitioned into sets Q (i) of level-i states; -δ = δ Q + δ A is a finite transition function, partitioned into question-and answer-related transitions;

Configurations of LA are of the form (D, E, f ), where D is a finite subset of D (consisting of data values that have been encountered so far), E is a finite subtree of D, and f : E → Q is a level-preserving function, i.e. if d is a level-i data value then f (d) ∈ Q (i) . A leafy automaton starts from the empty configuration κ 0 = (∅, ∅, ∅) and proceeds according to δ, making two kinds of transitions. Each kind manipulates a single leaf: for questions one new leaf is added, for answers one leaf is removed. Let the current configuration be κ = (D, E, f ).

-On reading a letter (t, d) with t ∈ Σ Q and d ∈ D a fresh level-i data, the automaton adds a new leaf d in a configuration and updates the states on the branch to d. So it changes its configuration to

leaf, the automaton deletes d and updates the states on the branch to d. So it changes its configuration to

Q . The last move is treated symmetrically.

In all cases, we write κ

Note that a single transition can only change states on the branch ending in d. Other parts of the tree remain unchanged.

For κ 1 to evolve into κ 2 (on (t, d 2 )), we need (q (0) , q (1) , t, r (0) , r (1) , r (2) ) ∈ δ

Q . On the other hand, to go from κ 2 to κ 3 (on (t, d 2 )), we want (r (0) , r (1) , r (2) , t,

there is a non-empty sequence of transitions as above with κ h accepting. The set of traces (resp. accepted traces) of A is denoted by Tr (A) (resp. L(A)). Remark 1. When writing states, we will often use superscripts (i) to indicate the intended level. 

, i.e. they are valid histories of a single non-negative counter (histories such that the counter starts and ends at 0). In this case, all traces are simply prefixes of such words.

Remark 2. Note that, whenever a leafy automaton reads (t, d) (t ∈ Σ Q ) and the level of d is greater than 0, then it must have read a unique question (t ′ , pred (d)) earlier. Also, observe that an LA trace contains at most two occurrences of the same data value, such that the first is paired with a question and the second is paired with an answer. Because the question and the answer share the same data value, we can think of the answer as answering the question, like in game semantics. Indeed, justification pointers from answers to questions will be represented in this way in Theorem 3. Finally, we note that LA traces are invariant under tree automorphisms of D.

Lemma 1. The emptiness problem for 2-LA is undecidable. For 1-LA, it is reducible to the reachability problem for VASS in polynomial time and there is a reverse reduction in exponential time, so it is decidable in Ackermannian time [32] but not elementary [13] .

Proof. For 2-LA we reduce from the halting problem on two-counter-machines. Two counters can be simulated using configurations of the form

where there are two level-1 nodes, one for each counter. The number of children at level 2 encodes the counter value. Zero tests can be implemented by removing the corresponding level-1 node and creating a new one. This is possible only when the node is a leaf, i.e., it does not have children at level 2. The state of the 2-counter machine can be maintained at level 0, the states at level 1 indicate the name of the counter, and the level-2 states are irrelevant.

The translation from 1-LA to VASS is straightforward and based on representing 1-LA configurations by the state at level 0 and, for each state at level 1, the count of its occurrences. The reverse translation is based on the same idea and extends the encoding of a non-negative counter in Example 2, where the exponential blow up is simply due to the fact that vector updates in VASS are given in binary whereas 1-LA transitions operate on single branches. ⊓ ⊔ Lemma 2. 1-LA equivalence is undecidable.

Proof. We provide a direct reduction from the halting problem for 2-counter machines, where both counters are required to be zero initially as well as finally.

The main obstacle is that implementing zero tests as in the proof of the first part of Lemma 1 is not available because we are restricted to leafy automata with levels 0 and 1 only. To overcome it, we exploit the power of the equivalence problem where one of the 1-LA will have the task not of correctly simulating zero tests but recognising zero tests that are incorrect. The complete argument can be found in the full paper [18, Appendix B] . ⊓ ⊔

Here we identify a restricted variant of LA for which the emptiness problem is decidable. We start with a technical definition.

if there is a bound b such that each node at level i can create at most b children during a run. We refer to b as the branching bound.

Note that we are defining a "global" bound on the number of children that a node at level i may create across a whole run, rather than a "local" bound on the number of children a node may have in a given configuration.

To motivate the design of LLA, we observe that the undecidability argument (for the emptiness problem) for 2-LA used two consecutive levels (0 and 1) that are not bounded. For the node at level 0, this corresponded to the number of zero tests, while an unbounded counter is simulated at level 1. In the following we will eliminate consecutive unbounded levels by introducing an alternating pattern of bounded and unbounded levels. Even-numbered layers (i = 0, 2, ...) will be bounded, while odd-numbered layers will be unbounded. Observe in particular that the root (layer 0) is bounded. As we will see later, this alternation reflects the term/context distinction in game semantics: the levels corresponding to terms are bounded, and the levels coresponding to contexts are unbounded.

With this restriction alone, it is possible to reconstruct the undecidability argument for 4-LA, as two unbounded levels may still communicate. Thus we introduce a restriction on how many levels a transition can read and modify.

when adding or removing a leaf at an odd level 2i + 1, the automaton will be able to access levels 2i, 2i − 1 and 2i − 2; while -when adding or removing a leaf at an even level 2i, the automaton will be able to access levels 2i − 1 and 2i − 2.

In particular, when an odd level produces a leaf, it will not be able to see the previous odd level. The above constraints mean that the transition functions δ

Q can be presented in a more concise form, given below.

In terms of the previous notation used for LA, (q (i−2) , q (i−1) , x, r (i−2) , r (i−1) , r (i) ) ∈ δ (i) Q denotes all tuples of the form ( q, q (i−2) , q (i−1) , x, q, r (i−2) , r (i−1) , r (i) ), where q ranges over Q (0,··· ,i−3) .

A level-k local leafy automaton (k-LLA) is a k-LA whose transition function admits the above-mentioned presentation and which is bounded at all even levels.

Theorem 2. The emptiness problem for LLA is decidable.

Proof (Sketch). Let b be a bound on the number of children created by each even node during a run.

The critical observation is that, once a node d at even level 2i has been created, all subsequent actions of descendants of d access (read and/or write) the states at levels 2i − 1 and 2i − 2 at most 2b times. The shape of the transition function dictates that this can happen only when child nodes at level 2i + 1 are added or removed. In addition, the locality property ensures that the automaton will never access levels < 2i − 2 at the same time as node d or its descendants.

We will make use of these facts to construct summaries for nodes on even levels which completely describe such a node's lifetime, from its creation as a leaf until its removal, and in between performing at most 2b reads-writes of the parent and grandparent states. A summary is a sequence quadruples of states: two pairs of states of levels 2i − 2 and 2i − 1. The first pair are the states we expect to find on these levels, while the second are the states to which we update these levels. Hence a summary at level 2i is a complete record of a valid sequence of read-writes and stateful changes during the lifetime of a node on level 2i.

We proceed by induction and show how to calculate the complete set of summaries at level 2i given the complete set of summaries at level 2i + 2. We construct a program for deciding whether a given sequence is a summary at level 2i. This program can be evaluated via Vector Addition Systems with States (VASS). Since we can finitely enumerate all candidate summaries at level 2i, this gives us a way to compute summaries at level 2i. Proceeding this way, we finally calculate summaries at level 2. At this stage, we can reduce the emptiness problem for the given LLA to a reachability test on a VASS.

The complete argument is given in the full paper [18, Appendix C].

Let us remark also that the problem becomes undecidable if we remove either boundedness restriction, or allow transitions to look one level further.

Recall from Section 3 that, to interpret base types, game semantics uses moves from the set

The game semantic interpretation of a term-in-context Γ ⊢ M : θ is a strategy over the arena Γ ⊢ θ , which is obtained through product and arrow constructions, starting from arenas corresponding to base types. As both constructions rely on the disjoint sum, the moves from Γ ⊢ θ are derived from the base types present in types inside Γ and θ. To indicate the exact occurrence of a base type from which each move originates, we will annotate elements of M with a specially crafted scheme of superscripts. Suppose Γ = {x 1 : θ 1 , · · · , x l : θ l }. The superscripts will have one of the two forms, where i ∈ N * and ρ ∈ N:

-( i, ρ) will be used to represent moves from θ;

The annotated moves will be written as m ( i,ρ) or m (xv i,ρ) , where m ∈ M. We will sometimes omit ρ on the understanding that this represents ρ = 0. Similarly, when i is omitted, the intended value is ǫ. Thus, m stands for m (ǫ,0) . The next definition explains how the i superscripts are linked to moves from θ . Given X ⊆ {m ( i,ρ) | i ∈ N * , ρ ∈ N} and y ∈ N ∪ {x 1 , · · · , x l }, we let yX = {m (y i,ρ) | m ( i,ρ) ∈ X}.

Definition 9. Given a type θ, the corresponding alphabet T θ is defined as follows

To represent the game semantics of terms-in-context, of the form Γ ⊢ M : θ, we are going to use finite subsets of T Γ ⊢θ as alphabets in leafy automata. The subsets will be finite, because ρ will be bounded. Note that T θ admits a natural partitioning into questions and answers, depending on whether the underlying move is a question or answer.

We will represent plays using data words in which the underpinning sequence of tags will come from an alphabet as defined above. Superscripts and data are used to represent justification pointers. Intuitively, we represent occurrences of questions with data values. Pointers from answers to questions just refer to these values. Pointers from questions use bounded indexing with the help of ρ.

Initial question-moves do not have a pointer and to represent such questions we simply use ρ = 0. For non-initial questions, we rely on the tree structure of D and use ρ to indicate the ancestor of the currently read data value that we mean to point at. Consider a trace w(t i , d i ) ending in a non-initial question, where d i is a level-i data value and i > 0. In our case, we will have t i ∈ T Γ ⊢θ , i.e. t i = m (··· ,ρ) . By Remark 2, trace w contains unique occurrences of questions (t 0 , d 0 ), · · · , (t i−1 , d i−1 ) such that pred (d j ) = d j−1 for j = 1, · · · , i. The pointer from (t i , d i ) goes to one of these questions, and we use ρ to represent the scenario in which the pointer goes to (t i−(1+ρ) , d i−(1+ρ) ).

Pointers from answer-moves to question-moves are represented simply by using the same data value in both moves (in this case we use ρ = 0).

We will also use ǫ-tags ǫ Q (question) and ǫ A (answer), which do not contribute moves to the represented play. Each ǫ Q will always be answered with ǫ A . Note that the use of ρ, ǫ Q , ǫ A means that several data words may represent the same play (see Examples 4, 6) . Example 6. One might wish to represent plays of σ from the previous Example using data values d 0 ,

, so that the play from Example 4 is represented by (run (ǫ,0) 

. Unfortunately, it is impossible to construct a 2-LA that would accept all representations of such plays. To achieve this, the automaton would have to make sure that the number of run f 1 s is the same as that of run x s. Because the former are labelled with level-2 values and the latter with incomparable level-1 values, the only point of communication (that could be used for comparison) is the root. However, the root cannot accommodate unbounded information, while plays of σ can feature an unbounded number of run f 1 s, which could well be consecutive.

Before we state the main result linking FICA with leafy automata, we note some structural properties of the automata. Questions will create a leaf, and answers will remove a leaf. P-moves add leaves at odd levels (questions) and remove leaves at even levels (answers), while O-moves have the opposite effect at each level. Finally, when removing nodes at even levels we will not need to check if a node is a leaf. We call the last property even-readiness.

Even-readiness is a consequence of the WAIT condition in the game semantics. The condition captures well-nestedness of concurrent interactions -a term can terminate only after subterms terminate. In the leafy automata setting, this is captured by the requirement that only leaf nodes can be removed, i.e. a node can be removed only if all of its children have been removed beforehand. It turns out that, for P-answers only, this property will come for free. Formally, whenever the automaton arrives at a configuration κ = (D, E, f ), where d ∈ E and there is a transition

then d is a leaf. In contrast, our automata will not satisfy the same property for O-answers (the environment) and for such transitions it is crucial that the automaton actually checks that only leaves can be removed. ,

. The remaining transitions advance each component:

where m = run, done.

Γ ⊢ newvar x := i in M 1 By [22] , the semantics of this term is obtained from the semantics of Γ, x ⊢ M 1 by 1. restricting to plays in which the moves read x , write(n) x are followed immediately by answers, 2. selecting those plays in which each answer to a read x -move is consistent with the preceding write(n) x -move (or equal to i, if no write(n) x was made), 3. erasing all moves related to x, e.g. those of the form m (x,ρ) .

To implement 1., we will lock the automaton after each read x -or write(n) x -move, so that only an answer to that move can be played next. Technically, this will be done by adding an extra bit (lock) to the level-0 state. To deal with 2., we keep track of the current value of x, also at level 0. This makes it possible to ensure that answers to read x are consistent with the stored value and that write(n) x transitions cause the right change. Erasing from condition 3 is implemented by replacing all moves with the x subscript with ǫ Q , ǫ A -tags.

Accordingly, we have Q (0) = (Q .

Γ ⊢ f M h · · · M 1 : com with (f : θ h → · · · → θ 1 → com) Here we will need

The first group of transitions corresponding to calling and returning from f :

Additionally, in state (1, 0) we want to enable the environment to spawn an unbounded number of copies of each of Γ ⊢ M u : θ u (1 ≤ u ≤ h). This is done through rules that embed the actions of the automata for M u while (possibly) relabelling the moves in line with our convention for representing moves from game semantics. Such transitions have the general form

. Note that this case also covers f : com (h = 0). More details and the remaining cases are covered in the full paper [18, Appendix D], along with an example of a term and the corresponding LA. ⊓ ⊔

In this section we identify a family of FICA terms that can be translated into LLA rather than LA. To achieve boundedness at even levels, we remove while 5 . To achieve restricted communication, we will constrain the distance between a variable declaration and its use. Note that in the translation, the application of function-type variables increases LA depth. So in LFICA we will allow the link between the binder newvar/newsem x and each use of x to "cross" at most one occurrence of a free variable. For example, the following terms -newvar x := 0 in x := 1 || f (x := 2), -newvar x := 0 in f (newvar y in f (y := 1) || x :=!y) will be allowed, but not newvar x := 0 in f (f (x := 1)).

To define the fragment formally, given a term Q in βη-normal form, we use a notion of the applicative depth of a variable x : β (β = var, sem) inside Q, written ad x (Q) and defined inductively by the table below. The applicative depth is increased whenever a functional identifier is applied to a term containing x.

Note that in our examples above, in the first two cases the applicative depth of x is 2; and in the third case it is 3.

Definition 10 (Local FICA). A FICA-term Γ ⊢ M : θ is local if its βη-normal form does not contain any occurrences of while and, for every subterm of the normal form of the shape newvar /newsem x := i in N , we have ad x (N ) ≤ 2. We write LFICA for the set of local FICA terms. Proof (Sketch). We argue by induction that the constructions from Theorem 3 preserve presentability as a LLA.

The case of parallel composition involves running copies of M 1 and M 2 in parallel without communication, with their root states stored as a pair at level 0. Note, though, that each of the automata transitions independently of the state of the other automaton. In consequence, if the automata M 1 and M 2 are LLA, so will be the automaton for M 1 ||M 2 . The branching bound after the construction is the sum of the two bounds for M 1 and M 2 .

For Γ ⊢ newvar x := i in M , because the term is in LFICA, so is Γ, x : var ⊢ M and we have ad x (M ) ≤ 2. Then we observe that in the translation of Theorem 3 (Γ, x : var ⊢ M : θ) the questions related to x, (namely write(i) (x,ρ) and read (x,ρ) ) correspond to creating leaves at levels 1 or 3, while the corresponding answers (ok (x,ρ) and i (x,ρ) respectively) correspond to removing such leaves. In the construction for Γ ⊢ newvar x in M , such transitions need access to the root (to read/update the current state) and the root is indeed within the allowable range: in an LLA transitions creating/destroying leaves at level 3 can read/write at level 0. All other transitions (not labelled by x) proceed as in M and need not consult the root for additional information about the current state, as it is propagated. Consequently, if M is represented by a LLA then the interpretation of newvar x := i in M is also a LLA. The construction does not affect the branching bound, because the resultant runs can be viewed as a subset of runs of the automaton for M , i.e. those in which reads and writes are related.

For f M h · · · M 1 , we observe that the construction first creates two nodes at levels 0 and 1, and the node at level 1 is used to run an unbounded number of copies of (the automaton for) M i . The copies do not need access to the states stored at levels 0 and 1, because they are never modified when the copies are running. Consequently, if each M i can be translated into a LLA, the outcome of the construction in Theorem 3 is also a LLA. The new branching bound is the maximum over bounds from M 1 , · · · , M h , because at even levels children are produced as in M i and level 0 produces only 1 child.

⊓ ⊔ Corollary 1. For any LFICA-term Γ ⊢ M : θ, the problem of determining whether comp( Γ ⊢ M ) is empty is decidable.

Theorems 1 and 2 imply the above. Thanks to Theorem 1, it is decidable if a LFICA term is equivalent to a term that always diverges (cf. example on page 187). In case of inequivalence, our results could also be applied to extract the distinguishing context, first by extracting the witnessing trace from the argument underpinning Theorem 2 and then feeding it to the Definability Theorem (Theorem 41 [22] ). This is a valuable property given that in the concurrent setting bugs are difficult to replicate.

In this section, we show how to represent leafy automata in FICA. Let A = Σ, k, Q, δ be a leafy automaton. We shall assume that Σ, Q ⊆ {0, · · · , max } so that we can encode the alphabet and states using type exp. We will represent a trace w generated by A by a play play(w), which simulates each transition with two moves, by O and P respectively. The child-parent links in D will be represented by justification pointers. We refer the reader to [18, Appendix F] for details. Below we just state the lemma that identifies the types that correspond to our encoding, where we write θ max +1 → β for θ → · · · → θ max +1 → β.

Lemma 3. Let A be a k-LA and w ∈ Tr (A). Then play(w) is a play in θ k , where θ 0 = com max +1 → exp and θ i+1 = (θ i → com) max +1 → exp (i ≥ 0).

Before we state the main result, we recall from [22] that strategies corresponding to FICA terms satisfy a closure condition known as saturation: swapping two adjacent moves in a play belonging to such a strategy yields another play from the same strategy, as long as the swap yields a play and it is not the case that the first move is by O and the second one by P. Thus, saturated strategies express causal dependencies of P-moves on O-moves. Consequently, one cannot expect to find a FICA-term such that the corresponding strategy is the smallest strategy containing { play(w) | w ∈ Tr (A) }. Instead, the best one can aim for is the following result.

Theorem 5. Given a k-LA A, there exists a FICA term ⊢ M A : θ k such that ⊢ M A : θ k is the smallest saturated strategy containing { play(w) | w ∈ Tr (A) }.

Proof (Sketch). Our assumption Q ⊆ {0, · · · , max } allows us to maintain Astates in the memory of FICA-terms. To achieve k-fold nesting, we use the higherorder structure of the term: λf (0) .f (0) (λf (1) .f (1) (λf (2) .f (2) (· · · λf (k) .f (k) ))). In fact, instead of the single variables f (i) , we shall use sequences f (i) 0 · · · f (i) max , so that a question t (i) Q read by A at level i can be simulated by using variable f (i) t (i) Q (using our assumption Σ ⊆ {0, · · · , max }). Additionally, the term contains state-manipulating code that enables moves only if they are consistent with the transition function of A. ⊓ ⊔

We have introduced leafy automata, LA, and shown that they correspond to the game semantics of Finitary Idealized Concurrent Algol (FICA). The automata formulation makes combinatorial challenges posed by the equivalence problem explicit. This is exemplified by a very transparent undecidability proof of the emptiness problem for LA. Our hope is that LA will allow to discover interesting fragments of FICA for which some variant of the equivalence problem is decidable. We have identified one such instance, namely local leafy automata (LLA), and a fragment of FICA that can be translated to them. The decidability of the emptiness problem for LLA implies decidability of a simple instance of the equivalence problem. This in turn allows to decide some verification questions as in the example on page 187. Since these types of questions involve quantification over all contexts, the use of a fully-abstract semantics appears essential to solve them. The obvious line of future work is to find some other subclasses of LA with decidable emptiness problem. Another interesting target is to find an automaton model for the call-by-value setting, where answers enable questions [2, 25] . It would also be worth comparing our results with abstract machines [19] , the Geometry of Interaction [31] , and the π-calculus [6] .

Applying game semantics to compositional software modelling and verification

Call-by-value games

Game semantics

Verifying communicating multi-pushdown systems via split-width

On-the-fly techniques for games-based software model checking

Sequentiality and the pi-calculus

Shuffle expressions and words with nested data

On notions of regularity for data languages

Two-variable logic on data words

Fragments of ML decidable by nested data class memory automata

ML, visibly pushdown class memory automata, and extended branching vector addition systems with states

Weak and nested class memory automata

The reachability problem for Petri nets is not elementary

Ordered navigation on multiattributed data words

A counterexample-guided refinement tool for open procedural programs

Symbolic game semantics for model checking program families

Probabilistic analysis based on symbolic game semantics and model counting

Leafy automata for higher-order concurrency

Abstract machines for game semantics, revisited

Reasoning about Idealized Algol using regular expressions

Compositional model extraction for higher-order concurrent programs

Angelic semantics of fine-grained concurrency

Syntactic control of concurrency. Theoretical Computer Science pp

Saturation of concurrent collapsible pushdown systems

Game-theoretic analysis of call-by-value computation

Hector: An Equivalence Checker for a Higher-Order Fragment of ML

Homer: A Higher-order Observational equivalence Model checkER

APEX: An Analyzer for Open Probabilistic Programs

Model-checking higher-order programs with recursive types

Reducing context-bounded concurrent reachability to sequential reachability

The geometry of concurrent interaction: handling multiple ports by way of multiple tokens

Reachability in vector addition systems is primitiverecursive in fixed dimension

Games for complexity of second-order call-by-name programs

Game semantic analysis of equivalence in IMJ

An invitation to game semantics

Third-order Idealized Algol with iteration is decidable

Observational equivalence of 3rd-order Idealized Algol is decidable

Context-bounded model checking of concurrent software

Context-sensitive synchronization-sensitive analysis is undecidable

The essence of Algol

Automata for XML -A survey

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use