Abstract
We present a first-order modal μ-calculus which uses parameterised maximal fix-points to describe safety and liveness properties of processes. Then we give a local model checking proof system for deciding if a process satisfies such a formula. The processes we consider are those definable in regular value-passing CCS with parameterised recursive definitions. Certain rules in the proof system carry side conditions which leave auxiliary proof obligations of checking properties of the data language.
The proof system is incomplete in general, but we show, for two different sub-logics, that if a process with a restricted form of parameterisation satisfies a modal formula then this can be derived in the proof system. This is subject to the assumption that all auxiliary proof obligations concerning the data language can be discharged.
This research was supported by EPSRC project GR/K60701 and the 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.
References
R. Amadio and M. Dam. Toward a modal theory of types for the π-calculus. In Proc. Formal Techniques in Real Time and Fault Tolerant Systems, Uppsala 96, volume 1135 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
M. Dam. Model checking mobile processes. In E. Best, editor, Proceedings CONCUR 93, Hildesheim, volume 715 of Lecture Notes in Computer Science, pages 22–36. Springer-Verlag, 1993.
D. Gurov, S. Berezin, and B. Kapron. A modal μ-calculus and a proof system for value-passing processes. In Proc. Infinity Workshop on Verification of Infinite State Systems, Pisa, pages 149–163, 1996.
M. Hennessy and H. Lin. Symbolic bisimulations. Theoretical Computer Science, 138:353–389, 1995.
M. Hennessy and H. Lin. Proof systems for message-passing process algebras. Formal Aspects of Computer Science, pages 379–407, 1996.
M. Hennessy and H. Liu. A modal logic for message passing processes. Acta Informatica, 32:375–393, 1995.
K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72:265–288, 1990.
R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part I + II. Information and Computation, 100(1):1–77, 1992.
J. Rathke. Symbolic techniques for value-passing calculi. PhD thesis, University of Sussex, 1997. To appear.
J. Rathke and M. Hennessy. Local model checking for a value-based modal μ-calculus. Technical Report 0596, University of Sussex, 1996.
C. Stirling. Modal and temporal logics. In S. Abramsky, D. Gabbay, and T.Maibaum, editors, Handbook of Logic in Computer Science, Vol I. Oxford University Press, 1990.
C. Stirling and D. Walker. Local model checking in the modal μ-calculus. Theoretical Computer Science, 89:161–177, 1991.
G. Winskel. A note on model checking the modal v-calculus. Theoretical Computer Science, 83:157–167, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rathke, J., Hennessy, M. (1997). Local model checking for value-passing processes (Extended abstract). In: Abadi, M., Ito, T. (eds) Theoretical Aspects of Computer Software. TACS 1997. Lecture Notes in Computer Science, vol 1281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014555
Download citation
DOI: https://doi.org/10.1007/BFb0014555
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63388-4
Online ISBN: 978-3-540-69530-1
eBook Packages: Springer Book Archive