Pushdown Multi-Agent System Verification

1 Introduction

Model Checking is a well-established method widely used to verify hardware and software systems [Clarke et al., 2002]. The idea is simple and appealing: we use a mathematical model of the system we want to validate and check it over a formal specification of its desired behavior [Clarke and Emerson, 1981; Queille and Sifakis, 1981].

In the eighties, early use of model checking mainly considered finite-state closed systems, modeled as Kripke structures, and specifications given in terms of temporal-logic formulas [Pnueli, 1977]. The conceived algorithms, however, turn less appropriate in open-system verification as one has to take into account also the uncertainty about the agents' behavior. As a first solution, module checking [Kupferman et al., 2001] came out with its ability of handling the interaction between the system and an external unpredicted environment. Precisely it takes as inputs a graph partitioned in two sets (called a module) M and a formula ϕ, and checks whether M reactively satisfies ϕ, i.e., no matter how the environment behaves.

Starting from the works on module checking, two significant directions have been taken in open-system verification. One concerns extending the framework to more sophisticated systems while maintaining the dichotomy system-environment states in modeling. In this context, worthy of mention is the work on pushdown module checking [Bozzelli et al., 2010]. This has the merit of having handled the verification of infinitestate open systems and, thanks to the fact that the infinite number of states is induced by a recursive structure of finite size, the problem turns out to be decidable and precisely 3EXPTIME-COMPLETE for specifications in CTL⋆ . Another direction has instead completely redesigned the module checking approach in order to handle the more involved scenario of multi-agent (concurrent) systems. To let the temporal-logic framework working within this setting, Alternating-Time Temporal Logic (ATL⋆ , for short) [Alur et al., 2002] has been introduced. This logic generalizes CTL⋆ by means of strategic quantifiers. ATL⋆ formulas are interpreted over concurrent game structures (CGS, for short). Given an ATL⋆ formula 〈〈A〉〉ψ, with A set of agents, it is satisfied over a CGS G if there exists a strategy for the agents in A such that, no matter which strategy is executed by agents not in A, the resulting outcome in G satisfies ψ. As for finite-state CTL⋆ module checking, the model-checking problem for specifications in ATL⋆ turns out to be 2EXPTIME-COMPLETE. However, the two approaches are incomparable as in module checking it is possible to use nondeterministic strategies.

∗This work has been partially supported by the ERC Advanced Grant "RACE" (291528) at Oxford and the FP7 EU project 600958SHERPA.

Despite the undoubted utility of considering, from one hand, infinite-state open-system models induced by finite-size recursive structures and, from the other hand, multi-agent specifications, to the best of our knowledge no work has been devoted to the combination of the two.

In this paper, we consider multi-agent pushdown systems and address the related model checking problem for specifications expressed in ATL⋆ . To this aim, we first introduce pushdown game structures to properly model the infinite-state multi-agent system and formalize the model checking question. Then, by means of an automata-theoretic approach, we provide a 3EXPTIME solution to the addressed problem. Precisely, we construct a doubly-exponential size pushdown parity tree automaton that collects all execution trees satisfying the ATL⋆ formula. Then by using the fact that the emptiness of this automaton can be checked in exponential time [Kupferman et al., 2002], we get the desired result. We also provide a 2EXPSPACE lower bound by showing a reduction from the word acceptance problem for a deterministic Turing machine with doubly exponential space.

Related works. In recent years, model checking of pushdown systems has received a lot of attention, largely due to the ability of these systems to capture the flow of procedure of calls and returns in programs [Alur et al., 2005].

The work in this area started with Muller and Schupp, who showed that the monadic second-order theory of graphs induced by pushdown systems is decidable [Muller and Schupp, 1985]. Walukiewicz in [Walukiewicz, 1996] showed that the model checking for pushdown systems with respect to modal µ-calculus is EXPTIME-COMPLETE. The problem remains EXPTIME-COMPLETE also for CTL and LTL, while it becomes 2EXPTIME-COMPLETE for CTL⋆ [Walukiewicz, 2000; Bouajjani et al., 1997]. In [Bozzelli et al., 2010], open pushdown systems along with the module checking paradigm have been considered. This setting has been investigated under several restrictions including the imperfect-information case [Aminof et al., 2013].

Literature on model checking of ATL⋆ is also wide. This problem has been investigated under different settings and inspired powerful formalisms for the strategic reasoning (see [Bulling, 2014], for a recent survey). Model checkers for ATL and ATL⋆ also exist, such as MCMAS [Lomuscio and Raimondi, 2006; Cerm´ak et al., 2014; 2015].

Outline The rest of the paper is organized as follows. In Section 2 we introduce PGSs and provide an example to help clarifying the setting. There, we also show how a PGS can be embedded into an infinite-state CGS. In Section 3 we recall the syntax and the semantics of ATL⋆ over CGSs and define the model-checking problem of ATL⋆ over PGSs. In Section 4 we show that the latter can be solved in 3EXPTIME by means of an automata-theoretic approach. There, we also show a 2EXPSPACE-hard lower bound. Finally, in Section 5 we summarize the achieved results and discuss some future work.

2 Pushdown Game Structures

Classically, ATL⋆ formulas are interpreted over Concurrent Game Structures [Alur et al., 2002]. In this paper, we instead interpret ATL⋆ formulas over a new semantic framework, which we call Pushdown Game Structure. Intuitively, this new formalism provides a concurrent game structure in which a stack is added and the labeling and transition functions depend on its content. In this section, we also show that every pushdown game structure can be transformed into a suitable concurrent game structure, so providing the required interpretation of ATL⋆ formulas over the former. However, note that the latter requires a infinite number of states, used to represent all the possible configurations the pushdown system can enter. We start with the definition of pushdown game structures.

Definition 2.1 (Pushdown Game Structure) A Pushdown Game Structure (PGS, for short) is a tuple P = 〈AP,Ag, Ac, Loc, Γ, tr, ap, l 〉, where AP, Ag, Ac, Loc and Γ are finite sets of atomic propositions, agents, actions, locations, and stack alphabet, respectively, l ∈ Loc is an initial location, and ap : Loc × Γ⊥ → 2AP is a labeling function, where Γ⊥ = Γ ∪ {⊥} and ⊥ is the special bottom stack symbol not contained in Γ. Let Dc ≜ AcAg be the set of decisions, i.e., functions from Ag to Ac representing the action choices for each agent. Then, tr : Loc × Γ⊥ × Dc → Loc × Γ∗⊥ is a transition function mapping a location, a stack symbol, and a decision to a location and a word in the stack alphabet.

A pair s = (l, α) ∈ St ≜ Loc × (Γ∗ · {⊥}) is called state or configuration. We write top(α) for the left most symbol of α and call it the top of the stack content α. The PGS moves according to the transition function. This means that, if it is in the location l, the top of the stack content is γ, and the agents make a decision d, then tr(l, γ, d) = (l′ , α) means that the execution moves to the location l′ and the symbol γ is replaced with α on the top of the stack content. We assume that, if ⊥ is popped, then it is pushed right back, and that is the only case in which it is pushed. This means that ⊥ is always on the bottom of the stack and nowhere else. The stack containing only the symbol ⊥ is said to be empty.

As the stack has no a priori bound on its size, the set St is assumed to be possibly infinite. Saying this, it turns out that PGSs are infinite-state multi-agent systems.

The notion of labeling and transition can be lifted to states, as follows. For a state s = (l, α), we define ap(s) = ap(l, top(α)). Moreover, for a decision d ∈ Dc, we define tr((l, γ · α), d) = (l′ , β · α), with (l′ , β) = tr(l, γ, d).

Note that for a classical pop we write the empty word ε on the stack. To make a classical push one has to first put back the read top symbol and then push the required word. The transition function also allows to perform in one step a pop-push operation that replaces the top stack symbol with the required word.

For our convenience, we consider also two-player turnbased one-symbol stack games of the form P =〈AP, {E, A}, Loc, LocE, LocA, R, ap, l〉 where LocE and LocA are the sets of locations belonging to players E and A, respectively, and R ⊆ (Loc×{γ, ⊥})×(Loc×{push, , pop}), where γ is the only alphabet symbol of the stack, and push, pop, and are the push, pop, and null operation on the stack. If (l, x, l′ , op) ∈ R, then, for each configuration (l, α) with top(α) = x we can move to the configuration (l′ , α′ ) with α′ being the string obtained from α by applying the stack operation op. At each configuration (l, α) of the game, the owner of the location l can pick a successor, according to the relation R. It is not hard to see that two-player turn-based one-symbol stack games are special cases of PGSs

To get familiar with PGSs, we give an example.

Example 2.1 (Pushdown scheduler) Take a system consisting of two processes a and b that may access to a common resource via the respective requests ra and rb and a scheduler s that can grant in a LIFO order the processes requests, all memorized into a stack. As model we use a PGS P =〈AP, Ag, Ac, Loc, Γ, tr, ap, l 〉, with AP = {ra, rb, ga, gb, a, b, e}, Ag = {s, a, b}, Ac = {a, b, un, 0, 1}, Loc = {l, la, lb, lun}, and Γ = {ra, rb}. The scheduler s controls the location l by means of the actions a, b, and un, standing for "a can make a request", "b can make a request", and "the system can unload the stack requests", respectively. Accordingly, they lead to the locations la, lb, and lun. On la and lb, the agents a and b, respectively, can either make a request via action 1 or skip it with action 0. In the former case, the request is recorded into the stack by writing the symbol rx, for x ∈ {a, b}; otherwise, in the latter case there is no operation over the stack. Finally, l, ⊥

Figure 1: A Pushdown system scheduler.

the location lun triggers the granting phase by emptying the stack. During this phase, neither a nor b can make any further request. This can be seen as a legitimate constraint by thinking how classical synchronizing and backup systems are designed.

The labeling function, for all γ ∈ Γ⊥ and x ∈ {a, b}, is defined as follows: ap(l,⊥) = ∅, ap(l, rx) = {x}, ap(lx, γ) = {x}, ap(lun, rx) = {gx}, and ap(lun,⊥) = {e}. Intuitively, propositions a and b means that agents a and b are authorized to make a request, respectively. The proposition rx, instead, occurs when the corresponding request has been just made by agent x. On the other hand, the proposition gx occurs when the request rx has been just granted. Finally, e indicates that the unloading phase is terminated and so the stack is empty.

The transition function tr is described directly in Figure 1. The labeling of the edges have the following meaning. First, note that it is composed of two parts separated by a semicolumn. The left part represents the decision of the agents, given in the order s < a < b. The right part represents the stack operation. As an example, the label ∗1∗; push(ra) says that agent a is making a request ra and the symbol ra is pushed on the stack, where the symbol ∗ denotes any possible action for the other agents.

The nodes represent all possible states. Note that, for the locations la and lb we have collapsed the two possible configurations with β = ⊥ and β ̸= ⊥ since the transition over them does not depend on the stack content.

Finally, observe that the stack is unbounded and so an execution might generate an infinite number of distinguished states. Also, observe that the stack is fundamental to keep track of the order in which the requests appear.

To correctly interpret ATL⋆ formulas over PGSs, we show that a PGS can be represented as an infinite-state concurrent game structure, whose definition follows. Note that we use the one reported in [Mogavero et al., 2014].

Definition 2.2 (Concurrent Game Structures) A concurrent game structure (CGS, for short) is a tuple G ≜〈AP,Ag, Ac, St, tr, ap, s 〉, where AP, Ag, and Ac are as in PGS. St is an enumerable non-empty set of states, s ∈ St is an initial state, and ap : St → 2AP is a labeling function mapping each state to a set of atomic propositions true in that state. Finally, tr : St ×Dc → St is a transition function mapping pairs of states and decisions to states, where the set Dc is as in PGS.

Clearly, a PGS P = 〈AP, Ag, Ac, Loc, Γ, tr, ap, l 〉 can be suitably turned into a CGS GP =〈AP, Ag, Ac, St, tr, ap, s 〉, where St = Loc × Γ∗⊥, s = (l, ⊥), and the functions ap and tr are the lifting on states of the corresponding functions in P. Intuitively, the states of G are used to implicitly represent both the current location and store the stack content. Despite this, it is important to observe that, while a PGS has a finite number of control locations, the corresponding CGS necessarily has an infinite number of control states, as the number of different stack contents is unbounded.

We conclude this section by briefly recalling the classical notions of track, path, strategies and assignments, which are required for the semantics of ATL⋆ (see [Mogavero et al., 2014], for more). Intuitively, tracks and paths are legal sequences of reachable states, respectively seen as partial and complete descriptions of possible outcomes over a CGS. Formally, a track (resp., path) in a CGS is a finite (resp., an infinite) sequence of states ρ ∈ St∗ (resp., π ∈ Stω ) such that, for all i ∈ [0, |ρ| - 1[ (resp., i ∈ N), there is a decision d ∈ Dc with (ρ)i+1 = tr((ρ)i, d) (resp., (π)i+1 = tr((π)i, d)). The set Trk ⊆ St+ (resp., Pth ⊆ Stω ) contains all non-empty tracks (resp., paths). Moreover, Trk(s) ≜ {ρ ∈ Trk : (ρ)0 = s} (resp., Pth(s) ≜ {π ∈ Pth : (π)0 = s}) denotes the subsets of tracks (resp., paths) starting at a state s.

A strategy for an agent is a scheme containing all choices of actions, depending on the current outcome. Formally, a strategy in a CGS is a function f : Trk → Ac that maps each non-empty track to an action. The set Str contains all strategies. For a given subset A ⊆ Ag of agents, an assignment over A is a partial function χA : Ag ⇀ Str, mapping each agent in A to a strategy. By Asg we denote the set of assignments. A path is compatible with an assignment χA if it is obtained by agents in A using strategies in χA. More formally, for a given set A ⊆ Ag and an assignment χA over A, we say that a path π is compatible with χA if, for all i ∈ N it holds that (π)i+1 = tr((π)i, d), for some d ∈ Dc with d(a) ≜ χAsg(a)((π)≤i), for each a ∈ A. By play(χA, s) we denote the set of paths starting from s that are compatible with χA. Note that, for an assignment χAg over the full set Ag of agents, there exists only one compatible path. In this case, by abuse of notation, we denote it with play(χAg, s).

3 ATL*

In this section, we recall the syntax of ATL⋆ and introduce its semantics over PGS via its representation in terms of CGS (with infinite states). We start with the definition of ATL⋆ syntax.

Definition 3.1 (ATL⋆ Syntax) ATL⋆ formulas are built inductively from the set of atomic propositions AP and agents Ag, by using the following grammar, where p ∈ AP and A ⊆ Ag:

As syntactic sugar we also use ϕ1 ∨ ϕ2 ≜ ¬(¬ϕ1 ∧ ¬ϕ2), ϕ1 → ϕ2 ≜ ¬ϕ1 ∨ϕ2, ϕ1 ↔ ϕ2 ≜ (ϕ1 → ϕ2)∧(ϕ2 → ϕ1), [[A]]ϕ ≜ ¬〈〈A〉〉¬ϕ, Fϕ ≜ tUϕ, and Gϕ ≜ ¬F¬ϕ.

A sentence is a Boolean combination of ATL⋆ formulas of the form 〈〈A〉〉ψ. Intuitively, 〈〈A〉〉ψ means that each agent in A has a strategy such that, whatever the other agents do, the resulting play satisfies ψ.

We now provide some examples of ATL⋆ formulas that will be useful in the sequel. Precisely, we consider ϕ1 = 〈〈{s}〉〉(GFa ∧ GFb ∧ GFe), ϕ2 = 〈〈∅〉〉(GFa ∧ GFb ∧ GFe) and ϕ3 = 〈〈∅〉〉((ra ∧ X(¬eUrb)) → (Fgb → XFga)) over the sets AP and Ag given in Example 2.1. The formula ϕ1 states that agent s has a way to let propositions a, b, and e to occur infinitely often. The formula ϕ2 states that, no matters how the agents behave, propositions a, b, and e occur infinitely often. Finally, the formula ϕ3 states that, whenever a request rb occurs after an ra one in the same loading phase, then, if rb is eventually granted, then ra is granted later on as well.

We now provide the semantics of ATL⋆ .

Definition 3.2 (ATL⋆ Semantics) For a CGS G = 〈AP, Ag,Ac, St, tr, ap, s 〉 and a path π ∈ Pth, the modeling relation G, π |= ϕ is inductively defined as follows:

• The atomic and boolean cases are defined as usual;
• G, π |= 〈〈A〉〉ϕ if there is an assignment χA such that G, π′ |= ϕ, for all π′ ∈ play(χA, (π)0);
• G, π |= Xϕ if G, (π)≥1 |= ϕ;
• G, π |= ϕ1Uϕ2 if there exists j ∈ N such that G, (π)≥i |= ϕ1, for all i < j, and G, (π)≥j |= ϕ2.

For a sentence ϕ and two paths π, π with (π)0 = (π)0, it holds that G, π |= ϕ iff G, π |= ϕ. Indeed, according to the semantics of the existential quantification 〈〈A〉〉ψ, the only element of the path to take into account is the first one. For this reason, for a sentence ϕ we write G, s |= ϕ if G, π |= ϕ for some π ∈ Pth(s). Finally, we say that G satisfies ϕ, and write G |= ϕ, if G, s |= ϕ.

To get familiar with the semantics, consider the PGS P given in Example 2.1 and the formulas ϕ1, ϕ2, and ϕ3 given above. It is easy to see that GP |= ϕ1. Indeed, the strategy f that allows the scheduler to pick infinitely often the actions a, b, and un, makes all the generated paths to satisfy GFa∧GFb∧ GFe. On the other hand, it is easy to see that GP ̸|= ϕ2. Indeed, the strategy f for s such that f(ρ) = a, for all ρ ∈ Trk, never makes b and e to occur in the generated paths. Finally, we have that GP |= ϕ3.

Definition 3.3 (Model-checking) For a given PGS P and an ATL⋆ formula ϕ, the model-checking problem is to decide whether GP |= ϕ.

4 Model Checking

In this section, we provide a 3EXPTIME upper-bound and a 2EXPSPACE lower-bound for the model-checking problem of ATL⋆ over PGS.

4.1 Upper-bound Complexity

For the upper bound we use an automata-theoretic approach. We start with some notation and the definition of nondeterministic pushdown automata. See [Kupferman et al., 2002; 2000b] for more.

For a given set D ⊆ N, a D-tree T is a prefix closed subset of D∗ , i.e., a set in which, if x·d ∈ T then x ∈ T. The elements of T are called nodes and the empty word ε is called the root of T. For x ∈ T, the set of children of x is children(T, x) ≜ {x · i ∈ T : i ∈ D}. For x, y ∈ T, we write x ≺ y to mean that x is a proper prefix of y, i.e., there exists z ∈ D∗ such that x · z = y. For x ∈ T, a path in T from x is a minimal set π ⊆ T such that x ∈ π and for each y ∈ π such that children(T, y) ̸= ∅, there exist exactly one node in children(T, y) belonging to π. For an alphabet Σ, a Σlabeled tree is a pair T = 〈T, V〉 where T is a tree and V : T → Σ maps each node in T to an element in Σ. In the following, we mainly consider Σ to be the set power set 2AP of atomic propositions AP.

A Nondeteriministic Pushdown Tree Automata (PD-NTA, for short), over Σ-labeled trees, is a tuple A =〈Σ, Γ,Q, q, α0, δ, F〉, where Σ and Γ are finite input and stack alphabet sets, Q is a finite set of states, q is an initial state, α0 ∈ Γ∗ ·⊥ is an initial stack content, δ : Q×Σ× Γ⊥ → 22(Q×Γ∗ ) is a transition function such that, for all (q, σ, γ) ∈ Q × Σ × Γ⊥, δ(q, σ, γ) is a finite set, and F is an acceptance condition over Q.

When the automaton is in a state q, reading an input node x labeled with σ ∈ Σ, and the stack contains a word γ · α in Γ∗⊥, it chooses, for some k ∈ N, a tuple〈(q, β1), . . . , (qk, βk)〉 ∈ δ(q, σ, γ) and splits in k copies such that, for each 1 ≤ i ≤ k, the i-th copy is in the state qi and the stack content is updated by removing γ and pushing βi. Then, it reads the node x · i of the tree.

A run of a PD-NTA on a Σ-labeled tree T = 〈T, V〉 is a (Q × Γ∗⊥)-labeled tree 〈T, r〉 such that r(ε) = (q, α0) and for each x ∈ T with r(x) = (q, γ · α), there is a tuple〈(q, β1), . . . , (qk, βk)〉 ∈ δ(q, V(x), γ) for some k ∈ N, such that, for all 1 ≤ i ≤ k, r(x · i) = (qi, βi · α) if γ ̸= ⊥, and r(x · i) = (qi, βi · ⊥), otherwise.

Given a path π starting from ε, by infr(π) we denote the subset of states q such that there are infinitely many x ∈ π such that r(x) ∈ {q} × Γ∗⊥. A path satisfies a parity condition F = {F1, . . . , Fk}, with Fi ⊆ Fi+, for all i < k, and Fk = Q, if the minimum index 1 ≤ i ≤ k such that infr(π)∩Fi ̸= ∅ is even. A run〈T, r〉 is accepting if every path satisfies the acceptance condition. The PD-NTA A accepts an input tree 〈T, V〉 iff there is an accepting run of A over it. The language of A, denoted by L(A), contains all the trees accepted by A. The emptiness problem for PD-NTA is to decide, for a given A, whether L(A) = ∅. In [Kupferman et al., 2002] it is reported the following.

Theorem 4.1 The emptiness problem for a parity PD-NTA is EXPTIME-COMPLETE.

In several branching-time temporal-logic verification settings, the automata-theoretic approach has been fruitfully applied. Very close to our case are the procedures deployed for model checking pushdown systems over CTL⋆ specifications [Bouajjani et al., 1997; Bozzelli et al., 2010] and finitestate CGSs over ATL⋆ specifications [Alur et al., 2002]. The former is a top-down procedure that first builds an automaton accepting all the trees that satisfy the formula and then checks for the membership problem of the tree unwinding of the pushdown model. Precisely, to get a tight complexity, it starts with a single-exponential alternating 1 parity tree automaton and the membership problem results in a special alternating pushdown tree automaton named one-letter, with no blowup in size, whose emptiness can be checked in exponentialtime 2 resulting in an overall doubly-exponential time solution. The procedure for ATL⋆ , instead, uses a doubly-exponential bottom-up approach based on the idea of labeling each state of the structure with subformulas true in that state. In our setting we can neither proceed with the membership problem nor use a bottom-up procedure. Indeed, because of ATL⋆ , we need to consider not just the unwinding of the model but the tree execution induced by the player existentially quantified in the formula. Moreover, because of the possible infinite number of configurations induced by the PGS, a bottom-up procedure could never terminate. For this reason, we use a top-down approach that constructs a doubly exponential PD-NTA that simultaneously checks whether a tree is an execution of the structure and a model of the formula. As far as we know, this is the first top-down automata-theoretic approach exploited for ATL⋆ . Some details about this automata construction are reported in the following.

Theorem 4.2 The model-checking problem for ATL⋆ on PGS can be solved in 3EXPTIME.

Proof sketch: We give an intuition behind the automata construction by providing some details on how to extend the one introduced in [Bouajjani et al., 1997] used to solve the model-checking problem for branching-time specifications over pushdown systems. The mentioned approach starts with a tree automaton accepting all tree models of a formula ϕ, namely the formula automaton Aϕ, over which one can build a PD-NTA AP,ϕ accepting the unwinding of the pushdown structure P iff it is contained in the language of the formula automaton Aϕ. To handle ATL⋆ , one can start with a doublyexponential parity tree automaton as an adaptation of the one provided in [Schewe, 2008] 3 . Moreover, in order to correctly evaluate the formula over a PGS we need not just to consider the unwinding of the structure but rather the execution trees induced by the formula and precisely from the players existentially quantified in it. This results in selecting at each node subsets of children upon the choices of the players. As the number of these subsets is linear in the number of the decisions of the structure, the overall size of the PD-NTA we construct remains doubly-exponential. Thus, from Theorem 4.1 we derive a 3EXPTIME procedure. □

4.2 A Lower-bound Complexity

In this section, we show that the model-checking problem for ATL⋆ over PGSs is 2EXPSPACE-HARD by means of a reduction from the word acceptance problem for a deterministic Turing machine with doubly exponential space. Such reduction is inspired by the one provided in [Vester, 2014] for one-counter games.

1 Automata having as transition relation a positive Boolean combination of states and directions [Kupferman et al., 2000b].

2 Recall that in general the emptiness check for alternating pushdown automata is undecidable [Kupferman et al., 2002].

3 In [Schewe, 2008] it is given a single-exponential alternating automaton that can be easily translated into a non-deterministic one with a single exponential-time blowup.

Let T = 〈Q, q,Σ, δ, qF 〉 be a Turing machine that uses at most 22n cells on an input w of length n where, Q is the set of control states, q and qF are the initial and final states, respectively, Σ = {0, 1, a, r, ♯} is the finite alphabet set, and δ : Q×Σ→Q×Σ×{-1, 0,+1} is the (deterministic) transition function. For our convenience, if δ(q, a) = (q′ , a′ , x) we write δ1(q, a) = q′ , δ2(q, a) = a′ , and δ3(q, a) = x, respectively. The input set of T is given by ΣI = Σ\ {♯}. From this, we can construct a PGS PT ,w and an ATL⋆ formula ϕ such that T accepts w iff PT ,w |= ϕ. To do this, we need some auxiliary notation. First, w.l.o.g., we can assume that T always accepts when the symbol a is read, and always reject when the symbol r is read. Moreover, we can assume that T always halts in the position 1 of the tape and that there are two additional cells at the ends, numbered with 0 and 22n +1 containing the symbol a. Let ∆ = Σ∪(Q×Σ). Then a configuration is a sequence in ∆22n +2 containing exactly one element in Q×Σ. Since T is deterministic, then there is a unique run C w  · C w  · . . . of computations starting from C w  = a · (q,w) · . . .wn · ♯ · . . . · ♯ · a. C w i (j) denotes the j-th symbol of the i-th configuration in the computation. Observe that, given the three elements C w i (j - 1), C w i (j), and C w i (j + 1), then the symbol C w i+ (j) is uniquely determined, according to the definition of transition function. Then, for d ∈ ∆, by Pre(d) we denote the set of triples (d, d, d) such that d = C w i (j -1), d = C w i (j), d = C w i (j +1), and d = C w i+ (j).

At this point, we consider the auxiliary two-player turnbased one-symbol stack game RT ,w = 〈AP, {E, A}, Loc, LocE, LocA, R, ap, l〉 where:

• Loc = ([0, 22n + 1] × (∆ ∪ ∆3 )) ∪ {l, lz, lr, lF };
• LocE = ([0, 22n + 1] × ∆) ∪ {l};
• LocA = ([0, 22n + 1] ×∆3 ) ∪ {lz, lr, lF };
• R is the smallest relation such that:
• (l, x, l, push), for x ∈ {⊥, γ};
• (l, x, (1, (qF , a)), null) for x ∈ {⊥, γ};
• ((j, d), γ, (j, (d, d, d)), null) for all (d, d, d) ∈ Pre(d) and j ∈ [1, 22n ];
• ((j, a), x, lF , null) for all j ∈ [1, 22n ];
• ((j, d), x, lr, null) if j = 0 or j = 22n + 1;
• ((j, d), x, lz, null) if C w  (j) = d;
• (lz, γ, lF , null);
• (lz, γ, lr, pop);
• ((j, (d, d, d)), γ, (j -1, d), pop), for all j ∈ [0, 22n ] and d, d, d ∈ ∆;
• ((j, (d, d, d)), γ, (j, d), pop), for all j ∈ [0, 22n ] and d, d, d ∈ ∆;
• ((j, (d, d, d)), γ, (j +1, d), pop), for all j ∈ [0, 22n ] and d, d, d ∈ ∆.

Intuitively, player E pushes the symbol γ into the stack a number of times that corresponds to the length of the computation accepting w. After this, the game starts from the configuration (1, (qF , a), γ) and proceeds back-way along the computation of T over w. In the configurations with locations of the form (j, d), player E selects a possible predecessor triple (d, d, d) of d. At this point, player A selects one of the elements in (d, d, d), while a pop operation is performed on the stack. Finally, if the stack is empty and the location (j, d) is such that C w  (j) = d, then player E can move to configuration (lz, ⊥), from which player A is forced to move in location lF , since the transition (lz, γ, lr, pop) on empty stacks is deactivated. It is not hard to see that w is accepted by T iff player E can force the game RT ,w to reach lF .

This reasoning allows us to reduce the accepting problem to a reachability game played on RT ,w, which is of size doubly exponential w.r.t. to T , that can be specified by the ATL⋆ formula 〈〈E〉〉Fp, where p is the proposition labeling all the configurations having lF as location. Now, having RT ,w in mind, we can build a PGS PT ,w and an ATL⋆ formula ϕ such that PT ,w |= ϕ iff T accept w.

The construction of PT ,w is essentially a modification of RT ,w in which the position of the head on the tape is encoded by a suitable LTL formula ψ, rather than the set of states. This allows such a model to have polynomial size w.r.t. T and w. The way the formula ψ works is folklore and completely described in [Bozzelli et al., 2005; Kupferman et al., 2000a]. We omit it here due to the lack of space.

Finally, we can prove that PT ,w |= 〈〈E〉〉(ψ ∧ Fp) iff T accepts w, from which we derive the following theorem.

Theorem 4.3 The model-checking problem for ATL⋆ over PGS is in 2EXPSPACE-HARD.

5 Conclusion

In the last years, open pushdown models have received a lot of attention from the formal verification community, largely due to their ability to capture the control-flow of procedure calls and returns in reactive systems [Alur et al., 2005]. In several settings, the use of pushdown models allows to verify the correctness of infinite-state systems with a decidable complexity [Piterman and Vardi, 2004; Kupferman et al., 2002; Song and Touili, 2014]. As far as we know, all the work so far has concentrated on models with at most two-agents and with respect to specifications given in terms of classic temporal logics [Abdulla et al., ; Chatterjee and Velner, 2012; Bozzelli et al., 2010].

In this paper, we have introduced multi-agent pushdown game structures to model more involved infinite-state scenarios (as induced by a recursive structure) in which several agents can cooperate or act in an adversarial way in order to achieve a certain goal. As main contribution related to these structures we have introduced and studied the model checking problemwith respect to the logic ATL⋆ and showed that this problem can be solved in 3EXPTIME. We recall that the same complexity holds also for pushdown module checking with respect to specifications given in CTL⋆ . The latter is a special two-player setting, where one of the player, the environment, can also use nondeterministic strategies. We also provide a non tight 2EXPSPACE lower bound. Our conjecture is that the investigated problem is 3EXPTIME-COMPLETE. We leave this as future work.

On some extent, the high complexity of the addressed problem relies on the fact that the rich formalisms of pushdown models and ATL⋆ specification we combine are complex by themselves. While this allowed us to provide a result for a very general framework, the overall complexity can be easily reduced by considering opportune restrictions on both sides. Indeed, regarding the specification, by using ATL, the procedure easily reduces to 2EXPTIME. This is due the fact that it suffices to build a B¨uchi PD-NTA of single exponential size [Alur et al., 2002]. Further, one can restrict to pushdown models with bounded-stack. In several settings, it has been shown that under such a restriction the problem has the same or slightly higher complexity than the corresponding one for finite-state systems [Alur and Yannakakis, 2001; Aminof et al., 2012]. By employing techniques similar to the ones reported in [Alur and Yannakakis, 2001], we are confident that the model-checking problem of ATL specifications over bounded-stack PGS is PTIME-COMPLETE as it is for the case for CGS. If so, one can think of implementing an efficient model checker, as it has been done with MCMAS [Lomuscio and Raimondi, 2006; Cerm´ak et al., 2014]. This will be addressed as future work.

Another interesting setting to investigate is that of imperfect information under memoryless strategies. We recall that this setting is decidable in the finite-state case[Alur et al., 2002]. However, moving to pushdown systems one has to distinguish whether the missing information relies in the locations, in the pushdown store, or both. We recall that in pushdown module checking only the former case is decidable for specification given in CTL and CTL⋆ [Aminof et al., 2007; 2013].