Titlebook: Introduction to the Formal Design of Real-Time Systems; David Gray Textbook 1999 Springer-Verlag London Limited 1999 Bisimulation.communic

NUDGE

Proving Things Correct,tion for external behaviours. While this method scores on simplicity, in lots of cases action by action comparison is too distinctive; rather than proving two agents identical, we’re more likely to want to prove that they either have or do not have certain properties.

Vsd168

ODIUM

Automating SCCS,cations. A tool which goes a long way to meet these objectives is the Concurrency Work Bench (CWB) produced by those nice people at the Laboratory for the Foundation of Computer Science (LFCS), at the University of Edinburgh, and most of this chapter is devoted to its use.