Abstract
We present a proof system for verifying CCS processes in the modal ยต-calculus. Its novelty lies in the generality of the proof judgements allowing parametric and compositional reasoning in this complex setting. This is achieved, in part, by the use of explicit fixed point ordinal approximations, and in part by a complete separation, following an approach by Simpson, of rules concerning the logic from the rules encoding the operational semantics of the process language.
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
R. Amadio and M. Dam. Reasoning about higher-order processes. In Proc. CAAPโ95, Lecture Notes in Computer Science, 915:202โ217, 1995.
R. Amadio and M. Dam. A modal theory of types for the ฯ-calculus. In Proc. FTRTFTโ96, Lecture Notes in Computer Science, 1135:347โ365, 1996.
M. Dam. Proving properties of dynamic process networks. Information and Computation, 140:95โ114, 1998.
M. Dam, L.-รฅ. Fredlund, and D. Gurov. Toward parametric verification of open distributed systems. In Compositionality: the Significant Difference, H. Langmaack, A. Pnueli and W.-P. de Roever (eds.), Lecture Notes Notes in Computer Science, Springer-Verlag, 1536:150โ185, 1998.
M. Dam and D. Gurov. ยต-calculus with explicit points and approximations. In preparation, 1999.
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.
R. Milner. Communication and Concurrency. Prentice Hall International, 1989.
A. Simpson. Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 420โ430, San Diego, California, 26โ29 1995. IEEE Computer Society Press.
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.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56:72โ99, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
ยฉ 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dam, M., Gurov, D. (2000). Compositional Verification of CCS Processes. In: Bjรธner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 1999. Lecture Notes in Computer Science, vol 1755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46562-6_22
Download citation
DOI: https://doi.org/10.1007/3-540-46562-6_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67102-2
Online ISBN: 978-3-540-46562-1
eBook Packages: Springer Book Archive