Compositional Minimization in Span(Graph): Some Examples
Piergiulio Katis, Nicoletta Sabadini, Robert F. C. Walters · Electronic Notes in Theoretical Computer Science · 2004
We study a class of examples of minimizing automata with respect to branching bisimulation in the context of the Span(Graph) model.Compositional minimization is particularly efficient for the class which includes the classical dining philospher problem and variants.The reason for the efficiency is that finite subsets of the class generate finite submonoids of the bisimulation monoid.We indicate how this may be used in studying deadlock.In the case of the dining philosopher the critical fact is that (F • P ) 3 = (F • P ) 2 in the bisimulation monoid, where F is the fork and P the philosopher.