Abstract
We present a parametric tool for the analysis of distributed concurrent systems. Processes are internally represented as proved transition systems. Actually, we use a fragment of them, in which only one transition exits from a node among those mutually concurrent. This permits to have compact representations that are linear in average with the number of actions in the term of the language that describes the system. Another important property of these compact transition systems is that they preserve truly concurrent bisimulations, that can be checked in average in polynomial time. Parametricity is achieved by resorting to the rich labelling of the transitions encoding the parallel structure of processes. These labels are then “observed” for retrieving the interleaving, causal and locational semantics.
Work partially supported by ESPRIT Basic Research Action n. 8130 — LOMAPS, by Progetto Finalizzato CNR “Sistemi Informatici e Calcolo Parallelo — Obiettivo Lambrusco” and by Progetto Speciale CNR “Specifica ad Alto Livello e Verifica Formale di Sistemi Digitali”.
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
G. Boudol and I. Castellani. A non-interleaving semantics for CCS based on proved transitions. Foundamenta Informaticae, XI(4):433–452, 1988.
G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. A theory of processes with localities. In Proceedings of CONCUR'92, LNCS 630, pages 108–122. Springer-Verlag, 1992.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics-based tool for the verification of concurrent systems. ACM Transaction on Programming Languages and Systems, pages 36–72, 1993.
M. Clegg and A. Valmari. Reduced labelled transition systems save verification effort. In Proceedings of CONCUR'91, LNCS 527. Springer-Verlag, 1991.
Ph. Darondeau and P. Degano. Causal trees. In Proceedings of ICALF'89, LNCS 372, pages 234–248. Springer-Verlag, 1989.
R. de Simone and D. Vergamini. Aboard AUTO. Technical Report 111, INRIA Sophia-Antipolis, 1989.
P. Degano, R. De Nicola, and U. Montanari. Partial ordering derivations for CCS. In Proceedings of FCT, LNCS 199, pages 520–533. Springer-Verlag, 1985.
P. Degano and C. Priami. Proved trees. In Proceedings of ICALP'92, LNCS 623, pages 629–640. Springer-Verlag, 1992.
P. Degano and C. Priami. A compact representation of finite-state processes. Technical Report LOMAPSDIPISA2, LOMAPS Project, 1993.
P. Degano and C. Priami. Causality for mobile processes. In Proceedings of ICALP'95, LNCS. Springer-Verlag, 1995. To appear.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of CAV'91, LNCS 575, pages 332–342. Springer-Verlag, 1991.
J.C. Godskesen, K.G. Larsen, and M. Zeeberg. TAV users manual. Technical report, Aalborg University Center, Denmark, 1989.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
P. Inverardi, C. Priami, and D. Yankelevich. Automatizing parametric reasoning on distributed concurrent systems. Formal Aspects of Computing, 6(6):676–695, 1994.
P. C. Kanellakis and S. C. Smolka. CCS expressions, finite state processes and three problems of equivalence. In Proceedings of the Second ACM Symposium on Principles of Distributed Computing, 1983.
A. Kiehn. Local and global causes. Technical report, TUM 342/23/91, 1991.
X. Leroy and M. Mauny. The Caml Light System, Release 0.5. Documentation and User's Manual., 1992.
R. Milner. Communication and Concurrency. Prentice-Hall, London, 1989.
R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.
D. Park. Concurrency and automata on infinite sequences. In Proceedings of GI, LNCS 104, pages 167–183. Springer-Verlag, 1981.
D. Peled. All from one, one from all: On model checking using representatives. In Proceedings of CAV'93, LNCS 697, pages 409–423. Springer-Verlag, 1993.
C. Priami and D. Yankelevich. Read-write causality. In Proceedings of MFCS'94, LNCS 841, pages 567–576. Springer-Verlag, 1994.
A. Valmari and M. Tienari. An improved failure equivalence for finite-state systems with a reduction algorithm. In Proceedings of IFIP WG6.1 Protocol Specification, Testing and Verification, Stockholm, June 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bianchi, A., Coluccini, S., Degano, P., Priami, C. (1995). An efficient verifier of truly concurrent properties. In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 1995. Lecture Notes in Computer Science, vol 964. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60222-4_95
Download citation
DOI: https://doi.org/10.1007/3-540-60222-4_95
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60222-4
Online ISBN: 978-3-540-44754-2
eBook Packages: Springer Book Archive