A logic for distributed transition systems

  • K. Lodaya
  • R. Ramanujam
  • P. S. Thiagarajan
Technical Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 354)


We present a logical characterization of a particular aspect of concurrency called the concurrent step notion. We do so by providing a sound and complete axiomatization of models called distributed transition systems. In a distributed transition system an old state is transformed into a new state through a set of actions occurring concurrently. Our logical language has the minimal features of linear time temporal logic and that of propositional dynamic logic. Our main result implies that satisfiability in our logical system is decidable.


concurrent step distributed transition systems axiomatization soundness completeness 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BHP]
    Ben-Ari, M., Halpern, J.Y. and Pnueli, A. (1982): Deterministic Propositional Dynamic Logic: Finite Models, Complexity and Completeness. J. Comput. Syst. Sci., 25, pp. 402–417.CrossRefGoogle Scholar
  2. [DDM]
    Degano, P., De Nicola, R. and Montanari, U. (1987): A Distributed Operational Semantics for CCS based on Condition/Event Systems. Nota Interna I.E.I. — B4 — 21, Department of Computer Science, University of Pisa (To appear in Acta Informatica).Google Scholar
  3. [FL]
    Fischer, M.J. and Ladner, R.E. (1979): Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci., 18, pp 194–211.CrossRefGoogle Scholar
  4. [HM]
    Hennessy, M. and Milner, R. (1980): On Observing Non-determinism and Concurrency, Springer Lecture Notes in Computer Science, 85, Springer-Verlag, pp 299–309.Google Scholar
  5. [K]
    Kröger, F. (1987): Temporal Logic of Programs. EATCS Monograph on Theoretical Computer Science, 8, Springer-Verlag.Google Scholar
  6. [KP]
    Kozen, D. and Parikh, R. (1982): An Elementary Proof of Completeness of PDL. Theor. Comput. Sci., 14, pp 113–118.CrossRefGoogle Scholar
  7. [LPZ]
    Lichtenstein, O., Pnueli, A. and Zuck, L. (1985): The Glory of the Past. In: Logic of Programs, Ed. R. Parikh, Springer Lecture Notes in Computer Science, 193, Springer-Verlag, pp 196–218.Google Scholar
  8. [M]
    Milner, R., (1980): A Calculus of Communicating Systems. Springer Lecture Notes in Computer Science, 92, Springer-Verlag.Google Scholar
  9. [O]
    Olderog, E.-R. (1987): Operational Petri Net Semantics for CCSP. In: Advances in Petri Nets, Ed. G. Rozenberg, Springer Lecture Notes in Computer Science, 266, Springer-Verlag, pp 381–400.Google Scholar
  10. [P]
    Parikh, R. (1988): Decidability and Undecidability in Distributed Transition systems (Unpublished Manuscript).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • K. Lodaya
    • 1
  • R. Ramanujam
    • 1
  • P. S. Thiagarajan
    • 1
  1. 1.The Institute of Mathematical SciencesMadrasIndia

Personalised recommendations