Decidability, Behavioural Equivalences and Infinite Transition Graphs

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.