## Decidability, Behavioural Equivalences and Infinite Transition
Graphs

**Hans Hüttel**
*Abstract:* This thesis studies behavioural equivalences on
labelled infinite transition graphs and the role that they can play
in the context of modal logics and notions from language theory. A
natural class of such infinite graphs is that corresponding to the
*SnS*-definable tree languages first studied by Rabin. We show
that a modal mu-calculus with label set {0,...,*n* - 1} can
define these tree languages up to an observational equivalence.

Another natural class of infinite transition graphs is that of
normed BPA processes, which correspond to the graphs of leftmost
derivations in context-free grammars without useless productions. A
remarkable result is that strong bisimulation is decidable for
these graphs. After an outline of the existing proofs due to Baeten
et al. and Caucal we present a much simpler proof using a tableau
system closely related to the branching algorithms employed in
language theory following Korenjak and Hopcroft. We then present a
result due to Colin Stirling, giving a weakly sound and complete
sequent-based equational theory for bisimulation equivalence for
normed BPA processes from the tableau system. Moreover, we show how
to extract a fundamental relation (as in the work of Caucal) from a
successful tableau.

We then introduce silent actions and consider a class of normed
BPA processes with the restriction that processes cannot terminate
silently, showing that the decidability result for strong
bisimilarity can be extended to van Glabbeek's branching
bisimulation equivalence for this class of processes.

We complete the picture by establishing that *all* other
known behavioural equivalences and a number of preorders are
undecidable for normed BPA processes.

**PhD Thesis - Price £7.50**

*LFCS report ECS-LFCS-91-191 (also published as
CST-86-91)*

This report is available in the following formats:

Previous |

Index |

Next