Adrien Pommellet
email: adrien@lrde.epita.fr

Tayssir Touili

LTL Model Checking for Communicating Concurrent Programs

We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs).

The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al.

In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the lineartime temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.

Introduction

The use of parallel programs has grown in popularity in the past fifteen years, but these stay nonetheless fickle and vulnerable to specific issues such as race conditions or deadlocks. Static analysis methods for this class of programs remain therefore more relevant than ever.

The model checking framework has proven to be a cornerstone of modern static analysis techniques. The program is modelled as a simpler abstract mathematical model. Desirable properties and forbidden behaviours are then expressed using a well-defined logical framework, then checked against the abstract mathematical model of the program.

The linear-time temporal logic (LTL) encodes properties about the future of execution paths, that is, the sequence of configurations the model goes through. It can be used to express safety and liveness properties.

Pushdown systems (PDSs) were introduced to model the call stack of a program that stores information about the active procedures such as return addresses, passed parameters and local variables. Without such a stack, a finite-state automaton can't represent accurately programs with nested, recursive function calls, hence, the need for a more expressive model.

PDSs are a natural model for programs with sequential, recursive procedure calls [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF]. Thus, networks of pushdown systems can be used to model multi-threaded programs, where each PDS in the network models a sequential component of the whole program.

Communicating pushdown systems (CPDSs) were introduced by Bouajjani et al. in [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF] as a model for communicating multi-threaded programs. It is a natural abstraction: each thread is modelled as a PDS, and can synchronize by rendez-vous with other threads. Unfortunately, it has been proven by Ramalingam [16] that the reachability problem is undecidable for CPDSs. Therefore, the set of execution paths cannot be computed in an exact manner. To overcome this problem, Bouajjani et al. computed an abstraction of the execu-tion paths language, using a framework based on Kleene algebras.

Solving the model checking problem of LTL for the class of CPDSs would be a worthy addition to the existing verification techniques. However, this problem is obviously undecidable: we therefore seek an approximate answer.

Our contributions in this paper are the following:

-We define the semantics of single-indexed LTL formulas for CPDSs, that is, formulas of the form ϕ = (ψ 1 , . . . , ψ n ), where each LTL sub-formula ψ i must hold for the i-th process with regards to the synchronized CPDS semantics. -We show how to abstract the set of accepting traces of a Büchi pushdown system. To do so, we use the abstraction framework of [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF] as well as the LTL model checking methods for PDSs introduced by Esparza et al. in [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF]. -We use this abstraction on isolated pushdown components of the whole program in order to approximate the single-indexed LTL model checking problem for CPDSs. -As a new contribution of the journal version of this article, we extend the abstraction framework to universal single-indexed model checking and stutter invariant LTL formulas. -We apply this abstraction framework to detect race conditions in a toy example.

Some of these results were first presented in the conference version of this paper [START_REF] Pommellet | LTL model-checking for communicating concurrent programs[END_REF].

Related Work. Multi-stack pushdown systems (from then on MPDSs) are pushdown systems with two or more stacks; this class of automata can be used to model synchronized parallel programs. Qadeer et al. solved the model checking problem of LTL given a context bounding constraint on runs in [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF], where a context is an uninterrupted sequence of actions on a single thread. This result still holds with a weaker phase-bounding constraint, where only a single stack can be popped from during a phase, as proven by La Torre et al. in [START_REF] Torre | A robust class of context-sensitive languages[END_REF].

Atig introduced in [START_REF] Atig | Model-checking of ordered multi-pushdown automata[END_REF] ordered multi-pushdown automata, a sub-class of MPDSs such that the stacks are ordered and only the first-non empty stack can be popped from. Given this constraint, the model checking problem of LTL can be solved within an 2-ETIME upper bound. These models depend on bounding constraints on runs; our abstraction framework, while less accurate, does not.

Dynamic pushdown networks (DPNs) were introduced by Bouajjani et al. in [START_REF] Bouajjani | Regular symbolic analysis of dynamic networks of pushdown systems[END_REF]. A DPN models a concurrent program as a network with an unbounded number of pushdown components that can spawn new threads, also modelled as pushdown systems. Song et al. described in [START_REF] Song | Model-checking dynamic pushdown networks[END_REF] a model checking framework for singleindexed LTL and CTL formulas. A DPN can spawn new threads according to a finite number of patterns, since it has a finite number of rules. A single-indexed formula on a DPN is defined as a tuple ϕ = (ψ 1 , . . . , ψ n ), where each component ψ i is a formula that must hold for the i-th thread pattern. While CPDSs can't model thread spawns, DPNs do not feature synchronization between threads, a crucial aspect of concurrent programs. Song et al. later added in [START_REF] Song | LTL model-checking for dynamic pushdown networks communicating via locks[END_REF] locks that prevent some transitions from being performed by a thread if a common resource shared with other components has not been released beforehand. This is a weaker form of synchronization than communication by rendez-vous.

Synchronized dynamic pushdown networks (DPNs) were later introduced by Pommellet et al. in [START_REF] Pommellet | Static analysis of multithreaded recursive programs communicating via rendez-vous[END_REF]. The reachability problem for this class of automata is undecidable but can be abstracted. Abstractions for the model checking problem, however, have yet to be defined.

Paper outline. The paper is organised as follows. In Section 2, we present communicating pushdown systems (CPDSs) and detail how they can be used to model programs. In Section 3, we define the single-indexed linear-time temporal logic for CPDSs and remind the reader of results on the LTL model checking problem for PDSs. We briefly describe in Section 4 the abstraction framework designed by Bouajjani et al. in [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF] to overapproximate the set of execution paths of a PDS. In Section 5, as a main contribution of this paper, we introduce an abstract model checking algorithm for singleindexed LTL. We then extend the abstraction framework to stutter-invariant LTL formulas in Section 6. We then apply this scheme in order to detect a race condition in Section 7. Finally, we show our conclusion in Section 8.

Communicating Pushdown Systems

Pushdown systems

Pushdown systems are a natural model for sequential programs with recursive procedure calls.

Definition 1 (Pushdown system) A pushdown system (PDS) is a tuple P = (P, Σ, Γ, ∆, c 0 ) where P is a finite set of control states, Σ a finite input alphabet, Γ a finite stack alphabet, ∆ ⊆ P × Γ × Σ × P × Γ * a finite set of transition rules, and c 0 ∈ P × Γ * a starting configuration.

If d = (p, γ, a, p , w) ∈ ∆, we write d = (p, γ) a -→ (p , w). We call a the label of d. We can assume without loss of generality that ∆ ⊆ P × Γ × Σ × P × Γ ≤2 .

A configuration of P is a pair p, w where p ∈ P is a control state and w ∈ Γ * a stack content. Let Conf P = P × Γ * be the set of all configurations of P.

The reachability relation. For each a ∈ Σ, we define the transition relation a -→ P on configurations as follows: if (p, γ) a -→ (p , w) ∈ ∆, for each w ∈ Γ * , p, γw a -→ P p , ww . Intuitively, the automaton moves from state p to p while the symbol γ is popped from the stack and a word w is pushed on the stack.

From these relations, we can then infer the immediate successor relation → P = a∈Σ a -→ P . The reachability relation ⇒ P is the reflexive and transitive closure of the immediate successor relation → P . If C is a set of configurations, we introduce its set of predecessors pre * (P, C) = {c ∈ P × Γ * | ∃c ∈ C, c ⇒ P c }. We may omit the variable P when only a single PDS is being considered.

A run r starting from a configuration c is a sequence of configurations r = (r i ) i≥0 such that r 0 = c and ∀i ≥ 0, r i ai -→ P r i+1 . The word (a i ) i≥0 is then said to be the trace matched to r. Traces and runs may be finite or infinite.

Let Runs ω (P, C) (resp. Runs(P, C)) be the set of all infinite (resp. finite) runs of P starting from a configuration c ∈ C. We define Traces ω (P, C) and Traces(P, C) in a similar manner.

If P's initial configuration is c 0 , we introduce the set Runs ω (P) = Runs ω (P, {c 0 }). We define Runs(P), Traces(P), and Traces ω (P) in a similar manner.

Many static analysis methods rely on being able to determine whether a given critical state is reachable or not from the starting configuration of a program, hence, the need for reachability analysis techniques.

Regular sets of configurations. A set of configurations C of a PDS P is said to be regular if ∀p ∈ P , there exists a finite-state automaton A p on the alphabet Γ such that L(A p ) = {w | p, w ∈ C}, where L(A) stands for the language recognized by an automaton A.

The following property holds:

Theorem 1 (Caucal [START_REF] De Alfaro | On the regular structure of prefix rewriting[END_REF]) Given a PDS P and a regular set of configurations C, the set of configurations pre * (C) is regular.

Moreover, pre * (C) is effectively computable [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF].

The model and its semantics

Let us consider a program with n threads. Let Act be a set of actions (input alphabet) such that:

-Act contains a special action τ that represents internal actions of a thread. -Each pair (i, j) of threads in the network uses a dedicated set of signals Lab i,j = Lab j,i disjoint from the other sets of signals and from the internal action τ . If we define Lab i =

j =i Lab i,j , then Act/{τ } = i=1,...,n
Lab i ; we write Lab = Act/{τ }.

We then consider the following concurrent pushdown model: Definition 2 (Bouajjani et al. [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF]) A communicating pushdown system (CPDS) on the alphabet Act is a tuple CP = (P 1 , . . . , P n ) of pushdown systems such that each component P i has input alphabet Lab i ∪ {τ }.

Configurations and transitions

. A global configuration of CP is a n-tuple g = (c 1 , . . . , c n ) of configurations in Conf P1 × . . . × Conf Pn = Conf CP . The global starting configuration of CP is the tuple g 0 = (c 1 0 , . . . , c n 0 )
where c i 0 is the starting configuration of the component P i .

We define the following transition relation a -→ CP on global configurations:

-(c 1 , . . . , c n ) τ -→ CP (c 1 , . . . , c n ) if
there exists an index i such that c i τ -→ Pi c i and c j = c j for all j = i. A single process applies a pushdown operation on its own stack.

-(c 1 , . . . , c n ) a -→ CP (c 1 , . . . , c n ) if there exist two in- dices i and j, i = j, such that a ∈ Lab i,j , c i a -→ Pi c i , c j a
-→ Pj c j and c k = c k for all k = i and k = j. Two synchronized processes perform a simultaneous action.

Intuitively, a thread can either perform an internal action labelled by τ , or must synchronize with another thread in order to perform an action labelled by a common synchronization signal in Lab.

We define runs and traces with regards to this transition relation in a manner similar to PDSs: a run is a sequence of global configurations starting from g 0 and connected by transition rules; its matching trace is the sequence of labels of these transitions.

Example 1 (A global run) We consider three runs

a 1 τ -→ P1 b 1 x -→ P1 c 1 a 2 x -→ P2 b 2 y -→ P2 c 2 a 3 y -→ P3 b 3
on three PDSs P 1 , P 2 , and P 3 . Then

(a 1 , a 2 , a 3 ) τ -→ CP (b 1 , a 2 , a 3 ) x -→ CP (c 1 , b 2 , a 3 ) y -→ CP (c 1 , c 2 , b 3 )
is a global run g of (P 1 , P 2 , P 3 ). An internal transition of P 1 is followed by a synchronized transition between P 1 and P 2 , then another synchronized transition between P 2 and P 3 .

Given a global run g, we define g i as its projection on its i-th component Conf Pi .

Example 2 (Projecting a global run) The projection g 3 of the global run

(a 1 , a 2 , a 3 ) τ -→ CP (b 1 , a 2 , a 3 ) x -→ CP (c 1 , b 2 , a 3 ) y -→ CP (c 1 , c 2 , b 3 ) on Conf P3 is a 3 τ -→ CP a 3 x -→ CP a 3 y -→ CP b 3
Note that it is not a run of P 3 .

From a concurrent program to a CPDS model

We can assume that the concurrent program is represented by a n-tuple of control flow graphs, whose nodes represent control points of threads or procedures and whose edges are labelled by statements.

These statements can be variable assignments, procedure calls or returns, or communications between threads through unidirectional point-to point channels, where a thread sends a value x through a channel ch and another thread waits for this value then assigns it to a variable.

Without loss of generality, we assume that each thread can share some variables (from now on called thread variables) with the procedures it calls, but that there are no global variables shared between threads. We also consider that both local and thread variables can only take a finite number of values by abstracting their domain if needed.

As a consequence, threads can only synchronize through unidirectional, point-to-point channels: for all 1 ≤ i, j ≤ n, i = j, there is a channel ch i,j that allows thread i to send values to another thread j. With a send statement ch i,j !(x), a value x is sent through channel ch i,j from thread i to thread j. With a receive statement ch i,j ?(x), the value x from thread i received through channel ch i,j is assigned to a variable in thread j.

For each control flow graph, we will define a corresponding PDS P = (P, Act, Γ, ∆, c init ). The set of states P is the set of all possible valuations of thread variables (i.e. variables shared amongst procedures called by this thread). The stack alphabet Γ is the set of all pairs (n, l) where n is a node of the control flow graph and l is a valuation of the local variables of the current procedure. The whole program will be modelled by a tuple of these PDSs.

Lab i,j is the set of all possible synchronization actions ch i,j (x) between the components P i and P j : value x is carried from the i-th thread to the j-th thread through channel ch i,j . The set Act = τ i =j Lab i,j also contains an internal action τ .

For each statement s labelling an edge of the flow graph between nodes n 1 and n 2 , we introduce the following transition rules in the corresponding PDS, where t 1 and t 2 (resp. l 1 and l 2 ) are the valuations of thread (resp. local) variables before and after the execution of the statement:

-If s is an assignment, it is represented by a rule of the form:

(t 1 , (n 1 , l 1 )) τ -→ (t 2 , (n 2 , l 2 ))
Assigning a new value to a variable in t 1 or l 1 results in a new valuation t 2 or l 2 . Note that we have either t 1 = t 2 or l 1 = l 2 , depending on whether the value is assigned to a local variable (in the former case) or a thread variable (in the latter case). -If s is a procedure call, it is represented by a rule of the form

(g 1 , (n 1 , l 1 )) τ -→ (g 1 , (f 0 , l 0 )(n 2 , l 1 ))
where f 0 is the starting node of the called procedure and l 0 the initial valuation of its local variables. if s is a procedure return, it is represented a rule of the form

(t 1 , (n 1 , l 1 )) τ -→ (t 2 , ε)
We simulate returns of values by introducing an additional thread variable and assigning the return value to it in the valuation t 2 . -If s is an assignment ch?(x) of a value x carried through a channel ch, it is represented by a rule of the form

(t 1 , (n 1 , l 1 )) ch(x) ---→ (t 2 , (n 2 , l 2 ))
where t 1 and t 2 (resp. l 1 and l 2 ) are such that assigning the value x to a variable in t 1 (resp. l 1 ) results

in a new valuation t 2 (resp. l 2 ). Note again that we have either t 1 = t 2 or l 1 = l 2 , depending on whether the variable modified belongs to a procedure or a thread. -If s is an output ch!(x) through a channel ch of the value x, it is represented by rules of the form

(t 1 , (n 1 , l 1 )) ch(x) ---→ (t 1 , (n 2 , l 1 ))
such that the variable copied and sent through the channel has value x in either t 1 or l 1 .

Finally, we consider the starting configuration of each process c init = (t init , (n init , l init )) where t init and l init are respectively the initial valuations of the thread and local variables, and n init the starting node of its initial procedure.

LTL Model Checking on CPDSs

The most widely used variant of temporal logics is the linear-time temporal logic LTL introduced by Pnueli in [START_REF] Pnueli | The temporal logic of programs[END_REF].

The linear-time temporal logic LTL

Let AP be a finite set of atomic propositions used to express facts about a program. A path is an infinite word π = (π i ) ≥ 0 in the set Paths = (2 AP ) ω .

Definition 3 (LTL)

The set of LTL formulas is given by the following grammar:

ϕ, ψ ::= True | p ∈ AP | ¬ϕ | ϕ ∨ ψ | X ϕ (Next) | ϕ U ψ (Until)
X and U are called the next and until operators: the former means that a formula should happen at the next step, the latter, that a formula should hold at least until another formula becomes true. We consider the following semantics on paths: Definition 4 (Semantics of LTL) Let ϕ be a LTL formula, π ∈ Paths, and i ∈ N. We define inductively the semantics of the relation π, i |= ϕ:

π, i |= ρ where ρ ∈ AP ⇔ ρ ∈ π i π, i |= X ϕ ⇔ π, i + 1 |= ϕ π, i |= ϕ U ψ ⇔ ∃j ≥ i, π, j |= ψ and ∀k ∈ {i, . . . , j -1} , π, k |= ϕ π, i |= ϕ ∨ ψ ⇔ (π, i |= ϕ) ∨ (π, i |= ψ) π, i |= ¬ϕ ⇔ π, i |= ϕ π, i |= True always.
Intuitively, π, i |= ϕ means that the path π verifies ϕ from its i-th symbol onward. We consider the language L(ϕ) = {w | w ∈ (2 AP ) ω and w, 0 |= ϕ} of an LTL formula ϕ, that is, the set of all paths verifying ϕ according to the semantics outlined previously.

For convenience's sake, we introduce the operators F ϕ = (True U ϕ) and G ϕ = ¬(F ¬ϕ) that stand respectively for finally and globally.

LTL and Büchi automata. We consider the following class of finite state automata:

Definition 5 (Büchi automaton) A Büchi automa- ton (BA) B is a tuple (Q, Σ, δ, q 0 , G) where Q is a finite set of states, Σ a finite input alphabet, δ ⊆ Q × Σ × Q a set of transitions, G ⊆ Q a set
of accepting states, and q 0 ∈ Q the initial state.

The language L(B) accepted by B is the set of all infinite sequences w in Σ ω such that there is an infinite run r of B with trace w starting in state q 0 that visits accepting states in G infinitely often.

BA can be used in the following fashion:

Theorem 2 (Kesten et al. [START_REF] Kesten | A decision algorithm for full propositional temporal logic[END_REF]) Given a LT L formula ϕ, there exists an effectively computable Büchi automaton B on the alphabet Σ = 2 AP such that L(B) = L(ϕ).

LTL model checking for PDSs

Let ν : Conf P → 2 AP be a valuation function on configurations of a PDS P = (P, Act, Γ, ∆, c 0 ). It is said to be simple if for all w, w ∈ Γ * , p ∈ P , and γ ∈ Γ , we have ν( p, γw ) = ν( p, γw ). Intuitively, a simple valuation is equivalent to a function ν : P × Γ → 2 AP that only depends on the control state and the top stack symbol. Let r = (r i ) i≥0 be an infinite run of P. We define the image ν(r) = (ν(r i )) i≥0 in Paths of r by the valuation function ν. We write that r |= ν ϕ if ν(r), 0 |= ϕ. The model checking problem is defined as follows:

Definition 6 (Model checking) Given an LTL formula ϕ, a PDS P with a starting configuration c 0 , and a simple valuation ν on configurations of P, the existential model checking problem consists in determining whether ∃r ∈ Runs ω (P), r |= ν ϕ.

Obviously, since the negation of an LTL formula is still an LTL formula as well, determining whether ∀r ∈ Runs ω (P), r |= ν ϕ is an equivalent problem, called the universal model checking problem. Indeed:

¬(∀r ∈ Runs ω (P), r |= ν ϕ) ⇔ (∃r ∈ Runs ω (P), r |= ν ¬ϕ)
We will now present the automata-theoretic framework introduced in [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF][START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF] in order to solve the existential model checking problem.

Using Büchi pushdown automata. We consider the following class of automata: Definition 7 (Büchi pushdown automata) A Büchi pushdown automaton (BPDA) is a tuple BP = (P, Act, Γ, ∆, c 0 , G) such that (P, Act, Γ, ∆, c 0 ) is a PDS and G ⊆ P a set of accepting states.

In a similar manner to BA, an accepting run of BP is an infinite run of the PDS (P, Act, Γ, ∆, c 0 ) that visits infinitely often configurations whose control state is in G. To these runs, we match accepting traces.

A BPDA can be seen as a product automaton between a PDS and Büchi automaton. The use of this class of automata is the following: Theorem 3 Given a PDS P and an LTL formula ϕ, there exists an effectively computable BPDA BP such that t is an accepting trace of BP if and only if t is a trace of P matched to a run r such that r |= ν ϕ.

Thus, if we can solve the emptiness problem for BPDA, then we can solve the model-checking problem of LTL for PDSs as well. Indeed, if L(BP) = ∅, then there is no run r such that r. |= ν ϕ.

Repeating heads and the emptiness problem. A repeating head of BP is an element p, γ of G × Γ such that ∃w ∈ Γ * , p, γ → + BP p, γw . Let Rep(BP) be the finite set of repeating heads of BP. The following lemma characterizes accepting runs with regards to repeating heads: Lemma 1 r is an accepting run of a BPDA BP if and only if BP has a repeating head p, γ such that r visits configurations in p, γΓ * infinitely often.

Therefore, a run of a BPDA is accepting if and only if it visits a repeating head infinitely often. Moreover, the set of repeating heads is obviously finite, being a subset of P × Γ , and can be effectively computed in

O(|P | • |∆| 2 ) time and O(|P | • |∆|) space [7]. Let Rep(BP)Γ * = { p, γw | p, γ ∈ Rep(BP), w ∈ Γ * }
be the regular set of configurations starting with a repeating head. A BPDA will admit at least one accepting run if and only if there exists a repeating head reachable from the initial configuration, hence, the following theorem:

Theorem 4 Given a BPDA BP with starting configuration c 0 , its language L(BP) is not empty if and only pre * (Rep(BP)Γ * ) ∩ {c 0 } = ∅.

Since the set pre * (Rep(BP)Γ * ) is regular and effectively computable by Theorem 1, we can therefore solve the model checking problem using Theorems 3 and 4.

Single-indexed LTL model checking for CPDSs

Let CP = (P 1 , . . . , P n ) be a CPDS, ν a simple valuation function on Conf P1 ∪. . .∪Conf Pn , and for i = 1, . . . , n, let ψ i be an LTL formula. The tuple ϕ = (ψ 1 , . . . , ψ n ) is said to be a single-indexed LTL formula.

We define the following semantics for single-indexed LTL formula on CPDSs: Definition 8 (Single-indexed LTL semantics) Given a CPDS CP = (P 1 , . . . , P n ), an infinite global run g of CP, a simple valuation on pushdown components ν, and a single-indexed LTL formula ϕ = (ψ 1 , . . . , ψ n ), g |= ν ϕ if and only if for each i = 1, . . . , n, g i |= ν ψ i . Finding such a global run g is called the existential single-indexed model checking problem.

Intuitively, each PDS P i in the CPDS satisfies its own LTL formula ψ i , but does so while synchronizing with the others PDSs. This is a simpler problem than solving the existential model checking for a single LTL formula and a valuation function on global configurations: we will therefore try to solve it first, then focus later on the general case.

If the single-indexed model checking problem for CPDSs were decidable, so would be the reachability problem. However, it has unfortunately been proven by Ramalingam in [START_REF] Ramalingam | Context-sensitive synchronization-sensitive analysis is undecidable[END_REF] that this problem is undecidable for synchronization-sensitive pushdown systems. Hence, since the latter reachability problem is obviously undecidable, the former model checking problem is as well.

We therefore seek to get at least an approximate answer to this problem. The issue with single-indexed model checking is the following: for each i = 1, . . . , n, there may exist a run r i of the PDS P i satisfying a formula ψ i , but a global, synchronized run on the CPDS (P 1 , . . . , P n ) satisfying ϕ = (ψ 1 , . . . , ψ n ) may not exist if the individual pushdown components of the system can't synchronize. We will tackle this issue in the next section.

An Abstraction Framework for Traces

We want to abstract the single-indexed LTL model checking problem for CPDSs. To this end, we seek to over-approximate the set

L P (C , C) = {t ∈ Traces(P)|∃c ∈ C, ∃c ∈ C , c t - → * P c}
of traces of a PDS P leading from a regular set of configurations C to another C. We will use the mathematical framework introduced by Bouajjani et al. in [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF] to approximate the reachability problem for CPDSs. More details can be found in the appendix.

To this end, they consider a Kleene algebra K = (A, ⊕, , 0, 1) matched to an abstract lattice E = (A, ≤, , , ⊥, ) and a Galois connection that consists in an abstraction function α : Act * → K and a concretization function β : K → Act * such that, given two languages L 1 and L 2 on the alphabet Act: 1: From Act * to the abstract domain K and back again.

L 1 ⊆ β(α(L 1 )) L 2 ⊆ β(α(L 2 )) α(L 1 ) α(L 2 ) = ⊥ ⇔ β(α(L 1 )) ∩ β(α(L 2 )) = ∅ L 2 L 1 β(α(L 2 )) β(α(L 1 )) α(L 1 ) α(L 2 ) α α β β Act * K Fig.
Hence, as shown in Figure 1, the Galois connection can be used to over-approximate a language in 2 Act * (e.g. the trace language of a PDS), and we can directly check the emptiness of the intersection (a common operation as far as model checking goes) of these approximations in a simpler, often finite domain. Here are two examples of such finite-domain Kleene abstractions: Example 3 (The prefix abstraction) Let n ≥ 1 be an integer and W (n) = {w ∈ Act * | |w| ≤ n} be the set of words of length smaller than n.

We define the n-th order prefix abstraction α pref n as follows:

-The abstract lattice A = 2 W is generated by the elements v a = {a}, a ∈ Act. -⊕ = ∪. -U V = {pref n (uv) | u ∈ U, v ∈ V } where pref n (w)
stands for the prefix of w of length n (or lower if w is of length smaller than n). -0 = ∅ and 1 = {ε}.

From there, we build an abstract lattice where = W , = ∩, and ≤=⊆.

This abstraction is accurate for the n-th first steps of a trace: the other steps are then over-approximated by Act * for a finite trace or Act ω for an infinite trace. Hence, if w ∈ Act ω , then the prefix abstraction of {w} is

α pref n ({w}) = {pref n (w)} its matching connection β pref n ({p}) = p • Act *
and the resulting over-approximation the language

β pref n (α pref n ({w})) = pref n (w) • Act * Example 4 (First occurrence ordering) Let W be the set of words {w ∈ Act * | ∀a ∈ Act, |w| a ≤ 1}
where each letter occurs at most once (|w| a is the number of a in the word w).

We define the first occurrence ordering abstraction α foo as follows:

-The abstract lattice A = 2 W is generated by the elements v a = {a}, a ∈ Act -⊕ = ∪. -U V = {uv | u ∈ U and ∃v ∈ V, v is the projec- tion of v on letters not occuring in u}. -0 = ∅ and 1 = {ε}.
From there, we build an abstract lattice where = W , = ∩, and ≤=⊆.

If w is a trace in Act * , its first occurrence ordering is

α foo ({w}) = a 1 . . . a n
where the set of letters in w is exactly {a 1 , . . . , a n } and they first appear in the order a 1 , . . . , a n . Its matching connection is

β foo (a 1 •. . .•a n ) = a 1 a * 1 a 2 (a 1 +a 2 ) * . . . a n (a 1 +. . .+a n ) *
The resulting over-approximation is

β foo (α foo ({w})) = a 1 a * 1 a 2 (a 1 +a 2 ) * . . . a n (a 1 +. . .+a n ) *
Example 5 Let w = aacbabed(ab) ω . Then:

α pref 5 ({w}) = aacbabed(ab) ω α foo ({w}) = aacbabed(ab) ω
A finite-chain abstraction is such that the lattice (A, ≤) has no infinite ascending chains: as a consequence, infinite sequences of concatenations can be defined and effectively computed, and the abstraction framework can be applied to countably infinite traces. The prefix and first occurrence ordering abstractions defined previously are finite-chain.

Abstract Model Checking of LTL for CPDSs

In this section, as a main contribution of this paper, we will introduce an approximation framework for singleindexed LTL model checking on CPDSs.

Abstracting accepting traces of a BPDA

We show in this subsection how to over-approximate the set of accepting traces of BPDA. To do so, we extend the abstract reachability analysis introduced in [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF] to infinite runs.

Properties of accepting runs of BPDA. By Lemma 1, to each accepting run r of a BPDA BP, we can match a repeating head p, γ ∈ Rep(BP) that it visits infinitely often. Conversely, if a run r of a BPDA BP visits a repeating head p, γ ∈ Rep(BP) infinitely often, it is then obviously accepting since Rep(BP) ⊆ G × Γ . We will use the former property to abstract the set of accepting traces.

Let p, γ ∈ Rep(BP) be a repeating head. An accepting trace visiting the set p, γΓ * infinitely often can be split into two parts:

(1) first, it must reach the set p, γΓ * from the initial configuration c 0 ; (2) then, it must infinitely often move from p, γΓ * to p, γΓ * , using a sequence of transitions of length superior or equal to one.

Part (1) of an accepting trace visiting p, γ must therefore be in the set L BP ({c 0 }, p, γΓ * ), and part (2), in the set [L BP ( p, γΓ * , p, γΓ * )/{ε}] ω .

As a consequence, the set

L BP ({c 0 }, p, γΓ * ) • (L BP ( p, γΓ * , p, γΓ * )/{ε}) ω
is an over-approximation of the set of accepting traces visiting the repeating head p, γ infinitely often. Since it cannot be computed directly, we will apply the framework of Section 4 to abstract it.

Abstracting the set of accepting traces. Our method to abstract the set of accepting traces of a BPDA BP is the following: As a consequence, the following theorem holds: Theorem 5 Given a BPDA BP, we can compute a finite-chain abstraction of its set of accepting traces L(BP).

Abstracting the single-indexed model checking problem for CPDSs

Let CP = (P 1 , . . . , P n ) be a CPDS and ϕ = (ψ 1 , . . . , ψ n ) a single-indexed LTL formula. Our goal is to compute an over-approximation of the undecidable singleindexed LTL model checking problem, i.e. compute an over-approximation of the set of runs of CP verifying ϕ; if this over-approximation is empty, so is the actual set of runs verifying ϕ, and the answer to the existential single-indexed model checking problem is negative.

Our intuition is, for each component P i , to abstract the set of paths verifying ψ i , then examine the emptiness of the intersection of these abstractions. However, in a global run of a CPDS, the execution paths of the pushdown components are interleaved. Synchronization signals between two threads j and k may occur in the global run but will not appear in local runs of the i-th pushdown component. We cannot therefore study the paths of a pushdown system P i in isolation from the other components.

Projecting global runs. For each pushdown component

P i = (P i , Lab i ∪ {τ }, Γ, ∆ i , c i 0 ) of a CPDS CP = (P 1 , . . . , P n ), we introduce a new PDS P i = (P i , Act, Γ, ∆ i , c i 0 ) such that: -∆ i ⊆ ∆ i ; the new PDS P i extends the pushdown component P i . -For all p ∈ P i , γ ∈ Γ , and x ∈ {τ } ∪ j =i =k Lab j,k , (p, γ) x -→ (p, γ) ∈ ∆ i .
We add to each control state self-loops labelled either by the internal action τ or by every synchronization signal in Lab j,k between pair of different processes j and k for all j = i = k.

The PDS P i can either simulate P i or self-loop and output any possible signal emitted by other processes, be it an internal action or a synchronization between two other processes.

Given two regular sets of configurations C and C of P i , and the language L Pi (C , C) of traces leading from C to C, we have

L P i (C , C) = L Pi (C , C) ({τ } ∪ j =i =k Lab j,k ) *
where is the interleaving operator: we shuffle the paths of P i with internal and synchronization actions of other threads.

As a consequence, it allows us to over-approximate projections of the set of global runs: Lemma 2 Let g be a global run of the CPDS CP. Then g i is a run of P i .

Intuitively, we can prove recursively that, at every step of g i , we can either use an existing transition of P i if this step of the global run g involved the i-th component, or simulate any action performed by other threads with one of P i 's own self-loops.

Application to the model checking problem. Let g be a global run of CP and ϕ = (ψ 1 , . . . , ψ n ) a single-indexed LTL formula. Then g |= ν ϕ if and only if for each i = 1, . . . , n, g i |= ν ψ i .

By Lemma 2, if ∀r ∈ Runs ω (P i ), r |= ν ψ i , then g i |= ν ψ i . By Theorem 3, there exists a BPDA BP i such that L(BP i ) is the set of all traces of runs of P i verifying ψ i . L(BP i ) is empty if and only if ∀r ∈ Runs ω (P i ), r |= ψ i .

The projections g 1 , . . . , g n of a global run g have the same trace as the original run g. As a consequence, even if we can find in the automata P 1 , . . . , P n runs accepting the LTL formulas ψ 1 , . . . , ψ n , they can't be projections of a same accepting global run if they don't share the same trace.

We can use this property as a discriminating criterium for the existential single-indexed LTL model checking problem: we compute an abstraction of the set of accepting traces α(L(BP i )) of each BPDA BP i then check if these abstractions share a common trace.

Theorem 6 If α(L(BP 1 )) . . . α(L(BP n )) = ⊥, then there is no global run of CP accepting the single-indexed LTL formula ϕ.

Proof (Theorem 6) Let us assume that there exists a global run g of CP such that g |= ϕ. Let g i be its projection on the component P i . g i is a run of P i by Lemma 2, hence, its trace t i should belong to the overapproximation β(α(L(BP i )) of the set of traces of BP i .

However, the projections g 1 , . . . , g n of g all have the same trace as g, hence, t 1 = . . . = t n = t. As a consequence

t ∈ β(α(L(BP 1 )) ∩ . . . ∩ β(α(L(BP n ))
This set is therefore not empty, hence, by definition of Galois connections, α(L(BP 1 )) . . . α(L(BP n )) = ⊥ and there is a contradiction.

We can decide in a finite-chain domain if α(L(BP 1 )) . . . α(L(BP n )) = ⊥ Hence, Theorem 6 can be used to approximate the existential single-indexed model-checking problem.

The universal single-indexed model checking problem

We now try to apply our abstraction framework to the universal model checking problem: Definition 9 (Universal model checking) Given a CPDS CP = (P 1 , . . . , P n ) of CP, a simple valuation on pushdown components ν, and a single-indexed LTL formula ϕ, CP |= ν ϕ if and only if for each global run g of CP, g |= ν ϕ. Determining whether this property hold is called the universal single-indexed model checking problem.

Unlike LTL formulas, we don't know if the negation of a single-indexed LTL formula is also a single-indexed LTL formula. However, the following property holds:

¬(CP |= ν ϕ) = ¬(∀g ∈ Runs ω (CP), ∀i ∈ {1, . . . , n}), g i |= ν ψ i ) = ∃g ∈ Runs ω (CP), ∃i ∈ {1, . . . , n}, g i |= ν ψ i = ∃i ∈ {1, . . . , n}, ∃g ∈ Runs ω (CP), g i |= ν ¬ψ i = i∈{1,...,n} ∃g ∈ Runs ω (CP), g i |= ν ¬ψ i = i∈{1,...,n} ∃g ∈ Runs ω (CP), g |= ν ϕ i
Where ϕ i is a single-indexed LTL formula such that its i-th component is the LTL formula ¬ψ i and all the others are T rue.

As a consequence, at least one single-indexed existential model checking property "∃g ∈ Runs ω (CP), g |= ν ϕ i " holds true if and only if CP |= ν ϕ. Conversely, all the existential properties are wrong if and only if CP |= ν ϕ.

A summary of our abstraction procedures

In order to approximate the existential single-indexed model checking problem "Given a CPDS CP = (P 1 , . . . , P n ), a single-indexed LTL formula ϕ = (ψ 1 , . . . , ψ n ), and a simple valuation on pushdown components ν, is there a global run g of CP such that g |= ν ϕ?"

we apply the following procedure:

1. For each component P i , compute the altered PDS P i . 2. Then compute the product BPDA BP i of P i and ψ i according to Theorem 3 3. Compute the abstraction α(L(BP i )). 4. Check that α(L(BP 1 )) . . . α(L(BP n )) = ⊥. 5. If this is true, then by Theorem 6, the answer to the existential single-indexed model checking problem is negative. 6. However, if this is not the case, we can't draw any immediate conclusion. We may use the abstract counter-example to help us find an actual run of CP that verifies ϕ. We may also refine the Kleene abstraction by increasing its order if it's a prefix abstraction.

Note that, as an optimization, we can perform an emptiness check on the BPDA BP i before abstracting its language α(L(BP i )). If L(BP i ) = ∅, then there is obviously no global run g such that g i |= ν ψ i and the answer to the existential problem is negative. By doing so, we avoid computing the abstraction α(L(BP i )) that may lead to spurious counter-examples if it were not empty.

However, if we want to solve the universal singleindexed model checking problem "Is it true that if g is a global run of CP then g |= ν ϕ?" we apply instead this procedure:

1. For each component ψ i of ϕ, approximate the existential model checking of ϕ i (as defined in subsection 5.3)) on CP, using the procedure described above. 2. If, for every sub-problem "∃g ∈ Runs ω (CP), g |= ν ϕ i " the procedure returns a negative answer, then the answer to the universal single-indexed model checking of ϕ is positive. 3. However, if this is not the case, we can't draw any immediate conclusion. We may use the abstract counter-example to help us find an actual run of CP that does not verify ϕ. We may also refine the Kleene abstraction by increasing its order if it's a prefix abstraction.

We can apply this abstraction framework to safety -ensuring that an unsafe state is never reached -or liveness -checking that a desirable state can always be eventually reached -properties. By design, our procedure is better at providing a positive answer to these problems, as a definitive negative answer would require us to compute an infinite run as a counter-example, something we are not yet capable of (even as a semidecision procedure). It is unlikely such a semi-decision procedure is even possible, as the actual set we are approximating is an intersection of ω-context free languages.

Model Checking Stutter-invariant LTL Formulas on CPDSs

In the previous section, we focused on single-indexed LTL model checking for CPDSs. The valuation function was applied on a thread per thread basis: only one configuration in the set of configurations of pushdown components was evaluated at a time. It can be argued that such a definition is not natural, as local properties are applied to projections of a global run.

Hence, we should consider the LTL model checking problem on CPDSs where the valuation function takes a global configuration in the set Conf P1 × . . . × Conf Pn as an input. This problem is obviously undecidable, but we show that it can be abstracted for the sub-class of stutter-invariant LTL formulas.

Generic model checking for CPDSs

Given a CPDS CP = (P 1 , . . . , P n ), let ν : Conf CP → 2 AP be a valuation function on global configurations. It is said to be simple if ∀w 1 , . . . , w n , w 1 , . . . , w n ∈ Γ * ∀p 1 ∈ P 1 , . . . , p n ∈ P n , ∀γ 1 , . . . , γ n ∈ Γ, we have

ν( p 1 , γ 1 w 1 , . . . , p n , γ n w n ) = ν( p 1 , γ 1 w 1 , . . . , p n , γ n w n )
Intuitively, a simple valuation on global configurations is equivalent to a function

ν : (P 1 × Γ ) ∪ . . . ∪ (P n × Γ ) → 2 AP
that only depends on the control state and the top stack symbol of each component. To each global run g of CP, we can match a path ν(g) ∈ Paths.

We will now consider the general model checking problem, similar to the simpler PDS case: Definition 10 (LTL semantics) Given a CPDS CP, an infinite global run g of CP, a LTL formula ϕ, and a simple valuation on global configurations ν, g |= ν ϕ if and only if ν(g) |= ϕ. Finding such a global run g is called the existential model checking problem. This problem is obviously undecidable, being more general than the already undecidable reachability problem.

Stutter-invariant LTL formulas

Intuitively, stutter-invariant formulas are such that adding or removing repetitions in a path does not change its evaluation for such formulas. Hence, sequences that differ only in the amount of stuttering can be considered equivalent when checking stutter-invariant properties.

Definition 11 (Stutter-invariance)

A LTL formula ϕ is said to be stutter-invariant if, ∀(π i ) ≥ 0 ∈ Paths and ∀(n i ) i≥0 ∈ (N * ) N , π n0 0 π n1 1 . . . |= ϕ if and only if π |= ϕ
where π n0 0 π n1 1 . . . stands for the infinite sequence where the i-th value of π is repeated n i times. The paths π n0 0 π n1 1 . . . and π are said to be stutter-equivalent.

As proven by Peled et al. in [START_REF] Peled | Stutter-invariant temporal properties are expressible without the next-time operator[END_REF], LTL formulas without the operator next (X) are stutter-invariant and, conversely, any stutter-invariant LTL property is equivalent to an LTL \ (X) formula. The next operator is seldom used in concurrent model checking: hence, abstracting the stutter-invariant LTL model checking problem for CPDSs would be a worthy addition to existing verification techniques.

Note that the set of stutter-invariant formulas is stable by negation. As a consequence, the universal and existential stutter-invariant LTL model checking problems are equivalent:

(∀r, r |= ϕ) ⇔ ¬(∃r, r |= ¬ϕ)

Abstract model checking for stutter-invariant LTL

In this sub-section, we show how our abstraction framework for single-indexed LTL formulas can be applied to stutter-invariant model checking:

Theorem 7 Let CP be a CPDS, ν a simple valuation on global configurations, and ϕ, a stutter-invariant LTL formula. Then there exists a CPDS CP , a simple valuation on configurations of pushdown components ν , and a single-indexed formula ψ such that there exists a global run g of CP verifying g |= ν ϕ if and only if there exists a global run g of CP verifying g |= ν ψ.

As a consequence, if there is no global run g of CP such that g |= ν ψ, then there is no global run of CP such that g |= ν ϕ. Our abstraction framework on CP can provide us with a negative answer to the existential stutter-invariant model checking problem (or, similarly, with a positive answer to the universal problem).

Reduction to the single-indexed case. Intuitively, we will add to the pushdown components of CP a new PDS called the controller, whose purpose will be to store in its control state the current states and stack symbols of the other components so that it can be used as an input for the simple valuation function ν. To do so, we will modify the pushdown components so that after each transition they must send a status update to the controller.

As a consequence, the valuations of the actual global configurations of the CPDS CP and of the top configurations stored in the controller's memory will be similar, although the extra transitions added by the synchronization process between the controller and the other pushdown components will cause some stuttering. A global run of CP can therefore be used to design a new global run in the modified CPDS such that its projection on the controller will be equivalent as far as the verification of stutter-invariant properties is concerned.

Proof (Theorem 7) Without loss of generality, we assume that the control states sets (P i ) i=1...n are disjoint, that each pushdown component P i has a bottom stack symbol ⊥ in Γ that can never be popped and a starting configuration of the form c i 0 = s i 0 , ⊥ .

Modifying the pushdown components. For each pushdown component P i = (P i , {τ } ∪ Lab i , Γ, ∆ i , c i 0 ), we introduce a new PDS P i = (P i , Σ i , Γ, ∆ i , c i 0 ) such that: -Let P j i , j ∈ {1, . . . , n} be disjoint copies of P i . Then

P i = P i ∪ P 1 i ∪ . . . ∪ P n i
To each state p ∈ P , we match a state p j ∈ P j i . -We add new synchronization signals between the controller and the pushdown components:

Σ i = {τ } ∪ Lab i ∪ (P i × Γ × {1, . . . , n}) -∀(p, γ) a -→ (q, w) ∈ ∆ i such that a ∈ Lab i,j , we have (p, γ) a -→ (q j , w) ∈ ∆ i
Unlike ∆ i , instead of moving straight to q, the PDS goes through an intermediate state

q j . -∀(p, γ) τ -→ (q, w) ∈ ∆ i we have (p, γ) τ -→ (q i , w) ∈ ∆ i
The PDS goes through an intermediate state q i instead of moving straight to q.

-∀p ∈ P i and γ ∈ Γ , ∀j ∈ {1, . . . , n}, we have

(p j , γ) (p,γ,j) ----→ (p, γ) ∈ ∆ i
When the PDS is in an intermediate state p j , it moves to an actual state p ∈ P i and sends to the controller C a signal stating its current state, its top stack symbol (there is always one since we can't pop the bottom of the stack), and the index of the pushdown component it previously synchronized with (i stands for internal transitions of P i ) so that the controller can update its configuration.

Designing the controller. We define a new pushdown component C = (C, Σ, Γ, ∆ c ) called the controller such that:

-Let the set of control states be

C = (P 1 × Γ ) × (P 2 × Γ ) × . . . × (P n × Γ ) × Buffer where Buffer = ((P 1 ∪ . . . ∪ P n ) × Γ × {1, ..., n}) ∪ {Empty}
The set of control states stores the state and top stack symbols of the n other components, but also features a buffer that can either store a state and top stack symbol of a pushdown component or wait in an Empty state.

-Let the input alphabet be

Σ = (P 1 ∪ . . . ∪ P n ) × Γ × {1, . . . , n}
The input alphabet can be used to receive the state and top stack symbols of another pushdown component, as well as the index of the pushdown component it last synchronized with (an internal transition is considered as a synchronization of a component P i with itself).

-For each pushdown component P i ,

∀p 1 ∈ P 1 , . . . , ∀p n ∈ P n , ∀q i ∈ P i , ∀γ 1 , . . . , γ n , γ i ∈ Γ
we add to ∆ c the transition

(( p 1 , γ 1 , . . . , p i , γ i , . . . , p n , γ n , Empty), ⊥) (qi,γ i ,i) -----→ (( p 1 , γ 1 , . . . , q i , γ i , . . . , p n , γ n , Empty), ⊥)
If the buffer is empty and the controller receives a signal triggered by an internal transition of a pushdown component, then it can directly update its state according to the information sent.

-For each pushdown component P i , ∀j = i,

∀p 1 ∈ P 1 , . . . , ∀p n ∈ P n , ∀q i ∈ P i , ∀γ 1 , . . . , γ n , γ i ∈ Γ
we add to ∆ c the transition (( p 1 , γ 1 , . . . , p i , γ i , . . . , p n , γ n , Empty), ⊥)

(qi,γ i ,j) -----→ (( p 1 , γ 1 , . . . , p i , γ i , . . . , p n , γ n , q i , γ i , j ), ⊥)
If the buffer is empty and the controller receives a signal triggered by a synchronized transition of a pushdown component, then the data sent is stored in the buffer and the controller waits for the signal of the other component that took part in the synchronized transition.

-For each pushdown component P i , ∀j = i,

∀p 1 ∈ P 1 , . . . , ∀p n ∈ P n , ∀q i ∈ P i , ∀q j ∈ P j , ∀γ 1 , . . . , γ n , γ i , γ j ∈ Γ
we add to ∆ c the transition

(( p 1 , γ 1 , . . . , p i , γ i , . . . , p j , γ j , . . . , p n , γ n , q j , γ j , i ), ⊥) (qi,γ i ,j)
-----→ (( p 1 , γ 1 , . . . , q i , γ i , . . . , q j , γ j , . . . , p n , γ n ,

Empty), ⊥)

If the buffer is full, then the controller updates its states according to the information sent by the expected pushdown component as well as the data stored in the buffer.

We introduce a buffer in order to handle synchronized transitions between two pushdown components: if, in a global run, a synchronized transition is such that a CPDS moves from configuration

( p 1 , γ 1 w 1 , p 2 , γ 2 w 2 ) to ( p 1 , γ 1 w 1 , p 2 , γ 2 w 2 )
then the representation of the pushdown components in the controller should move from

( p 1 , γ 1 , p 2 , γ 2 ) to ( p 1 , γ 1 , p 2 , γ 2 )
without going through the partially updated configuration

( p 1 , γ 1 , p 2 , γ 2 )
that is never reached by the original CPDS. To avoid this issue, the first synchronization signal will be stored in the buffer, then both configurations are updated at the same time, using the buffer and the next synchronization signal.

Example 6 (Handling internal transitions) The run r i

p i , γ i w τ -→ q i i , γ i w (qi,γ i ,i)
-----→ q i , γ i w of the pushdown component P i can synchronize with the run r (. . . , p i , γ i , . . . , Empty)

(qi,γ i ,i)
-----→ (. . . , q i , γ i , . . . , Empty) of the controller.

Example 7 (Handling synchronized transitions) Consider the run r i

p i , γ i w i a -→ q j i , γ i w i (qi,γ i ,j) -----→ q i , γ i w i
and the run r j p j , γ j w j a -→ q i j , γ j w j (qj ,γ j ,i)

-----→ q j , γ j w j of the pushdown components P i and P j that can synchronize with the run r (. . . , p i , γ i , . . . , p j , γ j , . . . , Empty)

(qi,γ i ,j)

-----→ (. . . , p i , γ i , . . . , p j , γ j , . . . , q i , γ i , j )

(qj ,γ j ,i)

-----→ (. . . , q i , γ i , . . . , q j , γ j , . . . , Empty)

of the controller.

The valuation function. We define a new simple valuation function ν for the pushdown component on the set

(P 1 × Γ ) ∪ . . . ∪ (P n × Γ ) ∪ ((P 1 × Γ ) × . . . ×(P n × Γ ) × Buffer ) -ν ((x, y)) = ν(x) if x ∈ (P 1 × Γ ) × (P 2 × Γ ) × . . . × (P n × Γ )
and y ∈ Buffer ; the valuation function on the controller is equivalent to the simple valuation of global configurations of CP, and ignores the value of the buffer.

-ν (x) = True if x ∈ (P 1 × Γ ) ∪ . . . ∪ (P n × Γ )
The valuation function on the n other pushdown components is not relevant and always true.

The CPDS and the single-indexed LTL formula. Let us consider the CPDS with n + 1 components

CP = (C, P 1 , . . . , P n ) on the alphabet Act = Act ∪ (P 1 ∪ . . . ∪ P n ) × Γ × {1, . . . , n}
and the single-indexed formula ψ = (ϕ, True, . . . , True)

Our goal is to simulate (with some repetitions) in the controller component of CP paths matched to global runs of the original CPDS CP, and check the stutterinvariant formula ϕ there.

Computing a new global run. Let us assume that a global run g of CP verifying the stutter-invariant LTL formula ϕ exists. We will define inductively a global run g on CP , starting from the initial configuration (( s 1 0 , ⊥ , . . . , s n 0 , ⊥ , Empty), c 1 0 , . . . , c n 0 )

For each transition of the form

( p 1 , γ 1 w 1 , . . . , p n , γ n w n ) x -→ CP ( q 1 , γ 1 w 1 , . . . , q n , γ n w n )
belonging to g, we will design a sequence of transitions of g such that, given v = ν(( p 1 , γ 1 w 1 , . . . , p n , γ n w n )) and v = ν(( q 1 , γ 1 w 1 , . . . , q n , γ n w n )) the valuation ν on the controller C goes through a sequence of the form v λ v µ . Moreover, g should otherwise be similar to g w.r.t. the other n pushdown components, interactions with the controller component notwithstanding.

1. If x = τ , then the system CP executes in a component P i an internal action p i , γ i w i τ -→ Pi q i , γ i w i and ∀j = i p j , γ j w j = q j , γ j w j

We first use in CP an internal transition

p i , γ i w i τ -→ P i q i i , γ i w i
of the component P i .

It is then followed by a synchronized action between the transition

q i i , γ i w i (qi,γ i ,i)
-----→ P i q i , γ i w i of the system P i and the transition

(( p 1 , γ 1 , . . . , p i , γ i , . . . , p n , γ n , Empty), ⊥) (qi,γ i ,i)
-----→ (( p 1 , γ 1 , . . . , q i , γ i , . . . , p n , γ n , Empty), ⊥)

of the controller C.

Intuitively, the i-th component performs the internal action then synchronizes with the controller to update the stack configurations. CP performed the internal action in one step, CP in two. The latter path stutters once, as the controller's state does not change during the first step. 2. if x = a, a ∈ Lab i,j , then the system CP executes a synchronized action between two components P i and P j , but otherwise, ∀k = j, i,

p k , γ k w k = q k , γ k w k
We first perform in CP' a synchronized action between the transition p i , γ i w i a -→ P i q j i , γ i w i of the component P i and the transition p j , γ j w j a -→ P j q i j , γ j w j of the component P j .

Then we perform a synchronized action between the transition

q j i , γ i w i (qi,γ i ,j)
-----→ P i q i , γ i w i of the system P i and the transition (( p 1 , γ 1 , . . . , p i , γ i , . . . , p n , γ n , Empty), ⊥)

(qi,γ i ,j)

-----→ (( p 1 , γ 1 , . . . , p i , γ i , . . . , p n , γ n , q i , γ i , j ), ⊥)

of the controller C. It is finally followed by a synchronized action between the transition q i j , γ j w j (qj ,γ j ,i)

-----→ P j q j , γ j w j of P j and the transition (( p 1 , γ 1 , . . . , p i , γ i , . . . , p j , γ j , . . . , p n , γ n , q i , γ i , j ), ⊥)

(qj ,γ j ,i)

-----→ (( p 1 , γ 1 , . . . , p i , γ i , . . . , p j , γ j , . . . , p n , γ n , Empty), ⊥)

of the controller C.

We perform a synchronized action between P i and P j , then we update the controller by synchronizing C and P i , storing in the buffer the updated state to avoid a partially updated (hence incorrect) configuration, then we eventually synchronize C and P j while emptying the buffer.

When the valuation path g of CP goes through the values vv , the valuation path g of the controller in CP goes through the values v 2 v in case 1, and through the values v 3 v in case 2. Since ϕ is stutter-invariant and holds for g, then it must hold for the projection of g on the controller C, hence g |= ν ψ.

From CP to CP. Let g be a global run of CP . By design, if we remove any synchronized transition involving the controller from g and replace every transition of the form (p, γ)

x -→ (q j , w) ∈ ∆ i belonging to P i by its equivalent (p, γ)

x -→ (q, w) ∈ ∆ i in P i , we end up with a global run g of CP such that ν(g) and ν (g ) are stutter-equivalent. Hence, ν(g) |= ϕ if and only if ν (g ) |= ψ.

Application to race conditions

A race condition is an issue peculiar to multi-threaded programs that happens when events do not occur in the order the programmer intended, such as concurrent operations on a shared memory location. In this section, we show a toy example of a race condition in a CPDS that can be detected thanks to our abstraction. This example is inspired by the works in [START_REF] Chaki | Verifying concurrent message-passing c programs with recursive calls[END_REF][START_REF] Patin | Spade: Verification of multithreaded dynamic and recursive programs[END_REF][START_REF] Qadeer | Kiss: Keep it simple and sequential[END_REF] on a Windows NT Bluetooth driver.

The CPDS model

We consider a network composed of three processes: one of these handles memory allocation, and the two others processes can synchronize with it in order to use memory to fulfil requests. These processes are the following: MEMORY: handles the amount of free memory available; this amount decreases when another process uses memory; the process will send different signals depending on whether there is free memory left or not; CONSUME: can arbitrarily use the free memory handled by the previous process; REQUEST: has a stack of requests to fulfil, and will use memory to do so.

If MEMORY runs out of free memory and another process try to use some nonetheless, MEMORY will reach an error state.

Each process can be modelled by a PDS as follows:

7.1.1 The process MEMORY.

Let m and m e be its two states. Its stack alphabet is {γ, ⊥}. The number of γ's in the stack corresponds to the amount of memory available to other threads, a single γ being enough to handle a single request. This process will pop a γ from its stack if it receives a signal use. As an internal action, it can also push a γ on its stack (allocating memory) if there is no free memory left. It can send a signal on to other threads if there is at least one γ on the stack, and will send off otherwise.

If it receives a use signal but there is no γ on the stack, it will instead move to the error state m e . The process MEMORY is represented by the following PDS rules: Let c, c check , and c done be its three states and ⊥ its only stack symbol. This process can check if there is any free memory left by exchanging a signal on with MEMORY, then consume one unit by sending a signal use. Let r and r check be its two states. Its stack alphabet is {γ, ⊥}. The number of γ's in the stack corresponds to the number of requests it must handle. As an internal action, it can receive a new request and push a γ symbol on its stack. This process can check if there is any free memory left by exchanging a signal on with MEMORY, then handle a request and consume one unit by sending a signal use, popping a symbol γ from its own stack.

The process REQUEST is represented by the following PDS rules:

Using a single-indexed LTL formula

Let P be the set of all states of the CPDS. We define AP = P and a simple valuation ν such that for each stack symbol x and p ∈ P , ν( p, x ) = {p}. We express a correct behaviour of the CPDS as the conjunction of the three following LTL formulas:

ψ MEMORY = G(¬m e ); the process MEMORY can't reach its error state; ψ CONSUME = GF (c); the process CONSUME will always go back to its waiting state c; ψ REQUEST = G(r check ⇒ F (r)); the process RE-QUEST, when it starts handling a request, must complete it and go back to its default state.

We then apply the prefix abstraction scheme introduced in Section 5.2 to the universal single-indexed model checking problem

(MEMORY , CONSUME , REQUEST ) |= (ψ MEMORY , ψ CONSUME , ψ REQUEST )
Our algorithm finds a counter-example in seven steps. Intuitively, a race condition happens when both CON-SUME and REQUEST try to use memory while MEM-ORY only has a single unit available.

A.1 Abstractions and Galois connections

Let L = (2 Act * , ⊆, ∪, ∩, ∅, Act * ) be the complete lattice of languages on Act.

Our abstraction of L requires a lattice E = (D, ≤, , , ⊥, ), from now on called the abstract lattice, where D is a set called the abstract domain, as well as a pair of mappings (α, β) called a Galois connection, where α : 2 Act * → D and β :

D → 2 Act * are such that ∀x ∈ 2 Act * , ∀y ∈ D, α(x) ≤ y ⇔ x ⊆ β(y)
∀L ∈ L, given a Galois connection (α, β), we have L ⊆ β(α(L)); the Galois connection can be used to over-approximate a language in 2 Act * (e.g. the trace language of a PDS).

Moreover, it is easy to see that

∀L 1 , ∀L 2 ∈ L, α(L 1 ) α(L 2 ) = ⊥ if and only if β(α(L 1 )) ∩ β(α(L 2 )) = ∅ A.

Kleene algebras

We consider a special class of abstractions called Kleene abstractions.

An idempotent semiring is a structure K = (A, ⊕, , 0, 1), where ⊕ is an associative, commutative, and idempotent (a⊕a = a) operation such that A is closed under the infinite sum , and is an associative operation. 0 and 1 are neutral elements for ⊕ and respectively, 0 is an annihilator for (a 0 = 0 a = 0) and distributes over ⊕.

K is an Act-semiring if it can be generated by 0, 1, and elements of the form va ∈ A, ∀a ∈ Act. A semiring is said to be closed if ⊕ can be extended to an operator over countably infinite sets while keeping the same properties as ⊕.

We define a 0 = 1, a n+1 = a a n and a * = n≥0 a n . Adding the * operation to an idempotent closed Act-semiring K transforms it into a Kleene algebra.

A.3 Kleene abstractions

An abstract lattice E = (D, ≤, , , ⊥, ) is said to be compatible with a Kleene algebra K = (A, ⊕, , 0, 1) if D = A, x ≤ y ⇔ x ⊕ y = y, ⊥ = 0 and = ⊕.

A Kleene abstraction is an abstraction such that the abstract lattice E is compatible with the Kleene algebra and the Galois connections α : 2 Act * → D and β : D → 2 Act * are defined by:

α(L) = a1...an∈L va 1 . . . va n β(x) = {a 1 . . . an ∈ Act * | va 1 . . . va n ≤ x}
Intuitively, a Kleene abstraction is such that the abstract operations ⊕, , and * can be matched to the union, the concatenation, and the Kleene closure of the languages of the lattice L, 0 and 1 to the empty language and {ε}, va to the language {a}, the upper bound ∈ K to Act * , and the operation to the intersection of languages in the lattice L.

In order to compute α(L) for a given language L, each word a 1 . . . an in L is matched to its abstraction va 1 . . . va n , and we consider the sum of these abstractions.

A finite-chain abstraction is such that the lattice (A, ≤) has no infinite ascending chains: as a consequence, infinite sequences of concatenations i≥0 va i can be defined and effectively computed, and the abstraction framework can be applied to infinite traces in Act ω . The prefix and first occurrence ordering abstractions defined previously are finite-chain.

A.4 The set of K-predecessors

Let P = (P, Act, Γ, ∆, c 0 ) be a PDS and K = (A, ⊕, , 0, 1) a Kleene algebra corresponding to a Kleene abstraction of the set Act.

We define inductively the set Π K of path expressions as the smallest subset of K such that:

-1 ∈ Π K ; -if π ∈ Π K , then ∀a ∈ Act, va π ∈ Π K .
For a given path expression π, we define its length |π| as the number of occurrences of simple elements of the form va in π.

A K-configuration of P is a pair (c, π) in Conf K P = P × Γ * × Π K . We can extend the transition relation -→ P to Kconfigurations with the following semantics: ∀a ∈ Act, if c a -→ P c , then ∀π ∈ Π K , (c, va π) -→ P,K (c , π) (c, va π) is said to be an immediate K-predecessor of (c , π).

The reachability relation P,K is the reflexive transitive closure of -→ P,K .

Given a set of configurations C, we introduce the set of Kconfigurations pre * K (P, C):

B Abstracting Traces of Pushdown Systems

We now present the automata-theoretic approach used by Bouajjani et al. in [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF] to compute the set pre * K (P, C) in order to abstract runs of PDSs.

B.1 Representing regular sets of configurations

In order to represent regular sets of configurations, we consider the following structure: Definition 12 (Bouajjani et al. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF]) Let P = (P, Σ, Γ, ∆, c 0 ) be a pushdown system. A P-automaton A = (Q, Γ, δ, I, F ) is a finite-state automaton on the stack alphabet Γ of P where Q is a set of states such that P ⊆ Q, I = P the set of initial states, F ⊆ Q the set of final states, and δ ⊆ Q × Γ ∪ {ε} × Q a set of transitions.

Intuitively, a P-automaton is a finite-state automaton whose edges are labelled by stack symbols of P and whose initial states represent the states of P.

Let → A be the transition relation inferred from δ. We say that A accepts a configuration p, w if there is a path p w -→ * A f such that f ∈ F . Let L(A) ⊆ Conf P be the set of configurations accepted by A. Obviously, the following lemma holds: Lemma 3 (Bouajjani et al. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF]) A set of configurations C of a PDS P is regular if and only if there exists a P-automaton A such that L(A) = C.

Let C be a regular set of configurations of a PDS P = (P, Σ, Γ, ∆), and let A be a P-automaton accepting C. It has been proven by Didier Caucal in [START_REF] De Alfaro | On the regular structure of prefix rewriting[END_REF] that the sets pre * (P, C) is regular.

Moreover, it can be computed by applying a saturation procedure (where new transitions are incrementally added until a fixed point is reached) to a P-automaton representing C: Theorem 8 (Bouajjani et al. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF]) Given a PDS P and a regular set of configurations C, there exists a P-automaton A pre * accepting pre * (C).

B.2 K-automata

P-automata are used to represent regular sets of configurations. They can be extended to K-automata in order to handle sets of K-configurations of a PDS P. Intuitively, a K-automaton can be seen as a P-automaton whose transitions labelled by stack symbols in Γ have been given an additional label in K. In a similar manner, P-automaton can be seen as K-automaton whose transitions are all labelled by 1.

We define -→ A ⊆ Q×Γ * ×K ×Q× as the smallest transition relation satisfying:

q (ε,1) ---→ A q for every q ∈ Q; if (q, γ, e, q ) ∈ δ, then q (γ,e) ---→ A q ; if q (w,e) ----→ A q and q (w ,e ) -----→ A q as well, then q (ww ,e e ) --------→ A q .

We say that the K-automaton A accepts a K-configuration (< p, w >, π) if p (w,e) ----→ A q for q ∈ F and some e ∈ K such that π ≤ e.

Let L K (A) be the set of all configurations accepted by A, and T K (A) = {π | ∃c ∈ C, (c, π) ∈ L K (A)} the set of abstract traces matched to these configurations.

By adding extra labels in K to the P-automaton A pre * accepting pre * (C) yielded by Theorem 1, we can compute a K- automaton accepting set pre * K (P, C) using an iterative fixpoint algorithm:

Theorem 9 (Bouajjani et al [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF]) Let P = (P, Σ, Γ, ∆) be a PDS, A a P-automaton accepting a regular set of configurations C, and K a Kleene algebra matched to a finite-chain Kleene abstraction α. Then we can compute a K-automaton A pre * K matched to P accepting the set pre * K (P, C).

Assuming the size of C is constant, the running time of this algorithm is in O(l • |∆| 3 ) operations.

B.3 Approximating the set of traces

Let P be a PDS and C, C two regular sets of configurations of P. Let K be a Kleene algebra matched to a finite-chain Kleene abstraction α. Using Theorem 9, we can compute a K-automaton A pre * K matched to P accepting the set pre * K (P, C).

We can then construct a K-automaton A pre * K over Γ × K equal to the restriction of A pre * K to configurations in C . To do so, we consider the product between A pre * Obviously, the semantics of a PDS and a BPDA being similar, we can apply this framework to compute finite traces of BPDA as well.

Fig. 2 : 3 .

 23 Fig. 2: Abstracting the infinite set of traces matched to the repeating head p, γ

(r 1

 1 ) (m, γ) on --→ (m, γ); the process signals that there is still free memory left; (r 2 ) (m, ⊥) off --→ (m, ⊥); the process signals that there is no free memory left; (r 3 ) (m, ⊥) τ -→ (m, γ⊥); the process allocates memory; (r 4 ) (m, γ) use --→ (m, ε); the amount of free memory available decreases; (r 5 ) (m, ⊥) use --→ (m e , ⊥); the process reaches its error state. 7.1.2 The process CONSUME.

  CONSUME is represented by the following PDS rules: (r 6 ) (c, ⊥) on -→ (c check , ⊥); the process checks if there is any memory left; (r 7 ) (c check , ⊥) use --→ (c done , ⊥); the process uses one unit of memory; (r 8 ) (c done , ⊥) τ -→ (c, ⊥); the process goes back to its initial waiting state.

7. 1 . 3

 13 The process REQUEST.

(

  r 9a ) (r, γ) τ -→ (r, γγ); the process adds a new request; (r 9b ) (r, ⊥) τ -→ (r, γ⊥); the process adds a new request; (r 10 ) (r, γ) on --→ (r check , γ); the process checks if there is any free memory left; (r 11 ) (r check , γ) use --→ (r, ε); the process handles a request while using one unit of memory.

  pre * K (P, C) = {(c, π) | c ∈ pre * (P, C), π ≤ α(L P ({c}, C)) If (c, π) ∈ pre * K (P, C), then, by definition of the Kleene abstraction, (c, π) P,K (c , 1) for some c ∈ C. Intuitively, the abstract path expression π is meant to be the abstraction of an actual trace from c to C.

Definition 13 (

 13 K-automata) A K-automaton matched to aPDS P = (P, Σ, Γ, ∆) is a tuple A = (Q, Γ, δ, I, F ) where Q is a finite set of control states, δ ⊆ Q × Γ × K × Q a finiteset of transition rules, I = P the set of initial states, and F ⊆ Q the set of final states.

K

  and a P-automaton accepting the regular set of configurations C .Finally, α(L P (C , C)) = T K (A pre * K) is an abstraction of the set L P (C , C) of traces of the PDS P leading from the regular set of configuration C to another regular set of configurations C.

An erroneous trace

We write (r i ) ↔ (r j ) if we apply two rules that synchronize. We start from the initial configuration:

Conclusion and Future Works

In this paper, we study the model checking problem of single-indexed and stutter-invariant LTL properties for CPDSs, which is unfortunately undecidable. We design an algorithm to abstract the model checking problem that relies on the automata-theoretic approach of [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF][START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF] and the Kleene abstraction framework of [START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF]. We then apply this technique to a toy example and find a race condition.

An automata-theoretic approach to the CTL model checking problem for PDSs has been introduced in [START_REF] Song | Efficient CTL model-checking for pushdown systems[END_REF]. It remains to be seen if the CTL model checking problem for CPDSs can be abstracted in a similar manner to LTL.