Abstract
We study the problem of specifying and verifying properties of π-calculus processes while relying on a bisimulation semantics. As our property specification language we use a version of the modal μ-calculus adapted to the π-calculus. We show that the logical language is sufficiently expressive to characterize by means of a finite formula a process up to any approximation of the bisimulation relation. We consider the problem of checking that a process of the π-calculus satisfies a specification expressed in this modal μ-calculus. We develop an algorithm which is sound in general, and complete for processes having a finite reachability property. Finally, we present a proof system which can be applied to prove non-recursive properties of arbitrary processes. We show that the system is complete on the non-recursive fragment of the logical language.
The first author was partially supported by France Télécom, CTI-CNET 95-1B-182 Modélisation de Systèmes Mobiles. The second author was partially supported by EU Esprit project 8130 LOMAPS. Both authors were partially supported by HCM-Network Express.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Amadio and M. Dam. Reasoning about higher-order processes. In Proc. CAAP 95, Aarhus. SLNCS 915, 1995. Preliminary version appeared as SICS RR 94-18, available at http://wwwi3s.unice.fr/~amadio/.
R. Amadio and M. Dam. Toward a modal theory of types for the π-calculus. Technical Report 95-18, Swedish Institute for Computer Science, Stockholm, 1995. Available at ftp://sics.se/pub/fdt/mfd/tmttpc.ps.Z.
M. Dam. Model checking mobile processes. In Proc. CONCUR'93, Lecture Notes in Computer Science, 715:22–36, 1993. Full version in SICS report RR94:1, 1994.
M. Dam. Compositional proof systems for model checking infinite state processes. In Proc. CONCUR'95, Lecture Notes in Computer Science, 962:12–26, 1995.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137–162, 1985.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
U. Montanari and M. Pistore. Checking bisimilarity for finitary π-calculus. In CONCUR '95, SLNCS 962, 1995.
R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Process, Parts 1–2. Information and Computation, 100(1):1–77, 1992.
R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, 114:149–171, 1993.
F. Orava and J. Parrow. An algebraic verification of a mobile network. Formal Aspects of Computing, pages 497–543, 1992.
C. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311–347, 1987.
C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89:161–177, 1991.
D. Van Daalen. The language theory of Automath. PhD thesis, Technological University of Eindhoven, 1980. PhD thesis.
G. Winskel. Model checking the modal ν-calculus. Springer Lecture Notes in Computer Science, 372, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amadio, R.M., Dam, M. (1996). Toward a modal theory of types for the π-calculus. In: Jonsson, B., Parrow, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1996. Lecture Notes in Computer Science, vol 1135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61648-9_50
Download citation
DOI: https://doi.org/10.1007/3-540-61648-9_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61648-1
Online ISBN: 978-3-540-70653-3
eBook Packages: Springer Book Archive