Bisimulation Equivalence for First-Order Grammars
Petr Jancar (Techn. Univ. Ostrava, Czech Republic)
Info
|
Date |
21st February 2012 (week 6, Hilary Term 2012) |
|
Time |
11:30 |
|
Place |
147 |
Abstract
The aim of the talk is to demonstrate (on figures) the main ideas of the decidability of bisimulation equivalence for first-order grammars. This provides an alternative for Senizergues' decidability proof (1998, 2005) for nondeterministic pushdown automata with deterministic popping epsilon-steps, which generalized his decidability proof for the famous problem of language equivalence of deterministic pushdown automata (1997, 2001). One crucial novelty of the proof presented here is the framework of first-order terms. This framework seems to be more natural for the problem, allowing a presentation which should be transparent for general computer science audience. Though it seems that both the original proof and the proof presented here use the same ideas on an abstract level, the presented (substantially shorter) proof has not arisen as a translation of the original proof, and a detailed comparison would require an enormous technical work. For the deterministic (sub)case, a primitive recursive complexity upper bound was derived by Stirling (2002). Here we also suggest a way of presenting the ideas behind Stirling's proof in the framework of terms.
Further info
|
Related series |
|
