Bisimulation Equivalence of First Order Grammars
Peter Jancar (ostrava)
Info
|
Date |
21st February 2012 (week , 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 |
|
