Termination and confluence of term rewrite systems for GSOS process languages,Irek Ulidowski, Technical Report 2002/21, Department of Mathematics and Computer Science, University of Leicester, 2002. Abstract We consider the procedures for automatic derivation of axiom systems and term rewrite systems for process language in the GSOS format. We show that, for a decidable subclass of GSOS process languages, namely syntactically well-founded and linear GSOS process languages, the generated term rewrite systems are strongly normalising, confluent, and sound and complete for bisimulation modulo the associativity and commutativity of the choice operator on closed terms. This paper is available in ps form. |
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
|
Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk). |