Abstract
This paper presents π-logic, an action-based logic for π-calculus. A model checker is built for this logic, following an automata-based approach. This is made possible by a result which allows finite state Labelled Transition Systems to be associated with a wide class of π-calculus agents by preserving a notion of bisimulation equivalence. The model checker was thus built reusing an efficient model checker for the action based logic Actl, after a sound translation from π-logic into Actl has been defined.
Work partially funded by CNR Integrated Project Metodi e Strumenti per la Progettazione e la Verifica di Sistemi Eterogenei Connessi mediante Reti di Comunicazione.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E., E. Emerson, and A. Sistla: 1986, ‘Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specification’. ACM Transaction on Programming Languages and Systems 8 (2), 244–263.
Dam, M.: 1993, `Model checking mobile processes’. In: Proc. CONCUR’93, Vol. 715 of LNCS.
Emerson, E. A. and J. Halpern: 1986, ‘“Sometime” and “Not never” revisited: On branching versus linear time temporal logic’. Journal of ACM 33, 151–178.
Emerson, E. A. and C. Lei: 1986, ‘Efficient Model Checking in Fragments of the Propositional Mu-Calculus’. In: Proceedings of Symposium on Logics in Computer Science. pp. 267–278.
Ferrari, G., G. Ferro, S. Gnesi, U. Montanari, M. Pistore, and G. Ristori: 1997, ‘An automata based verification environment for mobile processes’. In: Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’97, Vol. 1217 of LNCS.
Ferro, G.: 1994, ‘AMC: ACTL Model Checker. Reference Manual’. Technical Report B4–47, IEI.
Gnesi, S.: 1997, ‘A formal verification environment for concurrent systems design’. In: Proc. Automated Formal Methods Workshop, ENTCS.
Gosling, J. and H. McGilton: 1996, ‘The Java Language Environment. A White Paper’. Technical report, Sun Microsystems.
Hennessy, M. and R. Milner: 1985, ‘Algebraic laws for nondeterminism and concurrency’. Journal of ACM 32, 137–161.
Kozen, D.: 1983, ‘Results on the propositional n-calculus’. Theoretical Computer Science 27, 333–354.
Milner, R.: 1989, Communication and Concurrency. Prentice-Hal.
Milner, R., J. Parrow, and D. Walker: 1992a, ‘A calculus of mobile processes (parts I and II)’. Information and Computation 100, 1–77.
Milner, R., J. Parrow, and D. Walker: 1992b, ‘Modal logic for mobile processes’. In: Proc. CONCUR’91, Vol. 527 of LNCS.
Montanari, U. and M. Pistor: 1997, ‘History Dependent Automata’. Technical report, Department of Computer Science, University of Pisa.
Montanari, U. and M. Pistore: 1995, ‘Checking bisimilarity for finitary zr-calculus’. In: Proc. CONCUR’95, Vol. 962 of LNCS.
Nicola, R. D. and F. W. Vaandrager: 1990, ‘Action versus state based logics for transition systems’. In: Proc. Ecole de Printemps on Semantics of Concurrency, Vol. 469 of LNCS.
Sangiorgi, D.: 1992, ‘Expressing mobility in process algebras: first-order and higher-order paradigms’. Ph.D. thesis, University of Edinburgh.
Stirling, C. and D. Walker: 1989, ‘Local model checking in the modal li-calculus.’. Theoretical Computer Science pp. 161–177.
Victor, B. and F. Moller: 1994, ‘The Mobility Workbench — A tool for the ircalculus’. In: Proc. CAV’94, Vol. 818 of LNCS.
Walker, D.: 1991, ‘π-calculus semantics for object-oriented programming languages’. In: Proc. TACS’91.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Gnesi, S., Ristori, G. (2000). A Model Checking Algorithm for π-Calculus Agents. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (eds) Advances in Temporal Logic. Applied Logic Series, vol 16. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9586-5_17
Download citation
DOI: https://doi.org/10.1007/978-94-015-9586-5_17
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5389-3
Online ISBN: 978-94-015-9586-5
eBook Packages: Springer Book Archive