Advertisement

Behavioural equivalence relations induced by programming logics

  • Stephen D. Brookes
  • William C. Rounds
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

In this paper we compare the descriptive power of three programming logics by studying the elementary equivalence relations which the logics induce on nondeterministic state-transition systems. In addition, we compare these relations with other natural state-equivalence relations for nondeterministic systems. We find that the notions of bisimilarity (Park [P], Ogden [O]) and observation equivalence (Milner [M]) are very strong equivalences compared with those induced by the logics. These three comprise regular trace logic (RTL), propositional dynamic logic (PDL), and Hennessy-Milner logic (HML). Regular trace logic is a new logic which can be used to give behavioural specifications for concurrent systems (e.g. Wolper [W], but with significant differences). It is a way of formalising those properties of programs which have been given informally in terms of path expressions [CH]. The model theory and axiomatics of this logic are interesting in their own right. Propositional dynamic logic is well-known; our treatment differs from the standard one only in that we regard the modalities as specifying intended behaviour instead of being programs. Hennessy-Milner logic is a simplified modal logic which those authors used as a characterisation of their notion of observation equivalence, which we call weak observation equivalence in this paper. We also include a brief treatment in this context of two other natural equivalences for nondeterministic systems: failure equivalence [HBR] and trace equivalence [H], both of which are weaker than the relations induced by the logics but can be characterised using appropriate logical subsets.

Keywords

Equivalence Relation Transition System Label Transition System Concurrent System Disjunctive Normal Form 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [B1]
    Brookes, S.D., On the relationship of CCS and CSP, this volume.Google Scholar
  2. [B2]
    Brookes, S.D., A Model for Communicating Sequential Processes, Ph.D. thesis, University of Oxford (submitted 1983).Google Scholar
  3. [CH]
    Campbell, R., and Habermann, N., The Specification of Process Synchronization by Path Expressions, Springer LNCS Vol. 16.Google Scholar
  4. [GR]
    Golson, W.G., and Rounds, W.C., Connections between Two Theories of Concurrency: Metric Spaces and Synchronisation Trees, Technical Report, Computing Research Laboratory, University of Michigan (January 1983)Google Scholar
  5. [H]
    Hoare, C.A.R., A model for Communicating Sequential Processes, Technical Report PRG-22, University of Oxford, Programming Research Group (1981).Google Scholar
  6. [HBR]
    Hoare, C.A.R., Brookes, S.D., and Roscoe, A.W., A Theory of Communicating Sequential Processes, Technical Report PRG-16, Oxford University, Programming Research Group (1981).Google Scholar
  7. [HKP]
    Harel, D., Kozen, D., and Parikh, R., Process Logic: Expressiveness, Decidability and Completeness, Proceedings of IEEE Symposium on Foundations of Computer Science (1980).Google Scholar
  8. [HM]
    Hennessy, M., and Milner, R., On Observing Nondeterminism and Concurrency, Proc. 7th ICALP, Springer LNCS Vol. 85 (1980).Google Scholar
  9. [K]
    Keller, R., Formal Verification of Parallel Programs, CACM 19, Vol. 7 (July 1976).Google Scholar
  10. [M]
    Milner, R., A Calculus of Communicating Systems, Springer LNCS Vol. 92.Google Scholar
  11. [O]
    Ogden, W.F., Private communication.Google Scholar
  12. [P]
    Park, D.M.R., Concurrency and Automata on Infinite Sequences, Computer Science Department, University of Warwick.Google Scholar
  13. [Pn]
    Pnueli, A., The Temporal Logic of Programs, Proceedings of IEEE Symposium on Foundations of Computer Science (1977).Google Scholar
  14. [RS]
    Rabin, M.O., and Scott, D.S., Finite Automata and their Decision Problems, IBM J. Res. 3:2 (1959).Google Scholar
  15. [R]
    Roscoe, A.W., A Mathematical Theory of Communicating Processes, Ph.D. thesis, Oxford University (1982).Google Scholar
  16. [RB]
    Rounds, W.C., and Brookes, S.D., Possible Futures, Acceptances, Refusals, and Communicating Processes, Proc. 22nd IEEE Symposium on Foundations of Computer Science (October 1981).Google Scholar
  17. [W]
    Wolper, P., Temporal Logic can be more expressive, Proc. 22nd IEEE Symposium on Foundations of Computer Science.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Stephen D. Brookes
    • 1
  • William C. Rounds
    • 2
  1. 1.Carnegie-Mellon UniversityPittsburgh
  2. 2.University of MichiganAnn Arbor

Personalised recommendations