Adrien Pommellet

Tayssir Touili

Model-Checking HyperLTL for Pushdown Systems

Temporal logics such as LTL are often used to express safety or correctness properties of programs. However, they cannot model complex formulas known as hyperproperties introducing relations between different execution paths of a same system. In order to do so, the logic HyperLTL adds existential and universal quantifications of path variables to LTL. The model-checking problem, that is, determining if a given representation of a program verifies a HyperLTL property, has been shown to be decidable for finite state systems. In this paper, we prove that this result does not hold for Pushdown Systems nor for the subclass of Visibly Pushdown Systems. We therefore introduce an algorithm that over-approximates the model-checking problem with an automatatheoretic approach. We also detail an under-approximation method based on a phase-bounded analysis of Multi-Stack Pushdown Systems. We then show how these approximations can be used to check security policies.

Introduction

The analysis of execution traces of programs can be used to prove correctness properties often expressed with the unifying framework of the linear temporal logic LTL. However, a LTL formula only quantifies a single execution trace of a system; LTL can't express properties on multiple, simultaneous executions of a program.

These properties on sets of execution traces are known as hyperproperties. Many safety and security policies can be expressed as hyperproperties; this is in particular true of information-flow analysis. As an example, the non-interference policy states that if two computations share the same public inputs, they should have identical public outputs as well, even if their private inputs differ. This property implies a relation between computations that can't be expressed as a simple LTL formula.

HyperLTL is an extension of LTL introduced by Clarkson et al. in [START_REF] Michael | Temporal logics for hyperproperties[END_REF] that allows the universal and existential quantifications of multiple path variables that range over traces of a system in order to define hyperproperties. As an example, the formula ∀π 1 , ∀π 2 , (a π1 ∧ a π2 ) ⇒ X ((b π1 ∧ b π2 ) ∨ (c π1 ∧ c π2 )) means that, given two path variables π 1 and π 2 in the set T races ω (S) of infinite traces of a system S, if π 1 and π 2 verify the same atomic property a at a given step, then they should both verify either b or c at the next step.

Clarkson et al. have shown that the model-checking problem S |= ψ of HyperLTL, that is, knowing if the set of traces of a system S verifies the HyperLTL formula ψ, can be solved when S is a finite state transition system (i.e. equivalent to a finite state automaton). However, simple transition models cannot accurately model programs with infinite recursion and procedure calls. Pushdown Systems (PDSs) that can simulate the call stack of a program are commonly used instead. The call stack stores information about the active procedures of a program such as return addresses, passed parameters and local variables.

Unfortunately, we show in this paper that the model-checking problem of HyperLTL for PDSs is undecidable: the set of traces of a PDS is a context-free language, and deciding whether the intersection of two context-free languages is empty or not remains an undecidable problem that can be reduced to the model-checking problem by using a HyperLTL formula that synchronizes traces.

On the other hand, determining the emptiness of the intersection of two visibly context-free languages is decidable. This class of languages is generated by Visibly Pushdown Automata (VPDA), an input-driven subclass of pushdown automata (PDA) first introduced by Alur et al. in [START_REF] Alur | Visibly pushdown languages[END_REF]: at each step of a computation, the next stack operation will be determined by the input letter in Σ read, depending on a partition of the input alphabet. We study the model-checking problem of HyperLTL for Visibly Pushdown Systems (VPDSs), and prove that it is also undecidable, as it happens to be a reduction of the emptiness problem for Two-Stack Visibly Pushdown Automata (2-VPDA), which has been shown to be undecidable by Carotenuto et al. in [START_REF] Carotenuto | 2-visibly pushdown automata[END_REF].

To overcome these undecidability issues, since the emptiness of the intersection of a context-free langage with regular sets is decidable, one idea is to consider the case where only one path variable of the formula ranges over the set of traces T races ω (P) of a PDS or VPDS P, while the other variables range over a regular abstraction α(T races ω (P)). Using an automata-theoretic approach, this idea allows us to over-approximate the model-checking problem of HyperLTL formulas that only use universal quantifiers ∀ with the exception of at most one path variable: if the HyperLTL formula holds for the over-approximation, it holds for the actual system as well.

On the other hand, under-approximations can be used to discover errors in programs: if a HyperLTL formula does not hold for an under-approximation of the model-checking problem, it does not hold for the actual system as well. We show that the model-checking problem for PDSs of HyperLTL formulas that only use universal quantifiers ∀ can be under-approximated by relying on a bounded-phase model-checking of a LTL formula for a Multi-Stack Pushdown System (MPDS), where a phase is a part of a run during which there is at most one stack that is popped from, as defined by Torre et al. in [START_REF] La | A robust class of context-sensitive languages[END_REF].

Related work.

Clarkson and Schneider introduced hyperproperties in [6] to formalize security properties, using second-order logic. Unfortunately, this logic isn't verifiable in the general case.

However, fragments of it can be verified: in [START_REF] Michael | Temporal logics for hyperproperties[END_REF], Clarkson et al. formalized the temporal logics HyperLTL and HyperCTL*, extending the widespread and flexible framework of linear time and branching time logics to hyperproperties. The model-checking problem of these logics for finite state systems has been shown to be decidable by a reduction to the satisfiability problem for the quantified propositional temporal logic QPTL defined in [START_REF] Sistla | The complementation problem for büchi automata with applications to temporal logic[END_REF].

Proper model-checking algorithms were then introduced by Finkbeiner et al. in [START_REF] Finkbeiner | Algorithms for modelchecking hyperltl and hyperctl[END_REF]. These algorithms follow the automata-theoretic framework defined by Vardi et al. in [START_REF] Vardi | An automata-theoretic approach to linear temporal logic[END_REF], and can be used to verify security policies in circuits. However, while circuits can be modelled as finite state systems, actual programs can feature recursive procedure calls and infinite recursion. Hence, a more expressive model such as PDSs is needed.

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], the forward and backward reachability sets of PDSs have been shown to be regular and effectively computable. As a consequence, the model-checking problem of LTL for PDSs is decidable; an answer can be effectively computed using an automata-theoretic approach. We try to extend this result to HyperLTL.

Multi-Stack Pushdown Systems (MPDSs) are unfortunately Turing powerful. Following the work of Qadeer et al. in [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF], La Torre et al. introduced in [START_REF] La | A robust class of context-sensitive languages[END_REF] MPDSs with bounded phases: a run is split into a finite number of phases during which there is at most one stack that is popped from. Anil Seth later proved in [START_REF] Seth | Global reachability in bounded phase multi-stack pushdown systems[END_REF] that the backward reachability set of a multi-stack pushdown system with bounded phases is regular; this result can then be used to solve the model-checking problem of LTL for MPDSs with bounded phases. We rely on a phase-bounded analysis of a MPDS to under-approximate an answer to the model-checking problem of HyperLTL for PDSs.

Paper outline. In Section 2 of this paper, we provide background on Pushdown Systems (PDSs) and Visibly Pushdown Systems (VPDSs). We define in Section 3 the hyper linear time logic HyperLTL, and prove that its model-checking problem for PDSs and VPDSs is undecidable. Then, in Section 4, we solve the model-checking problem of HyperLTL on constrained sets of traces then find an over-approximation of the model-checking problem for PDSs. In Section 5, we use Multi-Stack Pushdown Systems (MPDSs) and bounded phase analysis to under-approximate the model-checking problem. Finally, in section 6, we apply the logic HyperLTL to express security properties. Due to a lack of space, detailed proofs of some theorems can be found in the appendix.

Pushdown Systems

The Model

Pushdown systems are a natural model for sequential programs with recursive procedure calls [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF].

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 × Γ * an initial configuration.

If d = (p, γ, a, p , w) ∈ ∆, we write d = (p, γ) a -→ (p , w). We call a the label of Σ. We can assume without loss of generality that ∆ ⊆ P × Γ × Σ × P × Γ ≤2 and that c 0 is of the form p 0 , ⊥ , where ⊥ ∈ Γ is a special bottom stack symbol shared by every PDS on the stack alphabet Γ and p 0 ∈ P . A configuration of P is a pair p, w where p ∈ P is a control state and w ∈ Γ * a stack content.

For each a ∈ Σ, we define a transition relation a -→ P on configurations as follows: if (p, γ) a -→ (p , w) ∈ ∆, for each w ∈ Γ * , p, γw a -→ P p , ww . We then consider the immediate successor relation → P = ∪ a∈Σ a -→ P . We may omit the variable P when only a single PDS is being considered.

A run r is a sequence of configurations r = (c i ) i≥0 such that ∀i ≥ 0, c i ai -→ P c i+1 , c 0 being the initial configuration of P. The word (a i ) i≥0 is then said to be the trace of r. Traces and runs may be finite or infinite. Let T races ω (P) (resp. T races(P)) be the set of all infinite (resp. finite) traces of P.

A Büchi Pushdown Automaton (BPDA) is a pair BP = (P, F ), where P = (P, Σ, Γ, ∆, c 0 ) is a PDS and F ⊆ P a set of final states. An infinite run r = (c i ) i≥0 of BP and its matching trace (a i ) i≥0 are said to be accepting if there exists at least one infinitely often occurring state f in r such that f ∈ F . The language L ω (BP) accepted by BP is the set of all accepting traces of BP, and is said to be ω context-free.

Visibly Pushdown Systems

We consider a particular subclass of PDSs introduced by Alur et al. in [START_REF] Alur | Visibly pushdown languages[END_REF]. Let Σ c , Σ r , Σ l be a partition of the input alphabet, where Σ c , Σ r , and Σ l stand respectively for the call, return, and local alphabets.

Definition 2 (Visibly Pushdown System). A Visibly Pushdown System (VPDS) over a partition Σ c , Σ r , Σ l of Σ is a PDS P = (P, Σ, Γ, ∆, c 0 ) verifying the following properties:

-if (p, γ 1 ) a -→ (p , γ 2 ) ∈ ∆, then a ∈ Σ l , γ 1 = γ 2 , and ∀γ ∈ Γ , (p, γ) a -→ (p , γ) ∈ ∆; -if (p, γ) a -→ (p , ε) ∈ ∆, then a ∈ Σ r ; -if (p, γ 1 ) a -→ (p , γ 2 γ 1 ) ∈ ∆, then a ∈ Σ c , and ∀γ ∈ Γ , (p, γ) a -→ (p , γ 2 γ) ∈ ∆;
VPDSs are an input driven subclass of PDSs: at each step of a computation, the next stack operation will be determined by the input letter in Σ read, depending on which subset of the partition Σ c , Σ r , Σ l the aforementioned letter belongs to.

Visibly Pushdown Automata accept the class of visibly pushdown languages. If a BPDA BP is visibly pushdown according to a partition of Σ, we say it's a Büchi Visibly Pushdown Automata (BVPDA). The class of languages accepted by BVPDA is called ω visibly pushdown languages.

Unlike context-free languages, the emptiness of the intersection of visibly pushdown languages is a decidable problem and the complement of a visibly pushdown language is a visibly pushdown language that can be computed. The same properties also hold for ω visibly pushdown languages.

HyperLTL

The Logic

Let AP be a finite set of atomic propositions used to express facts about a program; a path is an infinite word in (2 AP ) ω = T . Let V be a finite set of path variables. The HyperLTL logic relates multiple paths by introducing path quantifiers.

Definition 3 (Syntax of HyperLTL). Unquantified HyperLTL formulas are defined according to the following syntax equation:

ϕ ::= ⊥ | (a, π) ∈ AP × V | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | X ϕ | ϕ U ϕ | G ϕ | F ϕ
From then on, we write a π = (a, π). HyperLTL formulas are defined according to the following syntax equation:

ψ ::= ∃π, ϕ | ∀π, ϕ | ϕ where π ∈ V is a path variable.
The existential ∃ and universal quantifiers ∀ are used to define path variables, to which atomic propositions in AP are bound. A HyperLTL formula is said to be closed if there is no free variable: each path variable is bound by a path quantifier once.

As an example, the closed formula ∀π 1 , ∃π 2 , ϕ means that for all paths π 1 , there exists a path π 2 such that the formula ϕ holds for π 1 and π 2 . Simple LTL formulas can be considered as a subclass of closed HyperLTL formulas of the form ∀π, ϕ with a single path variable.

Let Π : V → T be a path assignment function of V that matches to each path variable π a path Π(π) ∈ T . If Π(π) = (t j ) j≥0 , for all i ≥ 0, we define the i-th value of the path Π(π)[i] = t i and a suffix assignment function

Π[i, ∞] such that Π[i, ∞](π) = (t j ) j≥i .
We first define the semantics of this logic for path assignment functions.

Definition 4 (Semantics of unquantified HyperLTL formulas). Let ϕ be an unquantified HyperLTL formula. We define by induction on ϕ the following semantics on path assignment functions:

Π |= a π ⇔ a ∈ Π(π)[0] Π |= ¬ϕ ⇔ Π |= ¬ϕ Π |= ϕ 1 ∨ ϕ 2 ⇔ (Π |= ϕ 1 ) ∨ (Π |= ϕ 2 ) Π |= ϕ 1 ∧ ϕ 2 ⇔ (Π |= ϕ 1 ) ∧ (Π |= ϕ 2 ) Π |= X ϕ ⇔ Π[1, ∞] |= ϕ Π |= ϕ U ψ ⇔ ∃j ≥ 0, Π[j, ∞] |= ψ and ∀i ∈ {0, . . . , j -1} , Π[i, ∞] |= ϕ Π |= G ϕ ⇔ ∀i ≥ 0, Π, i |= ϕ Π |= F ϕ ⇔ ∃i ≥ 0, Π, i |= ϕ
Π |= ϕ if ϕ holds for a given assignment of path variables defined according to Π.

Let T : V → 2 T be a set assignment function of V that matches to each path variable π ∈ V a set of paths T (π) ⊆ T . We can now define the semantics of closed HyperLTL formulas for set assignment functions.

Definition 5 (Semantics of closed HyperLTL formulas). We consider a closed HyperLTL formula ψ = χ 0 π 0 , . . . , χ n π n , ϕ, where each χ i ∈ {∀, ∃} is an universal or existential quantifier, and ϕ an unquantified HyperLTL formula using trace variables π 0 , . . . , π n .

For a given set assignment function T , we write that

T |= ψ if for χ 0 t 0 ∈ T (π 0 ), . . ., χ n t n ∈ T (π n ), we have Π |= ϕ, where Π is the path assignment function such that ∀i ∈ {0, . . . , n}, Π(π i ) = t i . As an example, if ψ = ∀π 1 , ∃π 2 , ϕ is a closed HyperLTL formula and T is a set assignment function of V, then T |= ψ if ∀t 1 ∈ T (π 1 ), ∃t 2 ∈ T (π 2 ) such that Π |= ϕ, where Π(π 1 ) = t 2 and Π(π 2 ) = t 2 .
Intuitively, T |= ψ if, assuming path variables belong to path sets defined according to T , the closed formula ψ holds. From then on, we assume that every HyperLTL formula considered in this paper is closed.

HyperLTL and PDSs

Let P be a PDS on the input alphabet Σ = 2 AP and ψ a closed HyperLTL formula. We write that P |= ψ if and only if T |= ψ where the set assignment function T is such that ∀π ∈ V, T (π) = T races ω (P). Determining whether P |= ψ for a given PDS P and a given HyperLTL formula ψ is called the model-checking problem of HyperLTL on PDSs. The following theorem holds :

Theorem 1. The model-checking problem of HyperLTL for PDSs is undecidable.

We can prove this result by reducing the emptiness of the intersection of two context-free languages, a well-known undecidable problem, to the model-checking problem. Our intuition is to consider two context-free languages L 1 and L 2 on the alphabet Σ. As HyperLTL formulas apply to infinite words, we define two BPDA BP 1 and BP 2 that accept L 1 f ω and L 2 f ω respectively, where f / ∈ Σ is a special ending symbol. We then define a PDS P that can simulate either BP 1 or BP 2 .

We now introduce the formula ψ = ∃π 1 , ∃π 2 , ϕ start ∧ ϕ sync ∧ ϕ end : ϕ start expresses that trace variables π 1 and π 2 represent runs of BP 1 and BP 2 respectively, ϕ sync means that the two traces are equal from their second letter onwards, and ϕ end implies that the two traces are accepting. Hence, if P |= ψ, then BP 1 and BP 2 share a common accepting run, and

L 1 ∩ L 2 = ∅.
On the other hand, if L 1 ∩ L 2 = ∅, there is an accepting trace π common to BP 1 and BP 2 and we can define two traces π 1 and π 2 of P such that the formula ϕ start ∧ ϕ sync ∧ ϕ end holds. Since the emptiness problem is undecidable, so must be the model-checking problem.

The full proof is given in the appendix. As a consequence of Theorem 1, determining whether T |= ψ for a generic set assignment function T and a given HyperLTL formula ψ is an undecidable problem.

HyperLTL and VPDSs

Since the emptiness of the intersection of visibly pushdown languages is decidable, the previous proof does not apply to VPDSs and one might wonder if the model-checking problem of HyperLTL for this particular subclass is decidable. Unfortunately, we can show that this is not the case:

Theorem 2. The model-checking problem of HyperLTL for VPDSs is undecidable.

In order to prove this theorem, we will rely on a class of two-stack automata called 2-Visibly Pushdown Automata (2-VPDA) introduced in [START_REF] Carotenuto | 2-visibly pushdown automata[END_REF]. In a 2-VPDA, each stack is input driven, but follows its own partition of Σ. The same input letter may result in different pushdown rules being applied to the first and second stack: as an example, a transition can push a word on the first stack and pop the top letter of the second stack, depending on which partition is used by each stack. Moreover, in a manner similar to VPDA, transitions of 2-VPDA do not depend on the top stack symbols unless they pop them.

It has been shown in [START_REF] Carotenuto | 2-visibly pushdown automata[END_REF] that the emptiness problem is undecidable for 2-VPDA. Our intuition is therefore to prove Theorem 2 by reducing the emptiness problem for 2-VPDA to the model-checking problem of HyperLTL for VPDSs. To do so, for a given 2-VPDA D, we define a VPDS P and a HyperLTL formula ψ on two trace variables such that P |= ψ if and only if D has an accepting run.

P is such that it can simulate either stack of the 2-VPDA. However, both stacks must be synchronized in order to properly represent the whole automaton: the content of one stack can lead to a control state switch that may enable a transition modifying the other stack. The HyperLTL formula ψ determines which trace variable is related to which stack, synchronizes two runs of P in such a manner that they can be used to define an execution path of D, and ensure that this path is an accepting one. The full proof can be found in the appendix.

Model-checking HyperLTL with Constraints

Theorem 1 proves that the model-checking problem of HyperLTL for PDSs is undecidable. Intuitively, this issue stems from the undecidability of the intersection of context-free languages. However, since the emptiness problem of the intersection of a context-free language with regular sets is decidable, one can think of a way to abstract the set of runs of a PDS for some -but not all -path variables of a HyperLTL formula as a mean of regaining decidability.

As shown in [START_REF] Bermudez | Practical arbitrary lookahead lr parsing[END_REF][START_REF] Fernando | Finite-state approximation of phrase structure grammars[END_REF], runs of a PDS can be over-approximated in a regular fashion. Hence, for a given PDS P, if we consider a regular abstraction of the set of runs α(T races ω (P)), we can change the set assignment function for a path variable π in such a manner that T (π) = α(T races ω (P)) instead of T (π) = T races ω (P).

For a set assignment function T on a set of path variables V and a variable π ∈ V, we say that π is context-free w.r.t. to T if T (π) = T races ω (P) for a PDS P. We define regular and visibly pushdown variables in a similar manner.

Let ψ = χ 0 π 0 , . . . , χ n π n , ϕ be a closed HyperLTL formula on the alphabet AP with n + 1 trace variables π 0 , . . . , π n , where χ 0 . . . , χ n ∈ {∀, ∃}. In this section, we will present a procedure to determine whether T |= ψ in two cases.

1. If the variable π 0 is context-free w.r.t. T , and all the other variables are regular, then we can determine whether T |= ψ or not. We can then apply this technique in order to over-approximate the model-checking problem if T (π 0 ) = T races ω (P), T (π j ) = α(T races ω (P)) for j = 1 . . . n, and χ 1 , . . . , χ n = ∀.

The last n variables can only be universally quantified.

T |= ψ then implies that P |= ψ: indeed, the universal quantifiers on the path variables that range over the abstracted traces are such that, if the formula ϕ holds for every run in the over-approximation, then it also holds for every run in the actual set of traces. This is an over-approximation of the actual model-checking problem.

2. If there exists a variable π i such that π i is visibly context-free w.r.t. T , and all the other variables are regular, then we can determine whether T |= ψ or not. A single path variable at most can be visibly context-free (not necessarily π 0 , though), and all the others must be regular. We can then apply this technique in order to over-approximate the model-checking problem if P is a VPDS, T (π i ) = T races ω (P), T (π j ) = α(T races ω (P)) and χ j = ∀ for j = i. Each path variable with the exception of the visibly context-free one must be universally quantified.

Because of the universal quantifiers on the regular path variables, T |= ψ implies again that P |= ψ. This is another over-approximation of the modelchecking problem.

Moreover, these over-approximations are accurate for at least one variable in the trace variable set, as the original, ω context-free (or ω visibly pushdown) set of runs is assigned to this variable instead of an ω regular over-approximation.

With One Context-Free Variable and n Regular Variables

Let P be a PDS such that T (π 0 ) = T races ω (P), and K 1 , . . . , K n , finite state transition systems (i.e. finite automata without final states) such that for i = 1, . . . , n, T (π i ) = T races ω (K i ).

Theorem 3. If π 0 is context-free w.r.t. T and the other variables are regular, we can decide whether T |= χ 0 π 0 , . . . , χ n π n , ϕ or not.

To do so, we use the following well-known result: Lemma 1. Let ϕ be an LTL formula. There exists a Büchi automaton B ϕ on the alphabet 2 AP such that L(B ϕ ) = {w ∈ (2 AP ) ω | w |= ϕ}. We say that B ϕ accepts ϕ.

An unquantified HyperLTL formula with m trace variables π 1 , . . . , π m can be considered as a LTL formula on the alphabet (2 AP ) m : given a word w on (2 AP ) m and a ∈ AP , we say that w |= a πi if a ∈ w i (0), where w i is the i-th component of w. We then apply Lemma 1 and introduce a Büchi automaton B ϕ on the alphabet (2 AP ) n+1 accepting ϕ. We denote Σ = 2 AP .

We then compute inductively a sequence of Büchi automata B n+1 , . . . , B 1 such that:

-B n+1 is equal to the Büchi automaton B ϕ on the alphabet Σ n+1 ; if the quantifier χ i is equal to ∃ and B i+1 = (Q, Σ i+1 , δ, q 0 , F ) is a Büchi automaton on the alphabet Σ i+1 , let K i = (S, Σ, δ , s 0 ) be the finite state transition system generating T (π i ); we now define the Büchi automaton B i = (Q× S, Σ i , ρ, (q 0 , s 0 ), F ×S) where the set ρ of transitions is such that if q (a0,...,ai)

------→ q ∈ δ and s ai -→ s ∈ δ , then (q, s) (a0,...,ai-1)

--------→ (q , s ) ∈ ρ. Intuitively, the Büchi automaton B i represents the formula ∃π i , χ i+1 π i+1 , . . . , χ n π n , ϕ; its input alphabet Σ i depends on the number of variables that are not quantified yet; if the quantifier χ i is equal to ∀, we consider instead the complement B i+1 of B i+1 and compute its product with K i in a similar manner to the previous construction; B i is then equal to the complement of this product; intuitively, ∀π, ψ = ¬(∃π, ¬ψ).

Having computed B 1 = (Q, Σ, δ, q 0 , F ), let P = (P, Σ, Γ, ∆, p 0 , ⊥ ) be the PDS generating T (π 0 ). We assume that χ 0 = ∃. Let BP = (P × Q, Σ, ∆ , (p 0 , q 0 ), ⊥ , P ×F ) be a Büchi pushdown automaton, where the set of transitions ∆ is such that if q a -→ q ∈ δ and (p, γ) a -→ (p , w) ∈ ∆, then ((p, q), γ) a -→ ((p , q ), w) ∈ ∆ . BP represents the fully quantified formula ∃π 0 , χ 1 π 1 , . . . , χ n π n , ϕ. Obviously, B is not empty if and only if T |= ψ.

If χ 0 = ∀, we consider instead the complement B 1 of B 1 , then define a Büchi pushdown automaton BP in a similar manner. B is empty if and only if T |= ψ.

It has been proven 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] that the emptiness problem is decidable for Büchi pushdown automata. Hence, given our initial constraints on T and ψ, we can determine whether T |= ψ or not.

The Büchi automaton B ϕ has O(2 |ϕ| ) states; if we assume that all variables are existentially quantified, the BPDS

BP has ν = O(2 |ϕ| |P||K 1 | . . . |K n |) states.
According to [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF], checking the emptiness of BP can be done in O(ν 2 k) operations, where k is the number of transitions of BP, hence, in

O(ν 4 |Γ | 2 ).
Complementation of a Büchi Automaton may increase its size exponentially, hence, this technique may incur an exponential blow-up depending on the number of universal quantifiers. Application. If we consider that π 0 range over T races ω (P) and that π 1 , . . . , π n range over a regular abstraction α(T races ω (P)) of the actual set of traces, and we assume that χ 1 , . . . , χ n = ∀, we can apply this result to over-approximate the model-checking problem, as detailed earlier in this section.

It is worth noting that the complement of an ω context-free language is not necessarily an ω context-free language. Hence, we can't use the previous procedure to check a HyperLTL formula of the form ψ = ∃π, ∀π ϕ where π is a context-free variable and π is regular. We know, however, that ω visibly pushdown languages are closed under complementation. We therefore consider the case of a single visibly pushdown variable in the following subsection.

With One Visibly Pushdown Variable and n Regular Variables

Let P be a VPDS such that T (π i ) = T races ω (P), and (K j ) j =i finite state transition systems such that for j = i, T (π j ) = T races ω (K j ). Unlike the previous case, the visibly context-free variable no longer has to be the first one π 0 .

Theorem 4. If a variable π i is visibly pushdown w.r.t. T and the other variables are regular, we can decide whether T |= χ 0 π 0 , . . . , χ n π n , ϕ or not.

The proof of this theorem is similar to the proof of Theorem 3. We first build a sequence of Büchi automata B n+1 , . . . , B i+1 in a similar manner to the proof of Theorem 3, starting from a finite state automaton B n+1 = B ϕ on the alphabet Σ n+1 representing the unquantified formula ϕ then computing products with the transition systems K n+1 , . . . , K i+1 until we end up with a Büchi automaton B i+1 on the alphabet Σ i+1 .

Having computed B i+1 = (Q, Σ i+1 , δ, q 0 , F ), let P = (P, Σ, Γ, ∆, p 0 , ⊥ ) be the VPDS generating T (π i ). We assume that χ i = ∃. Let BP i = (P × Q, Σ i+1 , ∆ , (p 0 , q 0 ), ⊥ , P × F ) be a visibly Büchi pushdown automaton, where ∆ is such that if q (a0,...,ai-1,a)

---------→ q ∈ δ and (p, γ) a -→ (p , w) ∈ ∆, then ((p, q), γ) (a0,...,ai-1,a)

---------→ ((p , q ), w) ∈ ∆ . BP i is indeed a BVPDA on the alphabet Σ i+1 as its stack operations only depend on its i + 1-th variable. If χ i = ∀, we consider instead the complement B i+1 .

From the i-th variable onwards, we compute a sequence of visibly Büchi pushdown automata BP i , . . . , BP 0 on the alphabets Σ i+1 , . . . , Σ i respectively. For i ≥ k ≥ 1, if BP k = (P , Σ k+1 , ∆ , p 0 , ⊥ , F ), K i = (S, Σ, δ, s 0 ), and χ k = ∃, let BP k-1 = (P × S, Σ k , ∆ , (p 0 , s 0 ), ⊥ , F × S) be a visibly Büchi pushdown automaton, where the set of transitions ∆ is such that if (p, γ) ----------→ ((p , q ), w) ∈ ∆ . The last letter of each tuple always stands for the visibly pushdown path variable π i : BP k-1 is visibly pushdown as its stack operations only depend on this variable. If χ k = ∀, we consider the complement BP k of BP k instead, which is a visibly pushdown automaton as well.

(a0,...,a k-1 ,ai) ----------→ (p , w) ∈ ∆ and q a k-1 ---→ q ∈ δ, then ((p, q), γ) (a0,...,a k-2 ,ai)
We can check the emptiness of BP 0 . If it is indeed empty, then T |= ψ.

It has been proven in [START_REF] Alur | Visibly pushdown languages[END_REF] that the complement of a VPDA incurs an exponential blow-up in terms of states. Hence, the technique shown here is exponential (in terms of time) in the size of P and ϕ.

Application. If we consider that π i range over T races ω (P) and that π j , j = i range over a regular abstraction α(T races ω (P)) of the actual set of traces, and we assume that χ j = ∀ for j = i, we can apply this result to over-approximate the model-checking problem, as detailed earlier in this section.

Model-checking HyperLTL with Bounded Phases

In this section, we use results on Multi-Stack Pushdown Automata to define an under-approximation of the model-checking problem of HyperLTL formulas with universal quantifiers for PDSs.

Multi-stack pushdown systems (MPDSs) are pushdown systems with multiple stacks. Their semantics is defined in a manner similar to PDSs, and so are configurations, traces, runs, Multi-Stack Pushdown Automata (MPDA), and the semantics of LTL. MPDA are unfortunately Turing powerful even with only two stacks. Thus, La Torre et al. introduced in [START_REF] La | A robust class of context-sensitive languages[END_REF] a restriction called phase-bounding: Definition 6 (Phases of runs). A run r of a MPDS M is said to be k-phased if it can be split in a sequence of k runs r 1 , . . . , r k of M (i.e. r = r 1 . . . r k ) such that during the execution of a given run r i , at most a single stack is popped from.

For a given integer k, this restriction can be used to define a phase-bounded semantics on MPDSs: only traces matched to runs with at most k phases are considered. It has been proven in [START_REF] Seth | Global reachability in bounded phase multi-stack pushdown systems[END_REF] that the backward reachability set of MPDSs with bounded phases is regular and can be effectively computed; this property can then be used to show that the following theorem holds: Theorem 5 (Model-checking with bounded phases [START_REF] Seth | Global reachability in bounded phase multi-stack pushdown systems[END_REF]). The modelchecking problem of LTL for MPDSs with bounded phases is decidable.

Phase-bounding can be used to under-approximate the set of traces of a MPDS. If a given LTL property ϕ does not hold for a MPDS M with a phasebounding constraint, it does not hold for the MPDS M w.r.t. the usual semantics as well. We write M |= k ϕ if the LTL formula ϕ holds for traces of M with at most k phases.

We can use decidability properties of MPDSs with bounded phases to under-approximate the model-checking problem for pushdown systems. Let P = (P, Σ, Γ, ∆, c 0 ) be a PDS on the input alphabet Σ = 2 AP , and ψ = ∀π 1 , . . . , ∀π n , ϕ, a HyperLTL formula on n trace variables with only universal quantifiers.

Our intuition is to define a MPDS M such that each stack represents a path variable of the HyperLTL formula. This MPDS is the product of n copies of P. Because ψ features universal quantifiers only, the model-checking problem of the LTL formula ϕ for M is then equivalent to the model-checking problem of ψ for P: M simulates n runs of P simultaneously, hence, LTL formulas on M can be used to synchronize these runs. We can therefore use a phase-bounded approximation of the former problem to under-approximate the latter.

We introduce the MPDS M = (P n , Σ n , Γ n , n, ∆ , c 0 ), with an initial configuration c 0 = (p 0 , . . . , p 0 ), ⊥, . . . , ⊥ ) ∈ P n ×Γ n and a set of transitions ∆ defined as follows: ∀d 1 , . . . , d n ∈ ∆ n where d i = (p i , γ i ) ai -→ (p i , w i ) for i = 1, . . . , n, the transition ((p 1 , . . . , p n ), γ 1 , . . . , γ n ) (a1,...,an) ------→ ((p 1 , . . . , p n ), w 1 , . . . , w n ) belongs to ∆ . The following lemma then holds:

Lemma 2. M |= ϕ if and only if P |= ψ.
As a consequence, if M |= ϕ, then P |= ψ. We can then consider a phasebounded analysis of M: for a given integer k, if M |= k ϕ, then M |= ϕ, hence P |= ψ. We can therefore under-approximate the model-checking problem of HyperLTL formulas with universal quantifiers only.

Applications to Security Properties

We apply in this section our results to information flow security, and remind how, as shown in [START_REF] Michael | Temporal logics for hyperproperties[END_REF], security policies can be expressed as HyperLTL formulas. If we model a given program as a PDS or a VPDS P following the method outlined in [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF], we can then either over-approximate or under-approximate an answer to the model-checking problem P |= ψ of a policy represented by a HyperLTL formula ψ for this program.

Observational Determinism

The strict non-interference security policy is the following: an attacker should not be able to distinguish two computations from their outputs if they only vary in their secret inputs. Few actual programs meet this requirement, and different versions of this policy have thus been defined.

We partition variables of a program into high and low security variables, and into input and output variables. The observational determinism property holds if, assuming two starting configurations have identical low security input variables, their low security output variables will be equal as well.

We model the program as a PDS P on the input alphabet 2 AP , where atomic propositions in AP contain variable values: if a variable x can take a value a, then (x, a) ∈ AP . We can express the observational determinism policy as the following HyperLTL formula:

ψ OD = ∀π 1 , ∀π 2 , ( a∈LSi (a π1 ⇔ a π2 )) ⇒ G ( b∈LSo (b π1 ⇔ b π2 ))
where LS i (resp. LS o ) is the set of low security input (resp. output) variables values. Using our techniques detailed in Sections 5 and 4.1, we can both underapproximate and over-approximate the model-checking problem P |= ψ OD that is otherwise undecidable. A context-free example. Let AP = {i, o, h 1 , h 2 }, LS i = {i}, LS o = {o}, and let HS i = {h 1 , h 2 } be a set of high security inputs. We suppose we are given a program that can be abstracted by the following PDS P on the alphabet Σ = 2 AP , the stack alphabet Γ = {γ, ⊥}, and the set of states P = {p 0 , p 1 , p 2 , p 3 , p 4 }, with the following set of transitions, as represented by Figure 1: We would like to check if P |= ψ OD , where ψ OD is the observational determinism HyperLTL formula outlined above. Intuitively, it will not hold: two runs always have the same input i but, if they do not push the same number of symbols on the stack, their low-security outputs will differ.

(init) (p 0 , ⊥) {i} --→ (p 0 , γ⊥) (µ 2 ) (p 2 , γ) {h1} ---→ (p 3 , ε) (λ 1 ) (p 0 , γ) {h1} ---→ (p 1 , γγ) (µ 3 ) (p 3 , γ) {o} --→ (p 2 , γ) (λ 2 ) (p 0 , γ) {h2} ---→ (p 1 , γγ) (ν 1 ) (p 3 , ⊥) {o} --→ (p 4 , ⊥) (λ 3 ) (p 1 , γ) {o} --→ (p 0 , γ) (ν 2 ) (p 4 , ⊥) {o} --→ (p 4 , ⊥) (µ 1 ) (p 1 , γ) {o} --→ (p 2 , γ) p0 p1 p2 p3 p4 ⊥ → γ⊥ : {i} γ → γγ : {h1}, γ → γγ : {h2} γ → γ : {o} γ → γ : {o} γ → ε : {h1} γ → γ : {o} ⊥ → ⊥ : {o} ⊥ → ⊥ : {o}
Since transitions of P are only labelled by singletons, we can write ρ instead of {ρ} when describing traces. The set T races ω (P) of infinite traces of P is equal to

n∈N i • ((h 1 + h 2 ) • o) n • (h 1 • o) n+1
• o * : from the bottom symbol ⊥, rules (init), (λ 1 ), (λ 2 ), and (λ 3 ) push n + 1 symbols γ on the stack, rules (µ 1 ), (µ 2 ), and (µ 3 ) pop these (n + 1) symbols, then rule (ν 2 ) loop in state p 4 once the bottom of the stack is reached again and rule (ν 1 ) has been applied. T races ω (P) is context-free, hence, we can't model-check the observational determinism policy on P using the algorithms outlined in [6].

Using the under-approximation technique outlined in Section 5, we can show that ψ OD does not hold if we bound the number of phases to 2: we find a counter-example

π 1 = i • h 2 • o • h 1 • o • o * and π 2 = i • (h 2 • o) 2 • (h 1 • o) 2 • o * .
We can therefore reach the conclusion that P |= ψ OD ; the observational determinism security policy therefore does not hold for the original program.

Declassification

The strict non-interference security policy is very hard to enforce as many programs must, one way or another, leak secret information during their execution. Thus, we must relax the previously defined security properties.

We introduce instead a declassification policy: at a given step, leaking a specific high security variable is allowed, but the observational determinism must otherwise holds. As an example, let's consider a program accepting a password as a high security input in its initial state, whose correctness is then checked during the next execution step. The program's behaviour then depends on the password's correctness. We express this particular declassification policy as the following HyperLTL formula:

ψ D = ∀π 1 , ∀π 2 , (( a∈LSi (a π1 ⇔ a π2 )) ∧ X (ρ π1 ⇔ ρ π2 )) ⇒ G ( b∈LSo (b π1 ⇔ b π2 ))
where ρ is a high security atomic proposition specifying that an input password is correct. Again, using our techniques detailed in Sections 5 and 4.1, we can both under-approximate and over-approximate the model-checking problem P |= ψ D .

Checking a password. We consider a program where the user can input a low-security username and a high-security password, then get different outputs depending on whether the password is true or not.

Let AP = {u, pw 1 , pw 2 , pw 3 , o, ρ, h 1 , h 2 }, LS i = {u}, LS o = {o}, let ρ be a variable that is allowed to leak, and let HS i = {pw 1 , pw 2 , pw 3 , h 1 , h 2 } be a set of high security inputs. Assuming there is only a single username u and three possible passwords pw 1 , pw 2 , pw 3 , pw 3 being the only right answer, we can consider the following PDS P on the alphabet Σ = 2 AP , the stack alphabet Γ = {γ, ⊥}, the set of states P = {p 0 , p 1 , p 2 , p 3 , p true , p f alse }, with the following set of transitions, as represented by Figure 2:

(init 1 ) (p 0 , ⊥) {u,pw1} -----→ (p f alse , ⊥) (µ 1 ) (p 1 , ⊥) {o} --→ (p 1 , ⊥) (init 2 ) (p 0 , ⊥) {u,pw2} -----→ (p f alse , ⊥) (µ 2 ) (p 2 , γ) {h1} ---→ (p 2 , γγ) (init 3 ) (p 0 , ⊥) {u,pw3} -----→ (p true , ⊥) (µ 3 ) (p 2 , γ) {h2} ---→ (p 3 , γ) (pw true ) (p true , ⊥) {ρ} --→ (p 1 , ⊥) (µ 4 ) (p 3 , γ) {h2} ---→ (p 3 , ε) (pw f alse ) (p f alse , ⊥) {o} --→ (p 2 , γ⊥) (µ 2 ) (p 3 , ⊥) {h1} ---→ (p 3 , ⊥)
We would like to check if P |= ψ D , where ψ D is the declassification HyperLTL formula outlined above. Obviously, if we consider that ρ ∈ LS o , then observational determinism does not hold: given the same username u, depending on whether the high-security password p i chosen is right or not, the low-security output will differ. However, intuitively, the declassification policy should hold: given two different input passwords, the PDS will behave in the same manner as long as both are either true or false. The set T races ω (P) of infinite traces of P is equal to ({u,

p 3 } • {ρ} • {o 1 } * )∪ n∈N (({u, p 1 } + {u, p 2 }) • {o} • {h 1 } n • {h 2 } n+2 • {h 1 } * ): from the bottom symbol ⊥,
if the right password pw 3 has been input, rules (init 3 ) and (p true ) lead to state p 1 where the PDS loops; otherwise, if the password is wrong, rules (init 1 ), (init 2 ) and (p f alse ) push a symbol γ and lead to state p 2 , where rule (µ 2 ) pushes n symbols γ on the stack, then the PDS switches to state p 3 where it pops these (n + 1) symbols with rules (µ 3 ) and (µ 4 ) then loops with rule (µ 5 ) once the bottom of the stack has been reached. T races ω (P) is context-free, hence, we can't model-check the declassification policy on P using the algorithms outlined in [6].

Using the overapproximation techniques detailed in Section 4.1, we can consider the regular abstraction α(T races ω (P)) = ({u,

p 3 } • {ρ} • {o 1 } * )∪ (({u, p 1 } + {u, p 2 }) • ∅ • {h 1 } * • {h 2 } * • {h 1 } * )
of the actual set of traces. We can then reach the conclusion that P |= ψ D , since this property holds for the over-approximation as well; the declassification security policy therefore holds for this example.

Non-Inference

Non-inference is a variant of the non-interference security policy. It states that, should all high security input variables be replaced by a dummy input λ, the behaviour of low security variables should not change.

We express this property as the following HyperLTL formula:

ψ = ∀π 1 , ∃π 2 , G ( x∈V h i (x, λ) π2 ) ∧ G ( b∈LS (b π1 ⇔ b π2 ))
where LS stands for the set of all low security variables values, V h i for the set of high security input variables, and (x, λ) means that variable x has value λ. We can't rely on the method outlined in 4.1 because π 2 is existentially quantified, but an over-approximation can nonetheless be found using the method detailed in Section 4.2, if we model the program as a VPDS P, choose π 2 as the visibly context-free path variable, and make it so that π 1 ranges over a regular abstraction of the traces.

A Proof of Theorem 1

Let L 1 and L 2 be two context-free languages, and P 1 = (P 1 , Σ ∪ {f }, Γ, ∆ 1 , p 1 0 , ⊥ , F 1 ) and P 2 = (P 2 , Σ ∪ {f }, Γ, ∆ 2 , p 2 0 , ⊥ , F 2 ) two PDA accepting L 1 and L 2 respectively. Without loss of generality, we can consider that P 1 ∩ P 2 = ∅. Let e 1 / ∈ P 1 , e 2 / ∈ P 2 , and f / ∈ Σ. We define two BPDA BP

i = (P i , 2 Σ∪{f } , Γ, ∆ i , p i 0 , ⊥ , {e i }) for i = 1, 2, where ∆ i is such that (e i , γ) {f } --→ (e i , γ) ∈ ∆ i and (p f , γ) {f } --→ (e i , γ) ∈ ∆ i for all γ ∈ Γ and p f ∈ F i , and if (p, γ) a -→ (p , w) ∈ ∆ i , then (p, γ) {a} --→ (p , w) ∈ ∆ i .
If we consider that {a} is equivalent to the label a ∈ Σ ∪ {f }, BP 1 and BP 2 accept L 1 f ω and L 2 f ω respectively. Since HyperLTL formulas apply to infinite words in 2 A P , for i = 1, 2, we have designed a BPDA BP i that extends words in L i by adding a final dead state e i from which the automaton can only output an infinite sequence of a special ending symbol f .

We consider the PDS P = ({p

0 } ∪ P 1 ∪ P 2 , {{ι 1 }, {ι 2 }} ∪ 2 Σ∪{f } , Γ, ∆, c 0 ), where p 0 / ∈ P 1 ∪ P 2 , ι 1 , ι 2 / ∈ Σ ∪ {f }, c 0 = p 0 , ⊥ , and ∆ = {(p 0 , ⊥) {ι 1 } ---→ (p 1 0 , ⊥), (p 0 , ⊥) {ι 2 } ---→ (p 2 0 , ⊥)} ∪ ∆ 1 ∪ ∆ 2 .
The PDS P can simulate either BP 1 or BP 2 , depending on whether it applies first a transition labelled by {ι 1 } or {ι 2 } from the initial configuration c 0 .

We introduce the formula

ψ = ∃π 1 , ∃π 2 , ϕ start ∧ ϕ sync ∧ ϕ end on AP = {ι 1 , ι 2 } ∪ Σ ∪ {f }, where ϕ start = ι 1 π1 ∧ ι 2 π2 , ϕ sync = XG a∈AP (a π1 ⇔ a π2 ), and
ϕ end = FG (f π1 ∧ f π2
). We suppose that P |= ψ; ϕ start expresses that trace variables π 1 and π 2 represent runs of BP 1 and BP 2 respectively. ϕ sync means that the two traces are equal from their second letter onwards. ϕ end implies that the two traces are accepting runs. Therefore, if P |= ψ, then B 1 and B 2 share a common accepting run and L 1 ∩ L 2 = ∅. On the other hand, if L 1 ∩ L 2 = ∅, there is an accepting run π common to B 1 and B 2 , and we can then find two traces π 1 and π 2 of P such that the formula ∃π 1 , ∃π 2 , ϕ start ∧ ϕ sync ∧ ϕ end holds. The emptiness problem is, however, undecidable, and therefore so must be the model-checking problem.

B Proof of Theorem 2

In order to prove this theorem, we will rely on a class of two-stack automata called 2-Visibly Pushdown Automata (2-VPDA) introduced in [START_REF] Carotenuto | 2-visibly pushdown automata[END_REF]. Let Σ be a finite input alphabet with two partitions

Σ = Σ cj ∪ Σ rj ∪ Σ lj , j ∈ {1, 2}. We then introduce a 2-pushdown alphabet ℵ = (Σ c1 , Σ r1 , Σ l1 ) , (Σ c2 , Σ r2 , Σ l2 ) on Σ.
Definition 7 (2-Visibly Pushdown Automaton). A 2-Visibly Pushdown Automaton (2-VPDA) over ℵ is a tuple D = (P, Σ, Γ, ∆, c 0 , F ) 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, c 0 = p 0 , ⊥, ⊥ ∈ P × Γ × Γ an initial configuration, and F ⊆ P a set of final states. Moreover, ∆ is such that ∀d ∈ ∆, and for i ∈ {1, 2}:

if d is labelled by a letter in Σ ci , d pushes a word on the i-th stack regardless of its top stack symbol; if d is labelled by a letter in Σ ri , d pops the top letter of of the i-th stack; if d is labelled by a letter in Σ li , d does not modify the i-th stack.

The semantics of 2-VPDA is defined in a manner similar to PDA, and so are configurations, runs, execution paths, languages, and 2-Büchi Visibly Pushdown Automata (2-BVPDA). The following theorem holds: Theorem 6 (Undecidability of the emptiness problem for 2-VPDA [START_REF] Carotenuto | 2-visibly pushdown automata[END_REF]).

The emptiness problem for 2-VPDA is undecidable.

Our intuition is to prove theorem 2 by reducing the emptiness problem for 2-VPDA to the model-checking problem of HyperLTL for VPDSs.

Let D = (P, Σ, Γ, ∆, p 0 , ⊥, ⊥ , F ) be a 2-VPDA on an input alphabet Σ according to a partition ℵ = (Σ c1 , Σ r1 , Σ l1 ) , (Σ c2 , Σ r2 , Σ l2 ) . We introduce a 2-BVPDA BD = (P, 2 Σ∪{f } , Γ, ∆ , p 0 , ⊥, ⊥ , {e}) such that (e, γ, γ ) Let P 1 and P 2 (resp. ∆ 1 and ∆ 2 ) be two disjoint copies of P (resp. ∆ ). To each p ∈ P (resp. d ∈ ∆ ), we match its copies p 1 ∈ P 1 and p 2 ∈ P 2 (resp. d 1 ∈ ∆ 1 and d 2 ∈ ∆ 2 ). We define a PDS P = ({σ} ∪ P 1 ∪ P 2 , {{ι 1 }, {ι 2 }, {f }} ∪ 2 ∆ 1 ∪ 2 ∆ 2 , Γ, δ, σ, ⊥, ). The set δ is such that, for each transition d = (p, γ 1 , γ 2 --→ (p 2 , w 2 ). Transitions in δ are projections of the original transitions of the 2-BVPDA on one of its two stacks; their label depends on the original transition in ∆, unless they are labelled by f . Moreover, (σ, ⊥) {ι1} ---→ (p 1 0 , ⊥) and (σ, ⊥) {ι2} ---→ (p 2 0 , ⊥) both belong to δ. P is such that it can either simulate the first or the second stack of the 2-BVPDA BD, depending on which transition was used first. P is indeed a VPDS: a suitable partition of its input alphabet can be computed depending on which operation on the i-th stack transitions in ∆ perform. As an example, if d ∈ ∆ pushes a symbol on the first stack and pops from the second, d 1 belongs to the call alphabet and d 2 , to the return alphabet.

Given a set of trace variables V = {π 1 , π 2 } and a predicate alphabet AP = {ι 1 , ι 2 , f } ∪ ∆ 1 ∪ ∆ 2 , we then consider an unquantified HyperLTL formula ϕ of the form ϕ = ϕ start ∧ ϕ sync ∧ ϕ end , where ϕ's sub-formulas are defined as follows:

Initialization formula: ϕ start = ι 1 π1 ∧ ι 2 π2 ; Π |= ϕ start if and only if for i ∈ {1, 2}, Π[1, ∞](π i ) is a run that simulates the i-th stack of BD; Synchronization formula: ϕ sync = XG Therefore, if Π |= ϕ, we have Π(π i ) = (ι i , d i 1 , d i 2 . . .) for i = 1, 2, and the sequence of transitions (d 1 , d 2 , . . .) ∈ ∆ ω defines an accepting run on BD. Therefore, we can solve the model-checking problem P |= ∃π 1 , ∃π 2 , ϕ, if and only if we can determine whether L (BD) is empty or not, hence, L (D) as well. By here is a contradiction and the former problem is undecidable.

Fig. 1 :

 1 Fig. 1: The PDS P

Fig. 2 :

 2 Fig. 2: The PDS P

  γ, γ ) ∈ ∆ and (p f , γ, γ ) {f } --→ (e, γ, γ ) ∈ ∆ for all γ, γ ∈ Γ and p f ∈ F , and if (p, γ, γ ) a -→ (p , w, w ) ∈ ∆, then (p, γ, γ ) {a} --→ (p , w, w ) ∈ ∆ on the input alphabet Σ ∪ {f }.Obviously, BD is visibly if we add the symbol f to Σ l1 and Σ l2 and accepts L(D)f ω , assuming the label {a} is equivalent to the label a ∈ Σ ∪ {f }.

  w 1 , w 2 ) ∈ ∆, a = f , we add two transitions (p 1 , γ 1 ) {d 1 } ---→ (p 1 , w 1 ) and (p 2 , γ 2 ) {d 2 } ---→ (p 2 , w 2 ) to δ. If a = f , we add instead (p 1 , γ 1 ) {f } --→ (p 1 , w 1 ) and (p 2 , γ 2 ) {f }

d∈∆ (d 1 π1 ⇔ d 2

 12 π2 ); Π |= ϕ start ∧ ϕ sync if and only if Π[1, ∞](π 1 ) and Π[1, ∞](π 2 ) can be matched to a common run of the 2-BVPDA BD; Acceptation formula:ϕ end = FG (f π1 ∧ f π2 ); Π |= ϕ start ∧ ϕ sync ∧ ϕ end if and only if Π[1, ∞](π 1 ) and Π[1, ∞](π 2) can be used to define an accepting run of the 2-BVPDA BD.