Abstract
The aim of this paper is to examine some basic topics of true concurrency from the viewpoint of program logics. In particular, logical characterizations of observational (bisimulation) equivalences based on partial ordering observations are studied. To date, in contrast with the interleaving approach, such equivalences have been almost exclusively studied from the operational standpoint. We shall show that they can be defined in a logical setting and that standard modal and temporal techniques can also be applied to true concurrency models. As a result, the interleaving and the partial ordering views of concurrency are reconciled within a logical setting.
Research partially supported by Esprit Basic Research Action Program, Project 3011 CEDISYS, and by Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo, Project LAMBRUSCO.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Boudol, G. and Castellani, I. Concurrency and Atomicity. Theoret. Comput. Sci., 59, 1988, pp. 25–84
Browne, M.C., Clarke, E.M.and Grümberg, O. Characterizing Finite Kripke Structure in Propositional Temporal Logic, Theoret. Comput. Sci., 59, 1988, pp. 115–131
Clarke, E., Emerson, A., Sistla, P. Automatic Verifications of Finite State Concurrent Systems using Temporal Logic Specifications, ACM TOPLAS, 8, 1986, pp. 244–263.
Darondeau, P. and Degano, P. Causal Trees, in proceedings ICALP '89, LNCS, 372, pp.234–248, 1989.
Degano,P., De Nicola,R. and Montanari,U. Observational Equivalences for Concurrency Models, in Formal Description of Programming Concepts III, M. Wirsing, ed., North Holland, 1987, pp. 105–132.
Degano,P., De Nicola,R. and Montanari,U. A Partial Ordering Semantics for CCS, Technical Report, Dipartmento di Informatica, Università di Pisa, 1988, To appear in Theoret. Comput. Sci..
Degano,P., De Nicola,R. and Montanari,U. Partial Ordering Descriptions and Observations of Nondeterministic Concurrent Processes, in [REX89].
De Nicola, R. Extensional Equivalences for Transition Systems, Acta Informatica, 24, 1987, pp. 211–237.
Degano, P. and Montanari, U. Concurrent Histories: A Basis for Observing Distributed Systems, Journal of Computer and System Sciences, 34, 1987, pp. 442–461.
De Nicola,R. and Vaandrager,F. Three Logics for Branching Bisimulations, IEEE LICS Conference, 1990
van Glabbeek,R. and Goltz,U. Equivalence Notions for Concurrent Systems and Refinement of Actions, in proceeding MFCS '89, LNCS, 379, 1989.
van Glabbeek,R. and Weijland,P. Branching Time and Abstraction in Bisimulation Semantics, in Information Processing 89, (Ritter ed.) North Holland, 1989.
Hoaare,C.A.R. Communicating Sequential Processes, Prentice Hall, 1985
Hennessy,M. and Milner,R. Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM, 32, 1985.
Hennessy, M. and Stirling,C. The Power of Future Perfect in Program Logics, Info and Co., 1985, pp. 23–52.
Katz,S. and Peled,D. Interleaving set Temporal Logic, in 6th ACM Symp. on Distributed Computing, 1987.
Keller, R., Formal Verification of Parallel Programs, Com. ACM, 7, 1976
Lodaya, K and Thiagarajan, P.S. A Modal Logic for a Subclass of Event Structures, CALP '87, LNCS, 267, pp.290–303, 1987.
Lodaya,K, Ramanujam, R. and Thiagarajan,P.S. A Logic for Distributed Systems, in [REX89].
Milner,R. Communication and Concurrency, Prentice Hall 1989.
Nielsen, M., Plotkin, G. and Winskel, G. Petri Nets, Event Structures and Domains, Part 1, Theoret. Comput. Sci., 13, 1981, pp.85–108.
Park, D. Concurrency and Automata on Infinite Sequences, in Proc. GI, LNCS, 104, 1981, pp. 167–183.
Penczek, W. A Temporal Logic for Event Structures, Fundamenta Informaticae, 11, 1988, pp. 297–326.
Pratt, V. Modelling Concurrency with Partial Orders, International Journal of Parallel Programming, 15, 1986, pp. 33–71.
Reisig,W. Petri Nets, An Introduction. EATCS Monographs in Computer Science, Springer Verlag, 1985.
Reisig,W. Towards a Temporal Logic of Causality and Choice in Distributed Systems in [REX89].
Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, deBakker, deRoever and Rozenberg eds., LNCS, 354, 1988.
Rabinovich,A. and Trakhtembrot,B. Behaviour Structures and Nets, Fundamenta Informaticae, 1988.
Stirling,C. Modal and Temporal Logics, In Handbook of Logic in Computer Science, Vol I, Abramsky ed., to appear, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Nicola, R., Ferrari, G.L. (1990). Observational logics and concurrency models. In: Nori, K.V., Veni Madhavan, C.E. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1990. Lecture Notes in Computer Science, vol 472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53487-3_53
Download citation
DOI: https://doi.org/10.1007/3-540-53487-3_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53487-7
Online ISBN: 978-3-540-46313-9
eBook Packages: Springer Book Archive