TY - GEN
T1 - Proof-checking protocols using bisimulations
AU - Röckl, Christine
AU - Esparza, Javier
PY - 1999
Y1 - 1999
N2 - We report on our experience in using the Isabelle/HOL theorem prover to mechanize proofs of observation equivalence for systems with infinitely many states, and for parameterized systems. We follow the direct approach: An infinite relation containing the pair of systems to be shown equivalent is defined, and then proved to be a weak bisimulation. The weak bisimilarity proof is split into many cases, corresponding to the derivatives of the pairs in the relation. Isabelle/HOL automatically proves simple cases, and guarantees that no case is forgotten. The strengths and weaknesses of the approach are discussed.
AB - We report on our experience in using the Isabelle/HOL theorem prover to mechanize proofs of observation equivalence for systems with infinitely many states, and for parameterized systems. We follow the direct approach: An infinite relation containing the pair of systems to be shown equivalent is defined, and then proved to be a weak bisimulation. The weak bisimilarity proof is split into many cases, corresponding to the derivatives of the pairs in the relation. Isabelle/HOL automatically proves simple cases, and guarantees that no case is forgotten. The strengths and weaknesses of the approach are discussed.
UR - https://www.scopus.com/pages/publications/84888229570
U2 - 10.1007/3-540-48320-9_36
DO - 10.1007/3-540-48320-9_36
M3 - Conference contribution
AN - SCOPUS:84888229570
SN - 3540664254
SN - 9783540664253
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 525
EP - 540
BT - CONCUR 1999, Concurrency Theory - 10th International Conference, Proceedings
PB - Springer Verlag
T2 - 10th International Conference on Concurrency Theory, CONCUR 1999
Y2 - 24 August 1999 through 27 August 1999
ER -