Syntactic Formats for Free: An Abstract Approach to Process Equivalence
Bartek Klin
April 2003 |
Abstract:
A framework of Plotkin and Turis, originally aimed at providing
an abstract notion of bisimulation, is modified to cover other operational
equivalences and preorders. Combined with bialgebraic methods, it yields a
technique for deriving syntactic formats for transition system
specifications, which guarantee operational preorders to be precongruences.
The technique is applied to the trace prorder, the completed trace preorder
and the failures preorder. In the latter two cases, new syntactic formats
guaranteeing precongruence properties are introduced
Available as PostScript, PDF, DVI. |