Edinburgh Research Archive logo

Edinburgh Research Archive

University of Edinburgh homecrest
View Item 
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

Decidability, Behavioural Equivalences and Infinite Transition Graphs

View/Open
ECS-LFCS-91-191.pdf (735.0Kb)
ECS-LFCS-91-191.ps (637.4Kb)
Date
07/1991
Author
Hüttel, Hans
Metadata
Show full item record
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.
URI
http://hdl.handle.net/1842/411
Collections
  • Informatics thesis and dissertation collection

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page

 

 

All of ERACommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisorsThis CollectionBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisors
LoginRegister

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page