Abstract
A verification environment for the π-calculus is presented. The environment takes a direct advantage of a general theory which allows to associate ordinary finite state automata to a wide class of π-calculus agents, so that equivalent automata are associated to equivalent π-calculus agents. A key feature of the approach is the reuse of efficient algorithms and verification techniques which have been developed and implemented for ordinary automata.
Work partially founded by CNR Integrated Project Metodi e Strumenti per la Progettazione e la Verifica di Sistemi Eterogenei Connessi mediante Reti di Comunicazione and Esprit Working Group CONFER2.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Bouali and R. De Simone. Symbolic bisimulation minimization. In Proc. CAV'92, LNCS 663. Springer-Verlag, 1992.
A. Bouali, A. Ressouche, V. Roy and R. De Simone. The FC2Tools set. In Proc. CAV'96, LNCS 1102. Springer Verlag, 1996.
G. Boudol, I. Castellani, M. Hennessy and A. Kiehn. Observing localities. Theoretical Computer Science, 114: 31–61, 1993.
R. Cleveland, J. Parrow and B. Steffen. The Concurrency Workbench: a semantics-based tool for the verification of finite-state systems. ACM Transactions on Programming Languages and Systems 15(1):36–72, 1003.
M. Dam. Model checking mobile processes. In Proc. CONCUR'93, LNCS 715. Springer Verlag, 1993.
Ph. Darondeau and P. Degano. Causal trees. In Proc. ICALP'89, LNCS 372. Springer-Verlag, 1989.
R. De Nicola and F. W. Vaandrager. Action versus state based logics for transition systems. In Proc. Ecole de Printemps on Semantics of Concurrency, LNCS 469. Springer Verlag, 1990.
J.-C. Fernandez and L. Mounier. “On the fly” verification of behavioral equivalences and preorders. In Proc. CAV'91, LNCS 575. Springer Verlag, 1991.
G. Ferro. AMC: ACTL Model Checker. Reference Manual. IEI-Internal Report, B4-47, 1994.
S. Gnesi. A formal verification environment for concurrent systems design. In Proc. Automated Formal Methods Workshop, ENTCS 5. Elsevier, 1996.
S. Gnesi, G. Ristori. A Model Checking algorithm for π-calculus agents. IEI-Internal Report, B4-25, October 1996.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of ACM 32 (1), pp. 137–161, 1985.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science 27, pp. 333–354, 1983.
E. Madelaine and D. Vergamini. AUTO: A verification tool for distributed systems using reduction of finite automata networks. Formal Description Techniques II, 1990.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
R. Milner, J. Parrow and D. Walker. A calculus of mobile processes (parts I and II). Information and Computation, 100:1–77, 1992.
R. Milner, J. Parrow and D. Walker. Modal logic for mobile processes. In Proc. CONCUR'91, LNCS 527. Springer Verlag, 1992.
U. Montanari and M. Pistore. Checking bisimilarity for finitary π-calculus. In Proc. CONCUR'95, LNCS 962. Springer Verlag, 1995.
U. Montanari and M. Pistore. Minimal Transition Systems for History-Preserving Bisimulation. To appear Proc. STACS'97, LNCS, 1997.
U. Montanari and M. Pistore. History Dependent Automata. To appear as Technical Report, Department of Computer Science, University of Pisa.
U. Montanari, M. Pistore and D. Yankelevich. Efficient minimization up to location equivalence. In Proc. ESOP'96, LNCS 1058. Springer-Verlag, 1996.
F. Orava and J. Parrow. An Algebraic Verification of a Mobile Network” Formal Aspects of Computing 4, pp. 497–543.
P. Quaglia. The π-calculus with explicit substitutions. PhD thesis TD-09/96. Dipartimanto di Informatica, Università di Pisa, 1996.
V. Roy and R. De Simone. AUTO and autograph. In Proc. CAV'90, LNCS 531. Springer Verlag, 1990.
D. Sangiorgi. A theory of bisimulation for the π-calculus. In Proc. CONCUR'93, LNCS 715. Springer Verlag, 1993.
B. Victor and F. Moller. The Mobility Workbench — A tool for the π-calculus. In Proc. CAV'94, LNCS 818. Springer Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrari, G., Ferro, G., Gnesi, S., Montanari, U., Pistore, M., Ristori, G. (1997). An automata based verification environment for mobile processes. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035394
Download citation
DOI: https://doi.org/10.1007/BFb0035394
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive