Open AccessDeciding Framed Bisimilarity
Author(s) -
Hans Hüttel
Publication year - 2002
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v9i25.21741
Subject(s) - pi calculus , process calculus , decidability , fragment (logic) , equivalence (formal languages) , calculus (dental) , mathematics , turing , computer science , discrete mathematics , programming language , medicine , dentistry
The spi-calculus, proposed by Abadi and Gordon, is a process calculus based on the -calculus and is intended for reasoning about the behaviour of cryptographic protocols. We consider the finite-control fragment of the spi-calculus, showing it to be Turing-powerful (a result which is joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.) Next, we restrict our attention to finite (non-recursive) spi-calculus. Here, we show that framed bisimilarity, an equivalence relation proposed by Abadi and Gordon, showing that it is decidable for this fragment.