Reachability analysis of first-order definable pushdown systems
Lorenzo Clemente and Sławomir Lasota
University of Warsaw
Prague, September 2015
At a glance
Model: First-order definable pushdown automata (infinite data domain).
Problem: Reachability analysis.
Solution: Saturation technique in a logical form.
Complexity varies from EXPTIME to undecidable,�depending on the data domain.
At a glance
Model: First-order definable pushdown automata (infinite data domain).
Problem: Reachability analysis.
Solution: Saturation technique in a logical form.
Complexity varies from EXPTIME to undecidable,�depending on the data domain.
Part of an ongoing effort aiming at generalizing automata theory with atoms.
Builds on previous work by Bojańczyk, Klin, Lasota, Ochremiak, Toruńczyk.
Atoms
Fix a logical structure (𝔸, 𝑅1, …, 𝑅j) called atoms.
Atoms
Fix a logical structure (𝔸, 𝑅1, …, 𝑅j) called atoms.
Sets with atoms: Built from ∅, {, }, and elements of 𝔸.
Pushdown automata
Classical pushdown automaton〈Σ,𝛤,𝑃,𝜌〉
push ⊆ 𝑃⨉𝛤⨉Σ⨉𝑃⨉𝛤⨉𝛤
push(𝑝,𝛼,𝑎,𝑞,𝛽,𝛾) = “at location 𝑝 pop 𝛼, read 𝑎, go to loc. 𝑞, and push 𝛽𝛾”
pop ⊆ 𝑃⨉𝛤⨉Σ⨉𝑃
pop(𝑝,𝛼,𝑎,𝑞) = “at location 𝑝 pop 𝛼, read 𝑎, and go to location 𝑞”
Pushdown automata
Fix atoms 𝔸. First-order definable pushdown automaton〈Σ,𝛤,𝑃,𝜌〉over 𝔸:
push is a first-order definable subset of 𝑃⨉𝛤⨉Σ⨉𝑃⨉𝛤⨉𝛤
push(𝑝,𝛼,𝑎,𝑞,𝛽,𝛾) = “at location 𝑝 pop 𝛼, read 𝑎, go to loc. 𝑞, and push 𝛽𝛾”
pop is a first-order definable subset of 𝑃⨉𝛤⨉Σ⨉𝑃
pop(𝑝,𝛼,𝑎,𝑞) = “at location 𝑝 pop 𝛼, read 𝑎, and go to location 𝑞”
Pushdown automata
Fix atoms 𝔸. First-order definable pushdown automaton〈Σ,𝛤,𝑃,𝜌〉over 𝔸:
push is a first-order definable subset of 𝑃⨉𝛤⨉Σ⨉𝑃⨉𝛤⨉𝛤
push(𝑝,𝛼,𝑎,𝑞,𝛽,𝛾) = “at location 𝑝 pop 𝛼, read 𝑎, go to loc. 𝑞, and push 𝛽𝛾”
pop is a first-order definable subset of 𝑃⨉𝛤⨉Σ⨉𝑃
pop(𝑝,𝛼,𝑎,𝑞) = “at location 𝑝 pop 𝛼, read 𝑎, and go to location 𝑞”
infinite in two dimensions:�stack + data
Pushdown automata
Fix atoms 𝔸. First-order definable pushdown automaton〈Σ,𝛤,𝑃,𝜌〉over 𝔸:
push is a first-order definable subset of 𝑃⨉𝛤⨉Σ⨉𝑃⨉𝛤⨉𝛤
push(𝑝,𝛼,𝑎,𝑞,𝛽,𝛾) = “at location 𝑝 pop 𝛼, read 𝑎, go to loc. 𝑞, and push 𝛽𝛾”
pop is a first-order definable subset of 𝑃⨉𝛤⨉Σ⨉𝑃
pop(𝑝,𝛼,𝑎,𝑞) = “at location 𝑝 pop 𝛼, read 𝑎, and go to location 𝑞”
infinite in two dimensions:�stack + data
Related to register and timed automata,�where the components are quantifier-free definable.
Example
Take equality atoms (𝔸,=). Palindromes:
𝐿 = { 𝑎_0...𝑎_2𝑛 ϵ 𝔸* | ∀(0 ≤ 𝑖 ≤ 𝑛) · 𝑎_𝑖 = 𝑎_(2𝑛 − 𝑖) }
Recognized by〈Σ = 𝔸, 𝛤 = 𝔸, 𝑃 = {𝑝, 𝑞}, 𝜌 = push ∪ pop〉with
push(𝑝, 𝑏, 𝑎, 𝑝, 𝑐, 𝑑) if 𝑐 = 𝑎 and 𝑑 = 𝑏
push(𝑝, 𝑏, 𝑎, 𝑞, 𝜀, 𝑐) if 𝑐 = 𝑎
pop(𝑞, 𝑏, 𝑎, 𝑞) if 𝑏 = 𝑎
Example
Take total order atoms (ℚ,≤). Monotone palindromes:
𝐿 = { 𝑎_0...𝑎_2𝑛 ϵ ℚ* | ∀(0 ≤ 𝑖 ≤ 𝑛) · 𝑎_𝑖 ≤ 𝑎_(2𝑛 − 𝑖) }
Recognized by〈Σ = ℚ, 𝛤 = ℚ, 𝑃 = {𝑝, 𝑞}, 𝜌 = push ∪ pop〉with
push(𝑝, 𝑏, 𝑎, 𝑝, 𝑐, 𝑑) if 𝑐 = 𝑎 and 𝑑 = 𝑏
push(𝑝, 𝑏, 𝑎, 𝑞, 𝜀, 𝑐) if 𝑐 = 𝑎
pop(𝑞, 𝑏, 𝑎, 𝑞) if 𝑏 ≤ 𝑎
Orbit-finite sets and automata are represented via first-order formulae.
Reachability analysis
A pushdown automaton〈Σ,𝛤,𝑃,𝜌〉induces an infinite transition system:
Reachability problem
Given two configurations (𝑝,𝑢),(𝑞,𝑣) ϵ 𝑃⨉𝛤*, decide whether (𝑝,𝑢) →* (𝑞,𝑣)
Saturation
Reachability can be solved by the classic saturation procedure.
Two further ingredients for effectiveness:
Saturation
Reachability can be solved by the classic saturation procedure.
Two further ingredients for effectiveness:
This is precisely what oligomorphic atoms give you.
Oligomorphic atoms
Theorem 1. Let atoms 𝔸 be oligomorphic with decidable satisfiability. Reachability is decidable for first-order definable pushdown automata.
Oligomorphic atoms
Theorem 1. Let atoms 𝔸 be oligomorphic with decidable satisfiability. Reachability is decidable for first-order definable pushdown automata.
No bound on the complexity!
Complexity of satisfiability
𝐾(𝑛) for formulas�with 𝑛 variables
Oligomorphic atoms
Theorem 1. Let atoms 𝔸 be oligomorphic with decidable satisfiability. Reachability is decidable for first-order definable pushdown automata.
No bound on the complexity!
how many equivalence classes of formulas
Complexity of satisfiability
𝐾(𝑛) for formulas�with 𝑛 variables
can be bounded for homogeneous atoms
Homogeneous atoms
Let 𝑚 be the size of the formulas describing the automaton.
Let 𝐾(𝑛) be the complexity of satisfiability of formulas with 𝑛 variables.
Theorem 2. Let atoms 𝔸 be homogeneous. Reachability has complexity
poly(𝑚) · 2^poly(𝑛) · 𝐾(𝑛)
Theorem 3. Let 𝑋 ⊆ ℕ. There exist an homogeneous structure 𝔸(𝑋) s.t. membership in 𝑋 reduces to reachability of pushdown automata over 𝔸(𝑋).
Homogeneous atoms
Let 𝑚 be the size of the formulas describing the automaton.
Let 𝐾(𝑛) be the complexity of satisfiability of formulas with 𝑛 variables.
Theorem 2. Let atoms 𝔸 be homogeneous. Reachability has complexity
poly(𝑚) · 2^poly(𝑛) · 𝐾(𝑛)
Corollary 3. Reachability is fixed-parameter tractable with the number of variables 𝑛 as the parameter.
Theorem 3. Let 𝑋 ⊆ ℕ. There exist an homogeneous structure 𝔸(𝑋) s.t. membership in 𝑋 reduces to reachability of pushdown automata over 𝔸(𝑋).
Homogeneous atoms
Let 𝑚 be the size of the formulas describing the automaton.
Let 𝐾(𝑛) be the complexity of satisfiability of formulas with 𝑛 variables.
Theorem 2. Let atoms 𝔸 be homogeneous. Reachability has complexity
poly(𝑚) · 2^poly(𝑛) · 𝐾(𝑛)
Corollary 3. Reachability is fixed-parameter tractable with the number of variables 𝑛 as the parameter.
Corollary 4. Let satisfiability be EXPTIME. Then, reachability is EXPTIME.
Theorem 3. Let 𝑋 ⊆ ℕ. There exist an homogeneous structure 𝔸(𝑋) s.t. membership in 𝑋 reduces to reachability of pushdown automata over 𝔸(𝑋).
Homogeneous EXPTIME examples
equality | (𝔸,=) |
equivalence | (𝔸,≈) |
total order | (ℚ,≤) |
betweenness order | (ℚ,𝐵) |
cyclic order | (ℚ,𝐾) |
partial order | (𝔸,≤) |
tree order | (𝔸,≤,𝑅) |
preorder | (𝔸,⊑) |
graph | (𝔸,𝐸) |
tournament | (𝔸,𝑇) |
subsumes [Cheng and Kaminski, Acta Inf.’98],� [Murawski, Ramsay, and Tzevelekos, MFCS’14].
- Multidimensional stack alphabet vs. 1-dimensional.
- First-order definable transitions vs. quantifier-free.
Homogeneous EXPTIME examples
equality | (𝔸,=) |
equivalence | (𝔸,≈) |
total order | (ℚ,≤) |
betweenness order | (ℚ,𝐵) |
cyclic order | (ℚ,𝐾) |
partial order | (𝔸,≤) |
tree order | (𝔸,≤,𝑅) |
preorder | (𝔸,⊑) |
graph | (𝔸,𝐸) |
tournament | (𝔸,𝑇) |
Infinitely many examples
Let 𝔸 ⊗ 𝔹 denote the wreath product of two structures 𝔸, 𝔹.
Observation. If 𝔸 and 𝔹 are homogeneous, so it is 𝔸 ⊗ 𝔹. Moreover, satisfiability in 𝔸 ⊗ 𝔹 reduces efficiently to satisfiability in 𝔸 and in 𝔹.
Infinitely many examples
Let 𝔸 ⊗ 𝔹 denote the wreath product of two structures 𝔸, 𝔹.
Observation. If 𝔸 and 𝔹 are homogeneous, so it is 𝔸 ⊗ 𝔹. Moreover, satisfiability in 𝔸 ⊗ 𝔹 reduces efficiently to satisfiability in 𝔸 and in 𝔹.
Examples:
homogeneous with EXPTIME satisfiability!
Non-example
Timed atoms (ℚ,≤,+1) are not homogeneous (not even oligomorphic).
Theorem [Clemente, Lasota - LICS’15]. Reachability in a class of pushdown automata over timed atoms is in NEXPTIME.
Summary
Reachability in pushdown automata:
Arbitrary high complexity depending on the hardness of satisfiability.
Future directions
Proof of concept for further generalizations:
Advertisement
Atoms blog: http://atoms.mimuw.edu.pl