Reference:

C. Röckl and J. Esparza. Proof-checking protocols using bisimulations. In J. C. M. Baeten and S. Mauw, editors, Proc. of CONCUR'99, number 1664 in Lecture Notes in Computer Science, pages 525–540. Springer-Verlag, 1999.

Abstract:

Observation equivalence is of particular interest to the verification of concurrent systems, as it is compositional, detects deadlocks, and possesses a well-developed theory. We examine the mechanization of proofs by exhibiting bisimulation relations. As examples we have chosen infinite-state, as well as parameterized systems, that cannot be treated by fully automatic tools based on exploring the complete state space. The description of the systems is given by a transition semantics based on value-passing processes, though automata models, for instance, would be equally applicable. For the mechanization, we use the interactive theorem prover Isabelle/HOL, as it enables the user to apply inductive definitions and proofs, and provides powerful built-in proof tactics.

Suggested BibTeX entry:

@inproceedings{RE99,
    author = {C. R{\"o}ckl and J. Esparza},
    booktitle = {Proc. of CONCUR'99},
    editor = {J. C. M. Baeten and S. Mauw},
    number = {1664},
    pages = {525--540},
    publisher = {{Springer-Verlag}},
    series = {{Lecture Notes in Computer Science}},
    title = {Proof-Checking Protocols Using Bisimulations},
    year = {1999}
}