A fairly classic result from the concurrency-theory literature with a complexity-theoretic flavour is a theorem by José L. Balcázar, Joaquim Gabarró and Miklos Santha to the effect that checking various forms of bisimilarity (viz., strong, weak (aka observational equivalence) and rooted weak bisimilarity (aka observational congruence)) over finite labelled transition systems is P-complete. This theorem holds true even over acyclic labelled transition systems over a one-letter alphabet.
The original journal paper appeared in Formal Aspects of Computing in 1992. (See here for the BiBTeX reference. I am not aware of a version of it that is available on line.) It is one of those papers that I have been citing for a while, but whose result I had never studied in great detail despite meaning to do so.
At long last, I pulled myself together, read the fine print of the paper, and, jointly with Anna Ingolfsdottir, decided to pen down a write-up of the ideas in the proof of the main result in that work. We made the piece available from the web page for our book as supplementary reading material; see Deciding Bisimilarity over Finite Labelled Transition Systems is P-complete.
The note is written in the same pedagogical style as the textbook it accompanies, and we plan to reuse it as part of an ongoing project we expect to complete by the end of the year. We trust that it is suitable for classroom use as well as for self study, and we hope that it will make another classic result from concurrency theory accessible to mature BSc and MSc students.
No comments:
Post a Comment