# Verification of Opacity and Diagnosability for Pushdown Systems

Authors: Koichi Kobayashi; Kunihiko Hiraishi
Journal: Journal of Applied Mathematics
 (2013)

---

## Abstract

In control theory of discrete event systems (DESs), one of the challenging topics is the extension of theory of finite-state DESs to that of infinite-state DESs. In this paper, we discuss verification of opacity and diagnosability for infinite-state DESs modeled by pushdown automata (called here pushdown systems). First, we discuss opacity of pushdown systems and prove that opacity of pushdown systems is in general undecidable. In addition, a decidable class is clarified. Next, in diagnosability, we prove that under a certain assumption, which is different from the assumption in the existing result, diagnosability of pushdown systems is decidable. Furthermore, a necessary condition and a sufficient condition using finite-state approximations are derived. Finally, as one of the applications, we consider data integration using XML (Extensible Markup Language). The obtained result is useful for developing control theory of infinite-state DESs.


---

## Body

## 1. Introduction

To extend control theory of discrete event systems (DESs) expressed by finite automata [1] to that of infinite-state DESs is one of the challenging topics. Infinite automata [2] and unbounded Petri nets [3, 4] are common models of infinite-state DESs. In this paper, we focus on a pushdown automaton (PDA) [5, 6], which is one of the standard classes of infinite automata. A PDA is a finite automaton having a stack with infinite length, and a state transition is decided by the input symbol (event) and the stack symbol in the top of the stack. The stack can be manipulated by the input symbol in which the empty symbol is included. Furthermore, a visibly pushdown automaton (VPA) has been proposed as a special class of PDAs [7, 8]. Input symbols in a VPA are composed of three kinds of symbols, that is, push manipulations, pop manipulations, and internal manipulations (see Section 2.1 for further details). It is easier to analyze a VPA than a PDA. Some examples are given as applications of PDAs and VPAs. In the modeling of a software system, a PDA is frequently used (see, e.g., [9]). Also in analysis of a cyber-physical system (CPS), which has recently attracted much attention, a PDA is used [10]. A CPS is a system featuring a combination between computer systems and physical systems [11]. To model the complicate behavior of such a CPS, it is important to use a PDA. In addition, as an application of a PDA, intrusion detection in the field of computer security has been studied so far [12]. As an application of a VPA, analysis of XML (Extensible Markup Language), which is one of the markup languages and is widely used in several fields [8, 13], has been studied so far [8, 13]. Thus a PDA and a VPA have many applications, and, developing theory of DESs using a PDA and a VPA is important.For DESs modeled by PDAs and VPAs (called here pushdown systems), supervisory control [9, 14] and diagnosability verification [15] have been studied so far. Diagnosability verification is the problem of testing if the state reaches a given failure state under partial observations. In diagnosability verification, it has been proven in [15] that diagnosability of pushdown systems is in general undecidable and is decidable under the assumption that stack manipulations are completely observed. This assumption is very strong and is not practical. Furthermore, it is important to approximately verify diagnosability for pushdown systems without assumptions. On the other hand, in recent years, opacity in computer security has been studied in the framework of DESs [16–22]. Opacity aims to determine if a secret behavior in the system is kept opaque to outsiders. In [17], it has been shown that opacity verification of infinite-state systems is undecidable. Also in [19], opacity verification of infinite-state systems has been discussed using approximate models. However, to our knowledge, opacity verification of pushdown systems has not been studied so far.In this paper, we discuss verification of opacity and diagnosability for pushdown systems based on basic results in formal language theory [5, 6]. In opacity verification, it is proven that opacity of pushdown systems is in general undecidable. Furthermore, we clarify a condition such that opacity is decidable. In diagnosability verification, first, it is proven that if a part of observations in the system can be expressed as a regular language, that is, a language accepted by some finite automaton, then diagnosability is decidable. Next, a necessary condition for the pushdown system not to be diagnosable is derived based on finite-state overapproximations. In a similar way, a sufficient condition is also derived based on finite-state underapproximations. The proposed conditions enable us to verify diagnosability of a wider class of pushdown systems. Also, the relation among opacity verification, diagnosability verification, and the sensor selection problem is discussed. Finally, as one of the applications, we consider data integration of XML documents. In the case that documents in databases are expressed by the XML, one of the important problems is data integration, which is called here XML data integration. In particular, we discuss XML data integration with security considerations and show the effectiveness of the proposed approach. The conference paper [23] is a preliminary version of this paper. In this paper, we provide improved formulations and explanations, discussion on the computational complexity, and application to XML data integration.This paper is organized as follows. In Section2, first, the outline of pushdown systems is explained. Next, decidable problems and undecidable problems in PDAs and VPAs are explained. Finally, we introduce a finite-state overapproximation of PDAs. In Section 3, opacity verification is discussed. In Section 4, diagnosability verification is discussed, and some diagnosability conditions are derived. In Section 5, related topics are discussed. In Section 6, we consider an application of the proposed approach to XML data integration. In Section 7, we conclude this paper.Notation.
For a finite setΣ, let Σ* denote a set of all finite strings, which consist of elements in Σ, including the empty string ɛ. Let Σω denote a set of all infinite strings. Let |Σ| denote the number of elements in Σ. The set 𝒩 is defined as 𝒩:={0,1,2,…}.


## 2. Preliminaries

In this section, first, we introduce pushdown automata and their subclass. Next, undecidable problems in pushdown automata are explained. Furthermore, we introduce assumptions that will enable the undecidable problems to become decidable. Finally, a finite-state overapproximation used in diagnosability verification is explained.


### 2.1. Pushdown Systems

Consider the following pushdown automaton (PDA):(1)G=(Q,Σ,Γ,Δ,q0,Z0,F),
where Q is the finite set of states, Σ∪{ɛ} is the finite set of input symbols (events), Γ are the finite set of stack symbols, Δ=Δpush∪Δpop∪Δint: transition relations, q0∈Q are the initial state, and Z0∈Γ is the initial stack symbol. F⊆Q: the set of final states.In theory of DESs, the empty stringɛ is regarded as an unobservable event. In the PDA to be studied here, transition relations are composed of Δpush, Δpop, and Δint, which are called here a “push” manipulation, a “pop” manipulation, and an “internal” manipulation, respectively. In the push manipulation, a particular symbol is pushed to the top of the stack. In the pop manipulation, the top of the stack is popped off. In the internal manipulation, the stack is not changed, and only the state is changed. More precisely, three manipulations are given as
(2)Δpush⊆(Q×Σ×Γ)×Q,Δpop⊆(Q×Σ)×(Q×(Γ-{Z0})),Δint⊆(Q×Σ)×Q,
respectively. Functional forms of δ=(q,σ,γ,q′)∈Δpush, δ=(q,σ,q′,γ)∈Δpop, and δ=(q,σ,q′)∈Δint are given as δ:(q,σ,γ)→q′, δ:(q,σ)→(q′,γ), and δ:(q,σ)→q′, respectively. If the state and the symbol sequence in the stack are uniquely determined for given initial state and input symbol, a given PDA is said to be deterministic.In addition, if the state reaches some element of a subsetQ′⊆Q by an execution u∈Σ*, then it is said that an execution u reaches Q′. Furthermore, we can naturally extend these definitions to an infinite execution. If the state reaches some element of Q′ by one of the prefixes of an infinite execution w∈Σω, then it is said that the infinite execution w reaches Q′.LetΣo⊆Σ denote the set of observable events, and the set Σuo:=Σ¯o is the set of unobservable events. Let L(G) denote the set of languages accepted by G. Then let P(L(G)) denote the set of sequences of observable events; that is, the following two relations hold:
(3)P(σ)=σifσ∈Σo,P(σ)=ɛifσ∈Σuo.SinceP(σ1)=P(σ2) is satisfied for the two unobservable events σ1, σ2∈Σuo, two events σ1, σ2 are indistinguishable.Next, we introduce visibly PDAs [7, 8] as a subclass of PDAs.Definition 1.
A PDA (1) is said to be a visibly PDA (VPA) if Σ comprises Σ=Σpush∪Σpop∪Σint, where Σpush, Σpop, and Σint are input symbols corresponding to Δpush, Δpop, and Δint, respectively.In VPAs, manipulations to the stack can be visualized fromΣ.We illustrate this with a simple example.Example 2.
Consider the VPAG in Figure 1, where
(4)Q={q0,q1,q2},Σ={a,b,c,d},Γ={Z0,X,Y},Δpush={(q0,a,X,q0),(q0,a,Y,q0),(q0,a,X,q1)},Δpop={(q1,b,q1,X),(q2,d,q2,Y)},Δint={(q0,c,q2)},F={q1,q2}⊂Q.
In Figure1, a/+X and a/+Y express push manipulations, b/-X and d/-Y express pop manipulations, and c expresses an internal manipulation. Since Σ={a,b,c,d} comprises
(5)Σpush={a},Σpop={b,d},Σint={c},
we see that this automaton is a VPA. In addition, we have
(6)L(G)={anbn∣n≥1}∪{amcdm∣m≥0},
where anbn corresponds to the set of event sequences such that the state reaches q1. ancdn corresponds to the set of event sequences such that the state reaches q2.Figure 1
Example of VDPDAsG.Hereafter, a discrete event system expressed by a PDA and a VPA is called a DES-PDA and a DES-VPA, respectively. If it is not necessary to distinguish a DES-PDA and a DES-VPA, then these discrete event systems are called here pushdown systems (PDSs).


### 2.2. Decidable Problems and Undecidable Problems in Pushdown Automata

In this subsection, we explain decidable problems and undecidable problems in a languageL(G) accepted by PDA or VPA G, that is, a context-free language (CFL). See [5, 6] for further details.Suppose that the two PDAsG1 and G2 are given. Then L(G1) and L(G2) are CFLs, and the following result is known.Lemma 3.
The emptiness problem of an intersection ofL(G1) and L(G2), that is, the problem of deciding if L(G1)∩L(G2)=∅ holds, is undecidable.This lemma follows from the fact thatL(G1)∩L(G2) is not a CFL in general. The emptiness problem of an intersection of two CFLs is decidable under a given assumption.Lemma 4.
Assume that eitherL(G1) or L(G2) is given as a regular language; that is, either G1 or G2 is given as a finite automaton. Then the emptiness problem of an intersection of L(G1) and L(G2) is decidable. In addition, this problem can be solved in PTIME.Under the assumption in Lemma4, L(G1)∩L(G2) is a CFL, and the emptiness problem is decidable. This result in the emptiness problem of an intersection is used in diagnosability verification in Section 4.Next, the following result on the inclusion problem has been obtained.Lemma 5.
The inclusion problem of two PDAs,G1 and G2, that is, the problem of deciding if L(G1)⊆L(G2) holds, is undecidable.For VPAs, the following result has been obtained [7].Lemma 6.
The inclusion problem of two VPAsG1 and G2, that is, the problem of deciding if L(G1)⊆L(G2) holds is decidable. In addition, this problem can be solved in EXPTIME.On the other hand, a class of deterministic PDAs such that the inclusion problem is decidable is called superdeterministic PDAs [24]. A deterministic VPA is a subclass of the superdeterministic PDAs. This fact is clear from the definitions in [7, 24]. As a result, the following result can be obtained.Lemma 7.
Assume thatG1 and G2 are given as a PDA and a deterministic VPA, respectively. Then the problem of deciding if L(G1)⊆L(G2) is decidable. In addition, this problem can be solved in 2-EXPTIME.These results of the inclusion problem are used in opacity verification in Section3.


### 2.3. Finite-State Overapproximation of Pushdown Automata

In this section, we explain the finite-state overapproximations of PDAs. Several approximations have been proposed so far (see, e.g., [25] for further details). In this paper, the following finite-state overapproximation proposed in [9] is used.Definition 8.
For a given PDAG of (1), the finite-state overapproximation of G is defined by
(7)Go=(Q,Σ.Q,Δo,q0,F),
where Σ.Q and Δo are defined as follows:(i)
Σ.Q={σ·q∣σ∈Σ,q∈Q}.(ii)
Δo is given as Δo⊆(Q×Σ.Q)×Q. δ=(q,σ·q′,q′)∈Δo holds if and only if one of the following three conditions holds:
(1)
δ=(q,σ,γ,q′)∈Δpush holds for some γ∈Γ;(2)
δ=(q,σ,q′,γ)∈Δpop holds for some γ∈Γ;(3)
δ=(q,σ,q′)∈Δint holds.LetGs denote the PDA obtained by replacing σ∈Σ with σ.q∈Σ.Q. In the transitions of Go, the conditions on the stack are ignored. So L(Gs)⊆L(Go) holds.A finite-state overapproximation will be used in the topic on diagnosability (see Section4.4 for further details).


## 2.1. Pushdown Systems

Consider the following pushdown automaton (PDA):(1)G=(Q,Σ,Γ,Δ,q0,Z0,F),
where Q is the finite set of states, Σ∪{ɛ} is the finite set of input symbols (events), Γ are the finite set of stack symbols, Δ=Δpush∪Δpop∪Δint: transition relations, q0∈Q are the initial state, and Z0∈Γ is the initial stack symbol. F⊆Q: the set of final states.In theory of DESs, the empty stringɛ is regarded as an unobservable event. In the PDA to be studied here, transition relations are composed of Δpush, Δpop, and Δint, which are called here a “push” manipulation, a “pop” manipulation, and an “internal” manipulation, respectively. In the push manipulation, a particular symbol is pushed to the top of the stack. In the pop manipulation, the top of the stack is popped off. In the internal manipulation, the stack is not changed, and only the state is changed. More precisely, three manipulations are given as
(2)Δpush⊆(Q×Σ×Γ)×Q,Δpop⊆(Q×Σ)×(Q×(Γ-{Z0})),Δint⊆(Q×Σ)×Q,
respectively. Functional forms of δ=(q,σ,γ,q′)∈Δpush, δ=(q,σ,q′,γ)∈Δpop, and δ=(q,σ,q′)∈Δint are given as δ:(q,σ,γ)→q′, δ:(q,σ)→(q′,γ), and δ:(q,σ)→q′, respectively. If the state and the symbol sequence in the stack are uniquely determined for given initial state and input symbol, a given PDA is said to be deterministic.In addition, if the state reaches some element of a subsetQ′⊆Q by an execution u∈Σ*, then it is said that an execution u reaches Q′. Furthermore, we can naturally extend these definitions to an infinite execution. If the state reaches some element of Q′ by one of the prefixes of an infinite execution w∈Σω, then it is said that the infinite execution w reaches Q′.LetΣo⊆Σ denote the set of observable events, and the set Σuo:=Σ¯o is the set of unobservable events. Let L(G) denote the set of languages accepted by G. Then let P(L(G)) denote the set of sequences of observable events; that is, the following two relations hold:
(3)P(σ)=σifσ∈Σo,P(σ)=ɛifσ∈Σuo.SinceP(σ1)=P(σ2) is satisfied for the two unobservable events σ1, σ2∈Σuo, two events σ1, σ2 are indistinguishable.Next, we introduce visibly PDAs [7, 8] as a subclass of PDAs.Definition 1.
A PDA (1) is said to be a visibly PDA (VPA) if Σ comprises Σ=Σpush∪Σpop∪Σint, where Σpush, Σpop, and Σint are input symbols corresponding to Δpush, Δpop, and Δint, respectively.In VPAs, manipulations to the stack can be visualized fromΣ.We illustrate this with a simple example.Example 2.
Consider the VPAG in Figure 1, where
(4)Q={q0,q1,q2},Σ={a,b,c,d},Γ={Z0,X,Y},Δpush={(q0,a,X,q0),(q0,a,Y,q0),(q0,a,X,q1)},Δpop={(q1,b,q1,X),(q2,d,q2,Y)},Δint={(q0,c,q2)},F={q1,q2}⊂Q.
In Figure1, a/+X and a/+Y express push manipulations, b/-X and d/-Y express pop manipulations, and c expresses an internal manipulation. Since Σ={a,b,c,d} comprises
(5)Σpush={a},Σpop={b,d},Σint={c},
we see that this automaton is a VPA. In addition, we have
(6)L(G)={anbn∣n≥1}∪{amcdm∣m≥0},
where anbn corresponds to the set of event sequences such that the state reaches q1. ancdn corresponds to the set of event sequences such that the state reaches q2.Figure 1
Example of VDPDAsG.Hereafter, a discrete event system expressed by a PDA and a VPA is called a DES-PDA and a DES-VPA, respectively. If it is not necessary to distinguish a DES-PDA and a DES-VPA, then these discrete event systems are called here pushdown systems (PDSs).


## 2.2. Decidable Problems and Undecidable Problems in Pushdown Automata

In this subsection, we explain decidable problems and undecidable problems in a languageL(G) accepted by PDA or VPA G, that is, a context-free language (CFL). See [5, 6] for further details.Suppose that the two PDAsG1 and G2 are given. Then L(G1) and L(G2) are CFLs, and the following result is known.Lemma 3.
The emptiness problem of an intersection ofL(G1) and L(G2), that is, the problem of deciding if L(G1)∩L(G2)=∅ holds, is undecidable.This lemma follows from the fact thatL(G1)∩L(G2) is not a CFL in general. The emptiness problem of an intersection of two CFLs is decidable under a given assumption.Lemma 4.
Assume that eitherL(G1) or L(G2) is given as a regular language; that is, either G1 or G2 is given as a finite automaton. Then the emptiness problem of an intersection of L(G1) and L(G2) is decidable. In addition, this problem can be solved in PTIME.Under the assumption in Lemma4, L(G1)∩L(G2) is a CFL, and the emptiness problem is decidable. This result in the emptiness problem of an intersection is used in diagnosability verification in Section 4.Next, the following result on the inclusion problem has been obtained.Lemma 5.
The inclusion problem of two PDAs,G1 and G2, that is, the problem of deciding if L(G1)⊆L(G2) holds, is undecidable.For VPAs, the following result has been obtained [7].Lemma 6.
The inclusion problem of two VPAsG1 and G2, that is, the problem of deciding if L(G1)⊆L(G2) holds is decidable. In addition, this problem can be solved in EXPTIME.On the other hand, a class of deterministic PDAs such that the inclusion problem is decidable is called superdeterministic PDAs [24]. A deterministic VPA is a subclass of the superdeterministic PDAs. This fact is clear from the definitions in [7, 24]. As a result, the following result can be obtained.Lemma 7.
Assume thatG1 and G2 are given as a PDA and a deterministic VPA, respectively. Then the problem of deciding if L(G1)⊆L(G2) is decidable. In addition, this problem can be solved in 2-EXPTIME.These results of the inclusion problem are used in opacity verification in Section3.


## 2.3. Finite-State Overapproximation of Pushdown Automata

In this section, we explain the finite-state overapproximations of PDAs. Several approximations have been proposed so far (see, e.g., [25] for further details). In this paper, the following finite-state overapproximation proposed in [9] is used.Definition 8.
For a given PDAG of (1), the finite-state overapproximation of G is defined by
(7)Go=(Q,Σ.Q,Δo,q0,F),
where Σ.Q and Δo are defined as follows:(i)
Σ.Q={σ·q∣σ∈Σ,q∈Q}.(ii)
Δo is given as Δo⊆(Q×Σ.Q)×Q. δ=(q,σ·q′,q′)∈Δo holds if and only if one of the following three conditions holds:
(1)
δ=(q,σ,γ,q′)∈Δpush holds for some γ∈Γ;(2)
δ=(q,σ,q′,γ)∈Δpop holds for some γ∈Γ;(3)
δ=(q,σ,q′)∈Δint holds.LetGs denote the PDA obtained by replacing σ∈Σ with σ.q∈Σ.Q. In the transitions of Go, the conditions on the stack are ignored. So L(Gs)⊆L(Go) holds.A finite-state overapproximation will be used in the topic on diagnosability (see Section4.4 for further details).


## 3. Opacity Verification

This section looks at opacity verification of PDSs. First, the notion of opacity is defined. Next, after a condition for a PDS to be opaque is derived, a decidable class of PDSs is clarified.


### 3.1. Definition of Opacity

First, secret states are defined. LetQs⊂F denote the set of secret states. Then we define the notion of opacity based on the definition in [20].Definition 9.
For the PDSG of (1), suppose that the set of secret states Qs and the set of observable events Σo are given. Then the PDS is said to be opaque if for all t∈L(G) there exists s∈L(G)-{t} such that if t reaches Qs, then s does not reach Qs and P(s)=P(t).Several definitions of opacity have been proposed so far (see, e.g., [17, 20–22]). In this paper, the simplest definition in [20] is used.


### 3.2. Decidability of Opacity

LetV1 denote the set of finite event sequences such that the state reaches Qs. Let V2 denote the set of finite event sequences such that the state reaches Q-Qs. Then the opacity condition of PDSs can be derived as follows.Theorem 10.
A PDS is opaque if and only ifP(V1)⊆P(V2) holds.Proof.
If a PDS is opaque, thenP(V1) is included in P(V2). Conversely, if P(V1)⊆P(V2) holds, then for any v1∈P(V1), there exists v2∈P(V2) such that v1=v2. So the PDS is opaque.From Lemma5 and Theorem 10, we can obtain the following result immediately.Theorem 11.
Opacity of a DES-PDA is in general undecidable.In addition, from Lemma5 and Theorem 10, we can obtain the following result.Theorem 12.
Opacity of a DES-VPA is in general undecidable.Proof.
Even ifV1 and V2 are languages accepted by VPAs, then P(V1) and P(V2) are in general given as languages accepted by PDAs [15]. Then, from Lemma 5 and Theorem 10, opacity of a DES-VPA is undecidable.From Theorems11 and 12, we see that opacity of a DES-PDA and a DES-VPA are in general undecidable. On the other hand, from Lemma 6 and Theorem 10, we see that if observations of a DES-PDA is expressed by some VPA, then opacity of a DES-PDA may be decidable. Then we can obtain the following result.Theorem 13.
Assume thatP(V1) and P(V2) are languages accepted by VPAs, respectively. Then the problem of deciding if P(V1)⊆P(V2) holds is decidable; that is, opacity of a PDS is decidable. In addition, this problem can be solved in EXPTIME.In addition, from Lemma7 and Theorem 10, we can obtain the following result.Theorem 14.
Assume thatP(V1) and P(V2) are languages accepted by a PDA and a deterministic VPA, respectively. Then the problem of deciding if P(V1)⊆P(V2) holds is decidable; that is, opacity of a PDS is decidable. In addition, this problem can be solved in 2-EXPTIME.From Theorem14, we see that if P(V2) is given as a language accepted by a deterministic VPA, then the decidable condition is relaxed. Comparing Theorem 13 with Theorem 14, the inclusion problem in Theorem 14 is more difficult than that in Theorem 13. This is because in Theorem 14, P(V1) may be given as a language accepted by a PDA. If an overapproximation of a PDA can be derived as a VPA, then we can obtain a sufficient condition of a PDS to be opaque. In future work we plan to consider how to approximate a PDA by a VPA. On the other hand, in recent years, VPAs have been applied to several applications (see, e.g., [7–9]). Therefore, Theorem 13 and Theorem 14 will be useful.Finally, we show a simple example.Example 15.
Consider the DES-VPA in Figure1. Assume d=b. Suppose that Σo={a,b}, Σuo={c}, and Qs={q2} are given. Then we obtain
(8)P(V1)=P(V2)=anbn.
P
(
V
1
) and P(V2) are languages accepted by VPAs, respectively, and P(V1)=P(V2) holds. Therefore, this system is opaque.


## 3.1. Definition of Opacity

First, secret states are defined. LetQs⊂F denote the set of secret states. Then we define the notion of opacity based on the definition in [20].Definition 9.
For the PDSG of (1), suppose that the set of secret states Qs and the set of observable events Σo are given. Then the PDS is said to be opaque if for all t∈L(G) there exists s∈L(G)-{t} such that if t reaches Qs, then s does not reach Qs and P(s)=P(t).Several definitions of opacity have been proposed so far (see, e.g., [17, 20–22]). In this paper, the simplest definition in [20] is used.


## 3.2. Decidability of Opacity

LetV1 denote the set of finite event sequences such that the state reaches Qs. Let V2 denote the set of finite event sequences such that the state reaches Q-Qs. Then the opacity condition of PDSs can be derived as follows.Theorem 10.
A PDS is opaque if and only ifP(V1)⊆P(V2) holds.Proof.
If a PDS is opaque, thenP(V1) is included in P(V2). Conversely, if P(V1)⊆P(V2) holds, then for any v1∈P(V1), there exists v2∈P(V2) such that v1=v2. So the PDS is opaque.From Lemma5 and Theorem 10, we can obtain the following result immediately.Theorem 11.
Opacity of a DES-PDA is in general undecidable.In addition, from Lemma5 and Theorem 10, we can obtain the following result.Theorem 12.
Opacity of a DES-VPA is in general undecidable.Proof.
Even ifV1 and V2 are languages accepted by VPAs, then P(V1) and P(V2) are in general given as languages accepted by PDAs [15]. Then, from Lemma 5 and Theorem 10, opacity of a DES-VPA is undecidable.From Theorems11 and 12, we see that opacity of a DES-PDA and a DES-VPA are in general undecidable. On the other hand, from Lemma 6 and Theorem 10, we see that if observations of a DES-PDA is expressed by some VPA, then opacity of a DES-PDA may be decidable. Then we can obtain the following result.Theorem 13.
Assume thatP(V1) and P(V2) are languages accepted by VPAs, respectively. Then the problem of deciding if P(V1)⊆P(V2) holds is decidable; that is, opacity of a PDS is decidable. In addition, this problem can be solved in EXPTIME.In addition, from Lemma7 and Theorem 10, we can obtain the following result.Theorem 14.
Assume thatP(V1) and P(V2) are languages accepted by a PDA and a deterministic VPA, respectively. Then the problem of deciding if P(V1)⊆P(V2) holds is decidable; that is, opacity of a PDS is decidable. In addition, this problem can be solved in 2-EXPTIME.From Theorem14, we see that if P(V2) is given as a language accepted by a deterministic VPA, then the decidable condition is relaxed. Comparing Theorem 13 with Theorem 14, the inclusion problem in Theorem 14 is more difficult than that in Theorem 13. This is because in Theorem 14, P(V1) may be given as a language accepted by a PDA. If an overapproximation of a PDA can be derived as a VPA, then we can obtain a sufficient condition of a PDS to be opaque. In future work we plan to consider how to approximate a PDA by a VPA. On the other hand, in recent years, VPAs have been applied to several applications (see, e.g., [7–9]). Therefore, Theorem 13 and Theorem 14 will be useful.Finally, we show a simple example.Example 15.
Consider the DES-VPA in Figure1. Assume d=b. Suppose that Σo={a,b}, Σuo={c}, and Qs={q2} are given. Then we obtain
(8)P(V1)=P(V2)=anbn.
P
(
V
1
) and P(V2) are languages accepted by VPAs, respectively, and P(V1)=P(V2) holds. Therefore, this system is opaque.


## 4. Diagnosability Verification

In this section, first, diagnosability for the PDS (1) is defined according to the definition in [15, 26, 27]. Next, after the existing results in [15] are explained, two kinds of diagnosability conditions are proposed.


### 4.1. Definition of Diagnosability

First, failure states are defined. LetQf⊂Q denote the set of failure states. For Qf, the following two assumptions are made: (i) Qf⊂F and (ii) if the state reaches the set Qf, then the state stays within Qf. Since in this paper we focus on whether some failure has occurred in the past or not, these assumptions are imposed. These assumptions also imply that any failure is not restored automatically. Let Lf⊂L(G) denote the set of executions such that the state reaches some element in Qs.Next, the notion of diagnosability for the PDS (1) is defined according to [15, 26, 27].Definition 16.
For the PDS (1), suppose that the set of failure states Qf and the set of observable events Σo are given. Then the PDS (1) is diagnosable if the following condition holds:
(9)(∃n∈𝒩-{∞})(∀s∈Lf)(∀t∈L(G)s)|t|≥n⟹P-1P(st)∩L(G)⊆Lf,
where L(G)/s:={t∈Σ*∣st∈L(G)}, and P-1P(st) is the set of executions such that an observation is P(st).In this definition,P-1P(st)∩L(G)⊆Lf implies that all executions such that an observation is P(st) are included in Lf. So a failure can be detected from a finite observation. In other words, if there exists an unobservable infinite suffix, then the system is not diagnosable. Furthermore, deriving n in this definition is important, but this topic is not discussed in this paper. In [15], under some assumptions, a method for deriving n has been already discussed.Hereafter, a construction method of a diagnoser is not focused on (see [15] for construction of a diagnoser), and a method to test diagnosability is considered.


### 4.2. Existing Results

First, we introduce a necessary and sufficient condition of the PDS (1) not to be diagnosable [15, 28].Lemma 17.
For the PDS (1), suppose that the set of failure states Qf and the set of observable events Σo are given. Then the PDS is not diagnosable if and only if there exist two indistinguishable infinite executions w1 and w2 such that w1 reaches Qf while w2 does not.Next, the existing results [15] on diagnosability verification are introduced.Lemma 18.
Diagnosability of a DES-PDA is in general undecidable.Lemma 19.
Diagnosability of a DES-VPA is in general undecidable.These results can be obtained immediately, because the emptiness problem for an intersection of observations of infinite executionsw1 and w2 such that w1 reaches Qf while w2 does not is undecidable from Lemma 3.In [15], the following result has been derived.Lemma 20.
AssumeΣuo⊆Σint. Then diagnosability of a DES-VPA is decidable.In Lemma20, it is assumed that events corresponding to push and pop manipulations of the stack are observable. In [15], the diagnosability verification problem is reduced to the emptiness problem of Büchi automata under Σuo⊆Σint. So the property of pushdown automata is not considered. In this paper, as another approach, we consider diagnosability verification under other assumptions. Furthermore, approximate methods for verifying diagnosability of PDSs without assumptions are proposed.


### 4.3. Proposed Diagnosability Condition

First, based on Lemma4, we propose a diagnosability condition of PDSs.LetW1 denote the set of finite event sequences such that the state reaches Q-Qf. Let W2 denote the set of finite event sequences such that the state reaches Qf.Then we obtain the following result.Theorem 21.
Assume that eitherP(W1) or P(W2) is given as a language accepted by some finite automaton, that is, a regular language. Then diagnosability of a PDS is decidable. Furthermore, a PDS is not diagnosable if and only if P(W1)∩P(W2)≠∅ holds. In addition, this problem can be solved in PTIME.Proof.
From Lemma4 and Lemma 17, this theorem is obtained straightforwardly.We show a simple example.Example 22.
Consider the DES-VPA in Figure1 again. Suppose that Σo={a,b,c}, Σuo={d}, and Qf={q2} are given. Then we obtain
(10)W1=anbn,W2=amcdm,n≥1,m≥0,P(W1)=anbn,P(W2)=amc,n≥1,m≥0.
SinceP(W2) is a regular language, diagnosability of this DES-VPA is decidable. In fact, we see that P(W1)∩P(W2)≠∅ does not hold, and the defect can be detected by observing the event c. This example is very simple. However, we note that diagnosability of this system is undecidable in the case using the existing result in [15]. This is because this system does not satisfy the assumption in Lemma 20; that is, the unobservable event d is not an internal manipulation and is a pop manipulation.From this example, we can indicate that even ifW1, W2 are CFLs, then P(W1), P(W2) are generally neither CFLs nor regular languages. In the above example, W2 is a CFL, but P(W2) is a regular language. So we may consider to directly approximate P(W1), P(W2) by a regular language. From this viewpoint, we propose diagnosability conditions using the finite-state over/under-approximations.


### 4.4. Proposed Diagnosability Conditions Using Finite-State Approximations

Now, we show a diagnosability condition using a finite-state overapproximation in Definition8.Theorem 23.
Suppose that eitherP(W1) or P(W2) is approximated by a finite-state overapproximation in Definition 8. Let P¯1 and P¯2 denote approximated P(W1) and P(W2), respectively. Then a necessary condition for a PDS to be not diagnosable is that either P¯1∩P(W2)≠∅ or P(W1)∩P¯2≠∅ holds. In addition, this condition can be solved in PTIME.Proof.
From Theorem21, P(W1)⊆P¯1, and P(W2)⊆P¯2, we obtain the theorem immediately.Theorem23 provides a necessary condition.On the other hand, it is also important to obtain a sufficient condition. Then a finite-state underapproximation must be considered. A simple method to derive a finite-state underapproximation is that the length of the stack in a PDS is limited to a given finite length. See Example25 below for further details. So we assume that a finite-state under-approximation of either P(W1) or P(W2) is given.Then we obtain the following result.Theorem 24.
Suppose that eitherP(W1) or P(W2) is approximated by a finite-state under-approximation. Let P_1 and P_2 denote approximated P(W1) and P(W2), respectively. Then a sufficient condition for a PDS to be not diagnosable is that either P_1∩P(W2)≠∅ or P(W1)∩P_2≠∅ holds. In addition, this condition can be solved in PTIME.Proof.
From Theorem21, P_1⊆P(W1), and P_2⊆P(W2), we obtain the theorem immediately.From Theorems23 and 24, we see that diagnosability of a PDS can be approximately verified in PTIME. So Theorems 23 and 24 are simple but can be applied to several systems such as software systems.Example 25.
Suppose thatP(W1) and P(W2) are given as
(11)P(W1)={anbnci∣n≥1,i≥1},P(W2)={aibncn∣n≥1,i≥1},
respectively. Then P(W1)∩P(W2)={anbncn∣n≥1}≠∅ is obtained, and we see that this system is not diagnosable. However, P(W1)∩P(W2) is not a CFL (see [6] for further details).
Next, we verify diagnosability using Theorem23. In this example, we approximate P(W1) by a regular language. The PDA G1 accepting P(W1) is given by
(12)G1=(Q,Σ,Γ,Δ,q0,Z0,F),Q={q0,q1,q2},Σ={a,b,c},Γ={Z0,X},Δ=Δpush∪Δpop∪Δint,Δpush={(q0,a,X,q0),(q0,a,X,q1)},Δpop={(q1,b,q1,X)},Δint={(q1,c,q2),(q2,c,q2)},F={q2}⊂Q.
See also Figure2. Consider to derive the finite-state overapproximation in Definition 8. Then Σ.Q is given as
(13)Σ.Q={a·q0,a·q1,a·q2,b·q0,b·q1,b·q2,c·q0,c·q1,c·q2}.
Next, we deriveΔo. From Δpush, we obtain
(14)δ1=(q0,a·q0,q0),δ2=(q0,a·q1,q1).
FromΔpop, we obtain
(15)δ3=(q1,b.q1,q1).
FromΔint, we obtain
(16)δ4=(q1,c.q2,q2),δ5=(q2,c.q2,q2).
SoΔo={δ1,δ2,δ3,δ4,δ5} is obtained. Thus we can obtain the finite-state overapproximation G¯1 of the PDA G1 (see Figure 3). Using Σ={a,b,c}, the language accepted by G¯1 is obtained by
(17)L(G¯1)={a*ab*cc*}.
From the obtainedL(G¯1), we see that P(W1)⊆L(G¯1) holds. Furthermore, since L(G¯1)∩P(W2)≠∅ holds, the necessary condition in Theorem 23 is satisfied.Figure 2
PDAG1.Figure 3
Finite-state overapproximationG¯1 of G1.Next, we verify diagnosability using Theorem24. By limiting the length of the stack in P(W1) to n=2, the finite-state under-approximation P_1 can be obtained as
(18)P_1={aabbcc*}⊆P(W1).P
_
1 is accepted by the finite automaton in Figure 4. Since P_1∩P(W2)≠∅ holds, the sufficient condition in Theorem 24 is satisfied.Figure 4
Finite automaton acceptingP_1.


## 4.1. Definition of Diagnosability

First, failure states are defined. LetQf⊂Q denote the set of failure states. For Qf, the following two assumptions are made: (i) Qf⊂F and (ii) if the state reaches the set Qf, then the state stays within Qf. Since in this paper we focus on whether some failure has occurred in the past or not, these assumptions are imposed. These assumptions also imply that any failure is not restored automatically. Let Lf⊂L(G) denote the set of executions such that the state reaches some element in Qs.Next, the notion of diagnosability for the PDS (1) is defined according to [15, 26, 27].Definition 16.
For the PDS (1), suppose that the set of failure states Qf and the set of observable events Σo are given. Then the PDS (1) is diagnosable if the following condition holds:
(9)(∃n∈𝒩-{∞})(∀s∈Lf)(∀t∈L(G)s)|t|≥n⟹P-1P(st)∩L(G)⊆Lf,
where L(G)/s:={t∈Σ*∣st∈L(G)}, and P-1P(st) is the set of executions such that an observation is P(st).In this definition,P-1P(st)∩L(G)⊆Lf implies that all executions such that an observation is P(st) are included in Lf. So a failure can be detected from a finite observation. In other words, if there exists an unobservable infinite suffix, then the system is not diagnosable. Furthermore, deriving n in this definition is important, but this topic is not discussed in this paper. In [15], under some assumptions, a method for deriving n has been already discussed.Hereafter, a construction method of a diagnoser is not focused on (see [15] for construction of a diagnoser), and a method to test diagnosability is considered.


## 4.2. Existing Results

First, we introduce a necessary and sufficient condition of the PDS (1) not to be diagnosable [15, 28].Lemma 17.
For the PDS (1), suppose that the set of failure states Qf and the set of observable events Σo are given. Then the PDS is not diagnosable if and only if there exist two indistinguishable infinite executions w1 and w2 such that w1 reaches Qf while w2 does not.Next, the existing results [15] on diagnosability verification are introduced.Lemma 18.
Diagnosability of a DES-PDA is in general undecidable.Lemma 19.
Diagnosability of a DES-VPA is in general undecidable.These results can be obtained immediately, because the emptiness problem for an intersection of observations of infinite executionsw1 and w2 such that w1 reaches Qf while w2 does not is undecidable from Lemma 3.In [15], the following result has been derived.Lemma 20.
AssumeΣuo⊆Σint. Then diagnosability of a DES-VPA is decidable.In Lemma20, it is assumed that events corresponding to push and pop manipulations of the stack are observable. In [15], the diagnosability verification problem is reduced to the emptiness problem of Büchi automata under Σuo⊆Σint. So the property of pushdown automata is not considered. In this paper, as another approach, we consider diagnosability verification under other assumptions. Furthermore, approximate methods for verifying diagnosability of PDSs without assumptions are proposed.


## 4.3. Proposed Diagnosability Condition

First, based on Lemma4, we propose a diagnosability condition of PDSs.LetW1 denote the set of finite event sequences such that the state reaches Q-Qf. Let W2 denote the set of finite event sequences such that the state reaches Qf.Then we obtain the following result.Theorem 21.
Assume that eitherP(W1) or P(W2) is given as a language accepted by some finite automaton, that is, a regular language. Then diagnosability of a PDS is decidable. Furthermore, a PDS is not diagnosable if and only if P(W1)∩P(W2)≠∅ holds. In addition, this problem can be solved in PTIME.Proof.
From Lemma4 and Lemma 17, this theorem is obtained straightforwardly.We show a simple example.Example 22.
Consider the DES-VPA in Figure1 again. Suppose that Σo={a,b,c}, Σuo={d}, and Qf={q2} are given. Then we obtain
(10)W1=anbn,W2=amcdm,n≥1,m≥0,P(W1)=anbn,P(W2)=amc,n≥1,m≥0.
SinceP(W2) is a regular language, diagnosability of this DES-VPA is decidable. In fact, we see that P(W1)∩P(W2)≠∅ does not hold, and the defect can be detected by observing the event c. This example is very simple. However, we note that diagnosability of this system is undecidable in the case using the existing result in [15]. This is because this system does not satisfy the assumption in Lemma 20; that is, the unobservable event d is not an internal manipulation and is a pop manipulation.From this example, we can indicate that even ifW1, W2 are CFLs, then P(W1), P(W2) are generally neither CFLs nor regular languages. In the above example, W2 is a CFL, but P(W2) is a regular language. So we may consider to directly approximate P(W1), P(W2) by a regular language. From this viewpoint, we propose diagnosability conditions using the finite-state over/under-approximations.


## 4.4. Proposed Diagnosability Conditions Using Finite-State Approximations

Now, we show a diagnosability condition using a finite-state overapproximation in Definition8.Theorem 23.
Suppose that eitherP(W1) or P(W2) is approximated by a finite-state overapproximation in Definition 8. Let P¯1 and P¯2 denote approximated P(W1) and P(W2), respectively. Then a necessary condition for a PDS to be not diagnosable is that either P¯1∩P(W2)≠∅ or P(W1)∩P¯2≠∅ holds. In addition, this condition can be solved in PTIME.Proof.
From Theorem21, P(W1)⊆P¯1, and P(W2)⊆P¯2, we obtain the theorem immediately.Theorem23 provides a necessary condition.On the other hand, it is also important to obtain a sufficient condition. Then a finite-state underapproximation must be considered. A simple method to derive a finite-state underapproximation is that the length of the stack in a PDS is limited to a given finite length. See Example25 below for further details. So we assume that a finite-state under-approximation of either P(W1) or P(W2) is given.Then we obtain the following result.Theorem 24.
Suppose that eitherP(W1) or P(W2) is approximated by a finite-state under-approximation. Let P_1 and P_2 denote approximated P(W1) and P(W2), respectively. Then a sufficient condition for a PDS to be not diagnosable is that either P_1∩P(W2)≠∅ or P(W1)∩P_2≠∅ holds. In addition, this condition can be solved in PTIME.Proof.
From Theorem21, P_1⊆P(W1), and P_2⊆P(W2), we obtain the theorem immediately.From Theorems23 and 24, we see that diagnosability of a PDS can be approximately verified in PTIME. So Theorems 23 and 24 are simple but can be applied to several systems such as software systems.Example 25.
Suppose thatP(W1) and P(W2) are given as
(11)P(W1)={anbnci∣n≥1,i≥1},P(W2)={aibncn∣n≥1,i≥1},
respectively. Then P(W1)∩P(W2)={anbncn∣n≥1}≠∅ is obtained, and we see that this system is not diagnosable. However, P(W1)∩P(W2) is not a CFL (see [6] for further details).
Next, we verify diagnosability using Theorem23. In this example, we approximate P(W1) by a regular language. The PDA G1 accepting P(W1) is given by
(12)G1=(Q,Σ,Γ,Δ,q0,Z0,F),Q={q0,q1,q2},Σ={a,b,c},Γ={Z0,X},Δ=Δpush∪Δpop∪Δint,Δpush={(q0,a,X,q0),(q0,a,X,q1)},Δpop={(q1,b,q1,X)},Δint={(q1,c,q2),(q2,c,q2)},F={q2}⊂Q.
See also Figure2. Consider to derive the finite-state overapproximation in Definition 8. Then Σ.Q is given as
(13)Σ.Q={a·q0,a·q1,a·q2,b·q0,b·q1,b·q2,c·q0,c·q1,c·q2}.
Next, we deriveΔo. From Δpush, we obtain
(14)δ1=(q0,a·q0,q0),δ2=(q0,a·q1,q1).
FromΔpop, we obtain
(15)δ3=(q1,b.q1,q1).
FromΔint, we obtain
(16)δ4=(q1,c.q2,q2),δ5=(q2,c.q2,q2).
SoΔo={δ1,δ2,δ3,δ4,δ5} is obtained. Thus we can obtain the finite-state overapproximation G¯1 of the PDA G1 (see Figure 3). Using Σ={a,b,c}, the language accepted by G¯1 is obtained by
(17)L(G¯1)={a*ab*cc*}.
From the obtainedL(G¯1), we see that P(W1)⊆L(G¯1) holds. Furthermore, since L(G¯1)∩P(W2)≠∅ holds, the necessary condition in Theorem 23 is satisfied.Figure 2
PDAG1.Figure 3
Finite-state overapproximationG¯1 of G1.Next, we verify diagnosability using Theorem24. By limiting the length of the stack in P(W1) to n=2, the finite-state under-approximation P_1 can be obtained as
(18)P_1={aabbcc*}⊆P(W1).P
_
1 is accepted by the finite automaton in Figure 4. Since P_1∩P(W2)≠∅ holds, the sufficient condition in Theorem 24 is satisfied.Figure 4
Finite automaton acceptingP_1.


## 5. Discussions

### 5.1. Relationship between Opacity and Diagnosability Verifications

Opacity and diagnosability are closely related concepts. We can interpret that opacity is the converse notion of diagnosability. However, decidability conditions are different.In opacity verification, ifP(V1) and P(V2) are languages accepted by some VPA, respectively, then opacity is decidable (see also Theorem 13). That is, opacity can be discussed only in the framework of VPAs.On the other hand, in diagnosability verification, if eitherP(W1) or P(W2) is a language accepted by some finite automaton, then diagnosability is decidable (see Section 4.3). Thus approximations such as finite-state approximations described in Section 2.3 are required.From these results, the difference between opacity verification and diagnosability verification is clarified from the theoretical viewpoint. However, it is known that the computational complexity of the inclusion problem of VPAs is EXPTIME-complete and that of finite automata is PSPACE-complete [7]. Thus, from the computational viewpoint, it may be desirable to use finite-state approximations in opacity verification.


### 5.2. Optimal Sensor Selection

The optimal sensor selection problem, that is, the problem of minimizing the number of sensors which observe events, such that the system is diagnosable has been discussed in [29, 30]. Further, in opacity, the sensor selection problem has been discussed in [18]. One of the trivial solutions to the sensor selection problem in opacity is that the number of sensors should be zero, but this is not practical. So it is important to consider the optimal sensor selection problem such that the system is opaque and diagnosable simultaneously under Qs≠Qf. Then we can derive an optimal solution of this problem according to the results in Sections 4 and 3. This is one of the challenges to be undertaken in the future, that is, to develop an efficient algorithm.


### 5.3. Extension to Higher-Order Pushdown Systems

Higher-order pushdown automata (HPAs) [31, 32] have been proposed as one of the extensions of PDAs. HPAs are defined by using higher-order stacks, that is, a nested “stack of stacks” structures. HPAs are closely related to infinite graph theory and higher-order logic programming. Decidable problems and undecidable problems in HPAs are basically similar to those in PDAs. Thus our proposed approach will be applied to HPAs. In fact, the conditions that diagnosability of discrete event systems modeled by HPAs is decidable have been obtained in [15]. Since one of the conditions is Σuo⊆Σint, the conditions obtained can be regarded as a natural extension of Lemma 20.


## 5.1. Relationship between Opacity and Diagnosability Verifications

Opacity and diagnosability are closely related concepts. We can interpret that opacity is the converse notion of diagnosability. However, decidability conditions are different.In opacity verification, ifP(V1) and P(V2) are languages accepted by some VPA, respectively, then opacity is decidable (see also Theorem 13). That is, opacity can be discussed only in the framework of VPAs.On the other hand, in diagnosability verification, if eitherP(W1) or P(W2) is a language accepted by some finite automaton, then diagnosability is decidable (see Section 4.3). Thus approximations such as finite-state approximations described in Section 2.3 are required.From these results, the difference between opacity verification and diagnosability verification is clarified from the theoretical viewpoint. However, it is known that the computational complexity of the inclusion problem of VPAs is EXPTIME-complete and that of finite automata is PSPACE-complete [7]. Thus, from the computational viewpoint, it may be desirable to use finite-state approximations in opacity verification.


## 5.2. Optimal Sensor Selection

The optimal sensor selection problem, that is, the problem of minimizing the number of sensors which observe events, such that the system is diagnosable has been discussed in [29, 30]. Further, in opacity, the sensor selection problem has been discussed in [18]. One of the trivial solutions to the sensor selection problem in opacity is that the number of sensors should be zero, but this is not practical. So it is important to consider the optimal sensor selection problem such that the system is opaque and diagnosable simultaneously under Qs≠Qf. Then we can derive an optimal solution of this problem according to the results in Sections 4 and 3. This is one of the challenges to be undertaken in the future, that is, to develop an efficient algorithm.


## 5.3. Extension to Higher-Order Pushdown Systems

Higher-order pushdown automata (HPAs) [31, 32] have been proposed as one of the extensions of PDAs. HPAs are defined by using higher-order stacks, that is, a nested “stack of stacks” structures. HPAs are closely related to infinite graph theory and higher-order logic programming. Decidable problems and undecidable problems in HPAs are basically similar to those in PDAs. Thus our proposed approach will be applied to HPAs. In fact, the conditions that diagnosability of discrete event systems modeled by HPAs is decidable have been obtained in [15]. Since one of the conditions is Σuo⊆Σint, the conditions obtained can be regarded as a natural extension of Lemma 20.


## 6. Application to XML Data Integration

In this section, we consider XML data integration as an application. The XML (Extensible Markup Language) is a markup language that defines a set of rules for encoding data and documents and is widely used in several fields such as data and documents on the Web and medical databases. In cases where documents in databases are expressed by the XML, one of the important problems is data integration, which is called here XML data integration. In XML data integration, first, XML documents are extracted from multiple databases. Next, the extracted XML documents are integrated as one XML document. Here, we assume the existence of a database where the integrated XML document is indistinguishable from its extracted components. The XML document in such a database is called here the target XML document. Then we consider the following problems:Problem 1.
Suppose that an integrated XML document and a target XML document are given. Then(i)
can the integrated XML document be indistinguishable from the target XML document?(ii)
by masking particular data in the integrated XML document, can the integrated XML document be indistinguishable from the target XML document?
These problems are important from the viewpoint of security. In addition, this problem is closely related to opacity verification of PDSs in Section3. This is because in recent years, a method for expressing XML documents as a VPA has been studied in, for example, [8, 13].Hereafter, the relation between VPAs and XML documents will be explained. Next, by using a simple example, we explain how to solve the above problems.


### 6.1. Relation between Pushdown Systems and XML Documents

First, an example of XML documents expressing information about books is shown as follows:<book><title>IntroductiontoDiscreteEventSystems</title><author> C. G. Cassandras </author><author> S. Lafortune </author><ISBN> 978-0-387-33332-8 </ISBN></book>The XML scheme in the above example is based on the example in [13]. In addition, the above example implies information about the book of [1].  <book>,  <title>,  <author>, and  <ISBN> are open tags.  </book>,  </title>,  </author>, and  </ISBN> are close tags. Actual data such as “978-0-387-33332-8” is called a local symbol. Since in this paper we focus on XML schemas, we omit local symbols. The above XML document can then be expressed as the VPA S1=(Q,Σ,Γ,Δpush∪Δpop∪Δint,q0,Z0,F), where
(19)Q={q0,q1,q2,q3,q4,q5,q6,q7,q8},Σ={book,book¯,title,title¯,author,author¯,isbn,isbn¯},Γ={Z0,a,b,i,t},Δpush={(q0,book,b,q1),(q1,title,t,q2),(q3,author,a,q4),(q5,author,a,q4),(q5,isbn,i,q6)},Δpop={(q2,title¯,q3,t),(q4,author¯,q5,a),(q6,isbn¯,q7,i),(q7,isbn¯,q8,b)},Δint=∅,F={q8}⊂Q.Close tags are expressed by·¯. See also Figure 5. Thus a given XML document can be expressed by a VPA.Figure 5
VPAS1 expressing the XML document (information about books).


### 6.2. XML Data Integration with Security Considerations

Next, suppose that a VPA expressing information about publishers is given asS2 in Figure 6, where pub, pname, and addr imply “publisher,” “publisher name,” and “address,” respectively. Consider how to integrate the VPA S1 with the VPA S2. One of the simple methods is to connect S1 with S2 in series. Then we can obtain the VPA S3 in Figure 7.Figure 6
VPAS2 expressing information about publishers.Figure 7
VPAS3 obtained by integrating S1 with S2.Here, suppose that a target XML document is given as the VPA in Figure8, where “#” implies a wild-card event or a wild-card stack symbol. We consider Problem 1 (i). That is, we must check if L(S3)⊆L(T) is satisfied. This is the same as opacity verification. In this example, L(S3)⊆L(T) is not satisfied, because by observing “country,” the VPA S3 is distinguishable from the VPA T. Therefore, a solution of Problem 1 (i) is “no.” In other words, the integrated XML document is not opaque. From Theorem 13, it is assumed that this problem is decidable in general cases. We remark that in this case, Σ=Σo holds.Figure 8
VPAT expressing a target XML document.Next, consider Problem1 (ii). Suppose that the set of unobservable events Σuo is given as Σuo={country}. Then the VPA S3 is indistinguishable from the VPA T. Therefore, a solution of Problem 1 (i) is “yes.” In other words, we can say that the integrated XML document becomes opaque by masking “country.” Also in general cases, this problem is decidable. On the other hand, it is one part of the future work, that is, to develop an efficient algorithm for finding masked events. Since this problem is the converse notion of the optimal sensor selection problem for diagnosability, there is a possibility that the existing result on sensor selection can be applied.


## 6.1. Relation between Pushdown Systems and XML Documents

First, an example of XML documents expressing information about books is shown as follows:<book><title>IntroductiontoDiscreteEventSystems</title><author> C. G. Cassandras </author><author> S. Lafortune </author><ISBN> 978-0-387-33332-8 </ISBN></book>The XML scheme in the above example is based on the example in [13]. In addition, the above example implies information about the book of [1].  <book>,  <title>,  <author>, and  <ISBN> are open tags.  </book>,  </title>,  </author>, and  </ISBN> are close tags. Actual data such as “978-0-387-33332-8” is called a local symbol. Since in this paper we focus on XML schemas, we omit local symbols. The above XML document can then be expressed as the VPA S1=(Q,Σ,Γ,Δpush∪Δpop∪Δint,q0,Z0,F), where
(19)Q={q0,q1,q2,q3,q4,q5,q6,q7,q8},Σ={book,book¯,title,title¯,author,author¯,isbn,isbn¯},Γ={Z0,a,b,i,t},Δpush={(q0,book,b,q1),(q1,title,t,q2),(q3,author,a,q4),(q5,author,a,q4),(q5,isbn,i,q6)},Δpop={(q2,title¯,q3,t),(q4,author¯,q5,a),(q6,isbn¯,q7,i),(q7,isbn¯,q8,b)},Δint=∅,F={q8}⊂Q.Close tags are expressed by·¯. See also Figure 5. Thus a given XML document can be expressed by a VPA.Figure 5
VPAS1 expressing the XML document (information about books).


## 6.2. XML Data Integration with Security Considerations

Next, suppose that a VPA expressing information about publishers is given asS2 in Figure 6, where pub, pname, and addr imply “publisher,” “publisher name,” and “address,” respectively. Consider how to integrate the VPA S1 with the VPA S2. One of the simple methods is to connect S1 with S2 in series. Then we can obtain the VPA S3 in Figure 7.Figure 6
VPAS2 expressing information about publishers.Figure 7
VPAS3 obtained by integrating S1 with S2.Here, suppose that a target XML document is given as the VPA in Figure8, where “#” implies a wild-card event or a wild-card stack symbol. We consider Problem 1 (i). That is, we must check if L(S3)⊆L(T) is satisfied. This is the same as opacity verification. In this example, L(S3)⊆L(T) is not satisfied, because by observing “country,” the VPA S3 is distinguishable from the VPA T. Therefore, a solution of Problem 1 (i) is “no.” In other words, the integrated XML document is not opaque. From Theorem 13, it is assumed that this problem is decidable in general cases. We remark that in this case, Σ=Σo holds.Figure 8
VPAT expressing a target XML document.Next, consider Problem1 (ii). Suppose that the set of unobservable events Σuo is given as Σuo={country}. Then the VPA S3 is indistinguishable from the VPA T. Therefore, a solution of Problem 1 (i) is “yes.” In other words, we can say that the integrated XML document becomes opaque by masking “country.” Also in general cases, this problem is decidable. On the other hand, it is one part of the future work, that is, to develop an efficient algorithm for finding masked events. Since this problem is the converse notion of the optimal sensor selection problem for diagnosability, there is a possibility that the existing result on sensor selection can be applied.


## 7. Conclusion and Future Work

In this paper, opacity and diagnosability of discrete event systems expressed by pushdown automata (called here pushdown systems, PDSs) have been discussed based on formal language theory. In opacity verification, we have not only proven that opacity of a PDS is in general undecidable, but also characterized the condition such that opacity is decidable. We have also clarified that depending on a class of observations, the computational complexity is different. In diagnosability verification, we have proposed a new diagnosability condition, based on the fact that an intersection of a context-free language and a regular language is derived as a context-free language. In addition, we have derived diagnosability conditions using finite-state over/under-approximations of observations. Also we have clarified that the proposed diagnosability conditions can be solved in PTIME. In particular, since diagnosability conditions using approximations can be applied to a general class of PDSs and can be efficiently solved, several applications will be able to be considered. Finally, as an application, we have considered XML data integration. The obtained result is valuable as the basis of verification of PDSs and will be the first step toward development of control theory for infinite-state discrete event systems.In future work, there are many open problems, for example, implementation using a model checker and decentralized diagnosis [33]. In addition, the result on diagnosability analysis of unbounded Petri nets has been obtained in [4]. Also, for recursive tile systems, which are a class of infinite discrete event systems, the result on opacity and diagnosability has been obtained in [34]. It is important to clarify the relation between our result and these results. Finally, in order to show the effectiveness of our proposed method, it is important to consider several applications.



---

*Source: 654059-2013-05-22.xml*