Advertisement

Testing equivalence for Petri Nets with action refinement: Preliminary report

  • Lalita Jategaonkar
  • Albert Meyer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

A definition of “action refinement” is given for an operational model of concurrent processes based on safe Petri Nets, generalizing previous work of Vogler and van Glabbeek/Goltz. A failure-style denotational semantics is described for process nets. The semantics is fully abstract for Hennessy Testing-equivalence on nets acting as refinement operators as well as operands. The semantics embodies the notions of deadlock, failures and divergences found in the Hoare/CSP and Hennessy Testing-equivalence theories, as well as some of the basic ideas of “pomset runs” and “causal” partial orders of Net theory.

Keywords

Label Transition System Refinement Operator Downward Closure Action Refinement Reachable Marking 
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. 1.
    L. Aceto and U. Engberg. Failure semantics for a simple process language with refinement. Technical report, INRIA, Sophia-Antipolis, 1991.Google Scholar
  2. 2.
    L. Aceto and M. Hennessy. Towards action-refinement in process algebras. In Proceedings of 4th LICS, pages 138–145. IEEE Computer Society Press, 1989.Google Scholar
  3. 3.
    L. Aceto and M. Hennessy. Adding action refinement to a finite process algebra. In Proceedings of 18 th ICALP, volume 510 of Lecture Notes in Computer Science. Springer-Verlag, 1991.Google Scholar
  4. 4.
    S. D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In Seminar on Concurrency, volume 197 of Lecture Notes in Computer Science, pages 281–305. Springer-Verlag, 1984.Google Scholar
  5. 5.
    L. Castellano, G. De Michelis, and L. Pomello. Concurrency vs. interleaving: an instructive example. Bull. Europ. Assoc. Theoretical Computer Sci., 31:12–15, 1987.zbMATHGoogle Scholar
  6. 6.
    U. Goltz. CCS and petri nets. Technical report, GMD, July 1990.Google Scholar
  7. 7.
    M. C. Hennessy. Algebraic Theory of Processes. Series on Foundations of Computing. MIT Press, 1988. 272 pp.Google Scholar
  8. 8.
    M. C. Hennessy. Concurrent testing of processes. In Proceedings of 3rd CONCUR, 1992. Appears in this volume.Google Scholar
  9. 9.
    C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall, Inc., 1985. 256 pp.Google Scholar
  10. 10.
    L. Jategaonkar and A. R. Meyer. Testing equivalence for Petri nets with split and choice refinements. Paper presented at the Eighth Workshop on the Mathematical Foundations of Programming Semantics, Oxford, England, Apr. 1992.Google Scholar
  11. 11.
    R. Milner. Communication and Concurrency. Series in Computer Science. Prentice-Hall, Inc., 1989.Google Scholar
  12. 12.
    M. Nielsen, U. Engberg, and K. S. Larsen. Fully abstract models for a process language with refinement. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 523–548. Springer-Verlag, 1988.Google Scholar
  13. 13.
    R. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, CWI, 1990.Google Scholar
  14. 14.
    R. van Glabbeek and U. Goltz. Refinement of actions in causality based models. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 267–300. Springer-Verlag, 1990.Google Scholar
  15. 15.
    R. van Glabbeek and F. Vaandrager. Petri net models for algebraic theories of concurrency. In Proceedings of PARLE Conference, volume 259 of Lecture Notes in Computer Science, pages 224–242. Springer-Verlag, 1987.Google Scholar
  16. 16.
    W. Vogler. Failure semantics and deadlocking of modular petri nets. Acta Informatica, 26(4):333–348, 1989.zbMATHMathSciNetGoogle Scholar
  17. 17.
    W. Vogler. Failures semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 4:139–162, 1991.zbMATHMathSciNetCrossRefGoogle Scholar
  18. 18.
    W. Vogler. Is partial order semantics necessary for action refinement? Technical report, Technische Universitat Munchen, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Lalita Jategaonkar
    • 1
  • Albert Meyer
    • 1
  1. 1.MIT Laboratory for Computer ScienceCambridge

Personalised recommendations