The Computer Journal Advance Access published online on April 18, 2008
The Computer Journal, doi:10.1093/comjnl/bxn009
Congruence Formats for Weak Readiness Equivalence and Weak Possible Future Equivalence
1 Academy of Mathematics and System Science, Chinese Academy of Sciences, 55# East Road, Zhong Guan Cun Beijing 100080, P.R. China
2 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, 4# South Fourth Street, Zhong Guan Cun, Beijing 100190, P.R. China
* Corresponding author: xwhuang{at}amss.ac.cn
Received 26 June 2007; revised 17 January 2008
Accepted for publication 25 January 2008.
Weak equivalences are important behavioral equivalences in the course of specifying and analyzing reactive systems using process algebraic languages. In this paper, we propose a series of weak equivalences named weak parametric readiness equivalences, which take two previously known behavioral equivalences, i.e. the weak readiness equivalence and the weak possible future equivalence, as their special cases. More importantly, based on the idea of structural operational semantics, a series of rule formats are presented to guarantee congruence for these weak parametric readiness equivalences, i.e. to show that the proposed rule formats can guarantee the congruence of their corresponding weak parametric readiness equivalences. This series of rule formats reflects the differences in the weak parametric readiness equivalences. We conclude that when the weak parametric readiness equivalences become coarser, their corresponding rule formats turn tighter.
Key Words: weak equivalences • congruence formats • structural operational semantics