D.: Guarded operations Refinement and Simulation

Simulation rules have long been used as an effective computational means to decide refinement relations in state-based formalisms. Here we investigate how they might be amended so as to decide the event-based notion of singleton fail-ures refinement of abstract data types or processes that have operations with a “guarded ” interpretation. As the results presented here and found elsewhere in the literature are so sen-sitive to the details of the definitions used, we have machine-checked our results.