University of Sydney, Australia
Computer Science Seminar Room, G1.15
We show how to simplify a symbolic transition system to remove `unobservable' internal or silent actions while preserving the traces of the system. A corresponding simplification problem has been studied before for transition systems with handshake communication, an interleaving interpretation of parallel composition and bisimulation equivalence, but the framework we use, of non-blocked communication and trace equivalence, is important because it has been widely accepted for representing distributed applications; also the simplifications possible are much more powerful in this setting.
We have embodied the new simplification algorithms in a tool, and we demonstrate our achievements by using the tool on a well-known leader election algorithm, where the simplification reduces the algorithm (expressed as a composition of processes) until it consists of a single symbolic transition, whose correctness is evident by inspection.
Finally we discus our approach with handshake communication, a non interleaving interpretation of parallel composition and failure equivalence.