Skip to main content
SpringerLink
Log in

Dependency-based action refinement

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1997 (MFCS 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1295))

Abstract

Action refinement in process algebras has been widely studied in the last few years as a means to support top-down design of systems. A specific notion of refinement arises when a dependency relation on the actions (in the Mazurkiewicz sense) is used to control the inheritance of orderings from the abstract level. In this paper we present a rather simple operational semantics for dependency-based action refinement. We show the consistency of the operational with a (previously published) denotational semantics. We moreover show that bisimulation is a congruence for dependency-based refinement. Finally, we give an illustrative example.

The research reported in this paper was partially supported by the Human Capital and Mobility Cooperation Network “EXPRESS” (Expressiveness of Languages for Concurrency).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Aceto and M. Hennessy. Towards action-refinement in process algebras. Information and Computation, 103(2):204–269, 1993.

    Article  Google Scholar 

  2. L. Aceto and M. Hennessy. Adding action refinement to a finite process algebra. Information and Computation, 115(2):179–247, 1994.

    Article  Google Scholar 

  3. E. Best, R. Devillers, and J. Esparza. General refinement and recursion operators for the Petri box calculus. In Enjalbert, Finkel, and Wagner, eds., STACS 93, vol. 665 of LNCS, pp. 130–140. Springer, 1993.

    Google Scholar 

  4. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232–268, Jan. 1995.

    Article  Google Scholar 

  5. E. Brinksma, B. Jonsson, and F. Orava. Refining interfaces of communicating systems. In Abramsky and Maibaum, eds., TAPSOFT '91, Volume 2, vol. 494 of LNCS, pp. 297–312. Springer, 1991.

    Google Scholar 

  6. N. Busi, R. van Glabbeek, and R. Gorrieri. Axiomatising ST bisimulation equivalence. In Olderog, ed., Programming Concepts, Methods and Calculi, vol. A-56 of IFIP Transactions, pp. 169–188. IFIP, 1994.

    Google Scholar 

  7. L. Castellano, G. De Michelis, and L. Pomello. Concurrency vs. interleaving: An instructive example. Bull. Eur. Ass. Theoret. Comput. Sci., 31:12–15, 1987. Note.

    Google Scholar 

  8. P. Darondeau and P. Degano. Refinement of actions in event structures and causal trees. Theoretical Computer Science, 118:21–48, 1993.

    Article  Google Scholar 

  9. P. Degano and R. Gorrieri. A causal operational semantics of action refinement. Information and Computation, 122(1):97–119, 1995.

    Article  Google Scholar 

  10. P. Degano, R. Gorrieri, and G. Rosolini. A categorical view of process refinement. In de Bakker, de Roever, and Rozenberg, eds., Semantics: Foundations and Applications, vol. 666 of LNCS, pp. 138–153. Springer, 1992.

    Google Scholar 

  11. R. van Glabbeek and U. Goltz. Equivalences and refinement. In Guessarian, ed., 18éme Ecole de Printemps d'Informatique Théorique Semantique du Parallelisme, vol. 469 of LNCS, 1990.

    Google Scholar 

  12. U. Goltz, R. Gorrieri, and A. Rensink. Comparing syntactic and semantic action refinement. Information and Computation, 125(2):118–143, 1996.

    Article  Google Scholar 

  13. M. Huhn. Action refinement and property inheritance in systems of sequential agents. In Montanari and Sassone, eds., Concur'96, vol. 1119 of LNCS, pp. 639–654. Springer, 1996.

    Google Scholar 

  14. W. Janssen, M. Poel, and J. Zwiers. Actions systems and action refinement in the development of parallel systems. In Baeten and Groote, eds., Concur '91, vol. 527 of LNCS, pp. 298–316. Springer, 1991.

    Google Scholar 

  15. L. Jategaonkar and A. Meyer. Testing equivalences for Petri nets with action refinement. In Cleaveland, ed., Concur '92, vol. 630 of LNCS, pp. 17–31. Springer, 1992.

    Google Scholar 

  16. A. Mazurkiewicz. Basic notions of trace theory. In de Bakker, de Roever, and Rozenberg, eds., Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, vol. 354 of LNCS, pp. 285–363. Springer, 1989.

    Google Scholar 

  17. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  18. M. Nielsen, U. Engberg, and K. G. Larsen. Fully abstract models for a process language with refinement. In de Bakker, de Roever, and Rozenberg, eds., Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, vol. 354 of LNCS, pp. 523–549. Springer, 1989.

    Google Scholar 

  19. D. Park. Concurrency and automata on infinite sequences. In Deussen, ed., Proceedings 5th GI Conference, vol. 104 of LNCS, pp. 167–183. Springer, 1981.

    Google Scholar 

  20. A. Rensink. Posets for configurations! In Cleaveland, ed., Concur '92, vol. 630 of LNCS, pp. 269–285. Springer, 1992.

    Google Scholar 

  21. A. Rensink. Methodological aspects of action refinement. In Olderog, ed., Programming concepts, methods and calculi, vol. A-56 of IFIP Transactions. IFIP, 1994.

    Google Scholar 

  22. A. Rensink. An event-based SOS for a language with refinement. In Desel, ed., Structures in Concurrency Theory, Workshops in Computing, pp. 294–309. Springer, 1995.

    Google Scholar 

  23. A. Rensink and R. Gorrieri. Action refinement as an implementation relation. In Bidoit and Dauchet, eds., TAPSOFT '97. Theory and Practice of Software Development, vol. 1214 of LNCS, pp. 772–786. Springer, 1997.

    Google Scholar 

  24. A. Rensink and H. Wehrheim. Weak sequential composition in process algebras. In Jonsson and Parrow, eds., Concur '94: Concurrency Theory, vol. 836 of LNCS, pp. 226–241. Springer, 1994.

    Google Scholar 

  25. W. Vogler. Failure semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 4:139–162, 1991.

    Article  Google Scholar 

  26. H. Wehrheim. Parametric action refinement. In Olderog, ed., IFIP Transactions: Programming Concepts, Methods and Calculi, pp. 247–266. Elsevier, 1994.

    Google Scholar 

  27. H. Wehrheim. Specifying Reactive Systems with Action Dependencies: Modelling and Hierarchical Design. PhD thesis, University of Hildesheim, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, University of Hildesheim, Postfach 101363, D-31113, Hildesheim, Germany

    Arend Rensink & Heike Wehrheim

Authors
  1. Arend Rensink
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Igor Prívara Peter Ružička

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rensink, A., Wehrheim, H. (1997). Dependency-based action refinement. In: Prívara, I., Ružička, P. (eds) Mathematical Foundations of Computer Science 1997. MFCS 1997. Lecture Notes in Computer Science, vol 1295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0029990

Download citation

  • DOI: https://doi.org/10.1007/BFb0029990

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63437-9

  • Online ISBN: 978-3-540-69547-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation