JAIST Repository
https://dspace.jaist.ac.jp/Title

Visibly Stack AutomataAuthor(s)Nguyen, Van Tang; Ogawa, Mizuhito

CitationIssue Date

2006‑11‑27

TypePresentation

Text version

publisher

URL

http://hdl.handle.net/10119/8312

RightsDescription

3rd VERITE : JAIST/TRUST‑AIST/CVS joint workshop
on VERIfication TEchnologyでの発表資料, 開催：2006年11月27日〜28日, 開催場所：JAIST 知識科学
研究科講義棟・中講義室

Japan Advanced Institute of Science and Technology

Visibly Stack Automata

Nguyen Van Tang - Mizuhito Ogawa
School of Information Science
Japan Advanced Institute of Science and Technology1

Talk Outline
 Automata-theoretic based verification¾ Checking context-free specifications¾ Obstacles

Visibly Pushdown Automata¾ Visibly Pushdown Languages¾ Determinization

Visibly Stack Automata¾ Visibly Stack Languages¾ Determinization2

Automata-theoretic based verificationTo verify if a software system satisfies aregular specification
System is modeled as a pushdown automaton MRequirement is specified as a finite automaton S

M |= S iff:
 L(M) ⊆ L(S)L(M)∩L(S)C = ∅Model checking problems are reduced todecision problems of formal languages
Model checker: SPIN, MAGIC,..
3

Checking Context-free Specifications
 When S is a context-free specification
 Checking M|= S becomes undecidable
 Obstacles¾ Context-free languages (CFL) are not closed underintersection, complementation¾ The inclusion problem of CFL is undecidable

 Goals: Find a class of non-regular languages¾ Enjoys closure properties, Inclusion problem is decidable¾ Robustness4

Talk Outline
 Automata-theoretic based verification¾ Checking context-free specifications¾ Obstacles

Visibly Pushdown Automata¾ Visibly Pushdown Languages¾ Determinization

Visibly Stack Automata¾ Visibly Stack Languages¾ Determinization

5

Pushdown Automata (PDA) Def. PDA (P,Σ,Γ,Δ,p0,Z0,F) where•
•
•••
•
•

P : finite control locations
Γ: finite stack alphabet
Σ: finite input alphabet
Δ⊆(P×Γ×(Σ∪{ε})×(P×Γ*)) : transition
p0 : initial control location
Z0: initial stack symbolF⊆P :final control locations

 Accepted ⇔ run reaches some control location in F PDA are not determinizable. PDA are closed under union, but
6not closed under intersection, complementation

Visibly Pushdown Automata (VPA) VPA was introduced by J. Alur and P.Madhusudan in
2004, [p.202-211, ACM-STOC’s 04]
 Pushdown alphabet: partitioned into 3 disjoint setsΣ = Σpush ∪ Σpop ∪ Σlocal
 A visibly pushdown automaton over a pushdownalphabet Σ is a pushdown automaton that
¾ pushes a symbol onto the stack on a symbol in Σpush¾ pops the stack on a symbol in Σpop
¾ cannot change the stack on a symbol in Σlocal
Key:Stack size at any time is determined by the input word
but not control state or stack content

7Visibly Pushdown Languages (VPL) A language L is a VPL over a pushdown alphabet Σ, if
it is recognized by a VPA
 Examples¾ L = { anbn | n ≥ 1, a ∈ Σpush, b ∈ Σpop }¾ Every regular language L is a VPL

 VPLs are closed under:¾ Union:¾ Intersection: Product construction works !
¾ Complementation (see later)
α2M1

α1⊥

M2

γ2(α2, γ2)γ1(α1, γ1)

⊥M

⊥

8

Decision Problems
 Given a nondeterministic A (n states), construct anequivalent deterministic B in size O(2n^2).
 Emptiness: Decidable in polynomial-time (cubic)
 Language inclusion: L(A) ⊆ L(B) ?
¾ Determinize B, take its complement, take product with A,
and test for emptiness¾ Exponential-time complete

 VPLs is a subclass of DCFLs (languages defined bydeterministic PDAs)¾ DCFLs not closed under union, intersection¾ Equivalence problem for DCFLs decidable, but complex
9Determinization: Key ideas
 Def. A word u is well-matched if– For each prefix u’ of u, the number of Σpush symbols
in u’ is at most the number of Σpop symbols in u’.
– For each suffix u” of u, the number of Σpop symbols
in u” is at most the number of Σpush symbols in u”.
Push and Pop thesame symbola1…………..

w1

………..

……..

…

ω =

Unreachable states

w2

a2

10

Determinization: Sketch of the construction
 Idea: a well-matched word preserves stack; thus
regarded as internal transition (expressed assummaries Si ). Transitions by extra Σpush symbols
are postponed until corresponding Σpop symbols
will be read.
 Determinized VPA will consist of :– Control locations : { (S,R) | S: summary, R: reachables}– Stack alphabet : { (S,R,a) | S, R; a∈Σpush}– The initial state (Id, Pinit ), where Id = {(q,q)| q∈ P}– Final states { (S,R) | R∩F≠φ},– where• R (⊆ P)= { all states reachable after a word w }• S (⊆ P×P) = { all summaries on a well-marched word w }(i.e., (q,q’) ∈ S, if (q,⊥) can reach to (q’,⊥)).
11Determinization: Sketch of transitions
 Let w = w1c1w2c2…cnwn+1, where ci’s are in Σpush ,,wi’s are well matched words, let a be the next input.
– Stack is (Sn,Rn,cn)….(S1,R1,c1)⊥– Control location is (Sn+1,Rn+1),– If a∈Σlocal : (Sn+1,Rn+1) is combined with transitions by a.
– If a∈Σpush: push (Sn+1,Rn+1,cn+1) and control location is (id,{ q’ | reachable from q∈Rn+1 by a})– If a∈Σpop : let Update be combination of transitions by cn(push γ∈Γ), Sn+1, and transitions by a (pop same γ).
NewS is Sn combined with Update, and NewR is Rn
combined with Update (Rn+1 is discarded).
– where– Ri (⊆ P) = Set of all states reachable after w1c1…wi– Si (⊆ P×P) = Set of all summaries on wi
12

Talk Outline
 Automata-theoretic based verification¾ Checking context-free specifications¾ Obstacles

 Visibly Pushdown Automata¾ Visibly Pushdown Languages¾ Determinization

 Visibly Stack Automata¾ Visibly Stack Languages¾ Determinization

13

Stack Automata
 Stack automata: introduced by Ginsburg, Greibachand Harrison [JACM, No 2, Vol 14, pp.389-418, 1967]
 Stack automata = PDA + “read inside stack”.
 More powerful than PDA. For instance, {anbncn|n≥ 1}, {anbn^2|n≥1}
 Def. Stack alphabet: ∑ = ∑push∪∑pop∪ ∑local∪ ∑up∪∑down

14

Visibly Stack Automata (VSA) (1/2)
Def. A VSA A over stack alphabet ∑: A = 〈P,Pin, Γ, ↑, δ, F〉• P : finite set of control locations•Pin⊆ P: set of initial control locations•
Γ : finite stack alphabet, special symbols ⊥, T•↑ : stack pointer•F ⊆ P : set of final control locations•δ is a set of transitions 〈δpuah, δpop, δlocal, δup, δdown〉,
δpush ⊆ P×Σpush×P× Γ\{⊥,T}; δpop ⊆ P×Σpop×Γ×P;
δlocal ⊆P×Σlocal×P ;δdown ⊆ P×Σdown×Γ×P; δup ⊆ P×Σup×Γ×P;


(q,a,γ,q’)∈ δup (γ≠⊥,T) ⇔ (q,a,γ’,q’)∈ δup (γ’≠ γ, ⊥,T)
15(q,a,γ,q’)∈ δdown (γ≠⊥,T) ⇔ (q,a,γ’,q’)∈ δdown (γ’≠ γ, ⊥,T)

Visibly Stack Automata (2/2)
 Properties:¾ Stack has form Tγn…γi↑γi-1…γ1⊥¾ VSA can only push, pop when stack pointer at the top¾ When stack is empty, pop is read but not popped¾ Stack pointer cannot go beyond T or below ⊥¾ When pointer is reading ⊥ (T), down (up) is read butpointer does not move down (up) Def. A language L is a visibly stack language(VSL) if it is accepted by a VSA.
 Example: L={anbncn|n≥1, a∈∑push,b∈∑d,c∈∑u} VSL class is a proper extension of VPL class16

Closure properties & Decision problems
 Similar to VPLs, VSLs are closed under:¾ Union, intersection, complementation¾ Determinizable (more complicated, see later) Emptiness for stack automata is decidable!
D. Harel, Information and Computation, Vol.113, No.2, 278-299, 1994

 Inclusion problem is decidable for visibly stacklanguages.
17Determinization: Key ideas
 Matching condition between push and pop symbols
 Read the same symbol, whenever pointer goes up,
or goes down at the same position
Up and down, at samePush and Pop theposition, read same symbol
same symbol

Unreachable states
Unreachable states…………..
…………..

……

……..
……..

………..
………..

T
γ3
γ2γ1

ω =
ω =w1
w1

da1

w2
w2

u
a218

⊥

Determinization: Some definitions
Def. A word u is an up-down segment if:
1.
2.
3.



For each prefix u’ of u, the number of Σdown symbols in u’ isat most the number of Σup symbols in u’.
For each suffix u” of u, the number of Σup symbols in u” is at
most the number of Σdown symbols in u”.
There is no push, pop symbols in uDef. A word u is well-matched if:
1.
2.
3.

For each prefix u’ of u, the number of Σpush symbols in u’ is at
most the number of Σpop symbols in u’.
For each suffix u” of u, the number of Σpop symbols in u” is at
most the number of Σpush symbols in u”.
For each up (down) symbol a of u, a must belongs to an updown segment ud, ud is a subword of u.
19

Determinization: Sketch of the construction
 Determinized VSA will consist of :

¾ Control locations : { (S,R) | S: summary, R:reachables}¾ Stack alphabet : { (S,R,a) | S, R; a∈Σpush}¾ The initial state (Id,Pinit), where Id = {(q,q)| q∈ P}¾ Final states { (S,R) | R∩F≠φ},– where– R (⊆ P) = {all states reachable after a word w}– S (⊆ P×P) = {all summaries on a well-marched word w}(i.e., (q,q’) ∈ S, if (q,T↑⊥) can reach to (q’,T↑⊥)).
20

Determinization: Sketch of transitions
 Let w = w1c1w2c2…cnwn+1, where ci’s are in Σpush,, wi’s
are well matched words, let a be the next input.
– Stack is T ↑(Sn,Rn,cn)…(S1,R1,c1)⊥– Control location is (Sn+1,Rn+1),– If a∈Σlocal : (Sn+1,Rn+1) is updated using subset
construction with transitions by a.
– If a ∈Σdown: (Sn+1,Rn+1) is updated with transition by
a. Stack now is T(Sn,Rn,cn)↑…(S1,R1,c1)⊥– If a ∈Σup: (Sn+1,Rn+1) is updated with transitions bya, the pointer cannot go up. Stack stays unchanged,T ↑(Sn,Rn,cn)…(S1,R1,c1)⊥– where– Ri (⊆ P) = Set of all states reachable after w1c1…wi– Si (⊆ P×P) = Set of all summaries on wi21

Determinization: Sketch of transitions
 If a∈Σpush: push (Sn+1,Rn+1,cn+1) and control location is(id, { q’ | reachable from q∈Rn+1 by a}). Stack now isT ↑(Sn+1,Rn+1,cn+1)(Sn,Rn,cn)…(S1,R1,c1)⊥
 If a∈Σpop: let Update be combination of transitions bycn (push γ ∈Γ), Sn+1, and transitions by a (pop sameγ). NewS is Sn combined with Update, and NewR is Rncombined with Update (Rn+1 is discarded). Stack nowis T ↑(Sn-1,Rn-1,cn-1)…(S1,R1,c1)⊥– where– Ri (⊆ P) = Set of all states reachable after w1c1…wi– Si (⊆ P×P) = Set of all summaries on wi22

Conclusion Proposed the class of visibly stack languages
recognized by visibly stack automata
 To our knowledge, to date, VSLs is the largest classwhich enjoys closure properties. All the decision
problems are decidable for VSA.
 Infinite words:¾ Visibly Büchi pushdown automata [AM04]¾ Visibly Büchi stack automata¾ Closure properties, not determinizable, but language
inclusion is still decidable!

23Thank for your attention !

24