Bisimulation verification using the up to techniques

被引：2
作者：
Hirschkoff D. [1 ]
机构：
[1] LIP, ENS Lyon, 69364 Lyon, 07, 46, allée d'Italie
来源：
International Journal on Software Tools for Technology Transfer | 2001年 / 3卷 / 03期
关键词：
Bisimulation; Pi-calculus; Up to bisimulation; Verification;
D O I：
10.1007/s100090100041
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
This paper investigates the use of the so-called up to techniques for bisimulation in the framework of verification. We first introduce a method to exploit these techniques, that originate in theoretical works, in the applied context of verification. We then apply it on the π-calculus, in order to design an up to bisimulation verification algorithm for π-calculus terms. The outcome of such an effort is evaluated on two examples that were run on a prototype implementation. © 2001 Springer-Verlag.
引用
收藏
页码：271 / 285
页数：14
相关论文
共 45 条
  • [1] Abdulla P.A., Annichini A., Bensalem S., Bouajjani A., Habermehl P., Lakhnech Y., Verification of infinite-state systems by combining abstraction and reachability, Proc. CAV'99. LNCS 111, (1999)
  • [2] Abadi M., Gordon A., A calculus for cryptographic protocols: The spi calculus, Inf. Comput, 148, 1, pp. 1-70, (1999)
  • [3] Amadio R., An asynchronous model of locality, failure process mobility, Proc. Coordination'97. LNCS 1282, (1997)
  • [4] Boreale M., de Nicola R., Pugliese R., Proof Techniques for Cryptographic Processes, Proc. LICS'99
  • [5] Boreale M., On the Expressiveness of Internal Mobility in Name-Passing Calculi, TCS, 195, 2, pp. 205-226, (1998)
  • [6] Bryant R.E., Symbolic manipulation of Boolean functions using a graphical representation, In: Proc. 22nd Design Automation Conference, pp. 688-694, (1994)
  • [7] Boreale M., Sangiorgi D., Bisimulation in name-passing calculi without matching, Proc. LICS'98
  • [8] Cardelli L., Abstractions for Mobile Computations, Secure Internet Programming: Security Issues For Mobile and Distributed Objects. LNCS 1603, (1999)
  • [9] Caucal D., Graphes canoniques de graphes algébriques, Inf. Théor. Appl. (RAIRO), 24, 4, pp. 339-352, (1990)
  • [10] Cardelli L., Gordon A., Mobile Ambients, Proc. FOS-SACS'98. LNCS 1378, (1998)
12345