Skip to main content
SpringerLink
Log in

On Two Dually Nondeterministic Refinement Algebras

  • Conference paper
Relations and Kleene Algebra in Computer Science (RelMiCS 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4136))

Included in the following conference series:

Abstract

A dually nondeterministic refinement algebra with a negation operator is proposed. The algebra facilitates reasoning about total-correctness preserving program transformations and nondeterministic programs. The negation operator is used to express enabledness and termination operators through a useful explicit definition. As a small application, a property of action systems is proved employing the algebra. A dually nondeterministic refinement algebra without the negation operator is also discussed.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Back, R.-J.: Correctness Preserving Program Refinements: Proof Theory and Applications. Mathematical Centre Tracts, vol. 131. Mathematical Centre, Amsterdam (1980)

    Google Scholar 

  2. Back, R.-J., Kurki-Suonio, R.: Decentralization of Process Nets with Centralized Control. In: 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, ACM, Montreal, Quebec, Canada (1983)

    Google Scholar 

  3. Back, R.-J., von Wright, J.: Duality in specification languages: A lattice theoretical approach. Acta Informatica 27(7) (1990)

    Google Scholar 

  4. Back, R.-J., Sere, K.: Stepwise refinement of action systems. Structured Programming 12 (1991)

    Google Scholar 

  5. Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  6. Back, R.-J., von Wright, J.: Reasoning algebraically about loops. Acta Informatica 36 (1999)

    Google Scholar 

  7. Broy, M., Nelson, G.: Adding Fair Choice to Dijkstra’s Calculus. ACM Transactions on Programming Languages and Systems 16(3) (1994)

    Google Scholar 

  8. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. Technical Report 2003-7, Universität Augsburg, Institut für Informatik (2003)

    Google Scholar 

  9. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall International, Englewood Cliffs (1976)

    MATH  Google Scholar 

  10. Floyd, R.W.: Nondeterministic algorithms. Journal of the ACM 14(4) (1967)

    Google Scholar 

  11. Gardiner, P.H., Morgan, C.C.: Data refinement of predicate transformers. Theoretical Computer Science 87(1) (1991)

    Google Scholar 

  12. Kozen, D.: A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Inf. Comput. 110(2) (1994)

    Google Scholar 

  13. Kozen, D.: Automata and Computability. Springer-Verlag, Heidelberg (1997)

    MATH  Google Scholar 

  14. Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3) (1997)

    Google Scholar 

  15. Nelson, G.: A Generalization of Dijkstra’s Calculus. ACM Transactions on Programming Languages and Systems 11(4) (1989)

    Google Scholar 

  16. Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)

    MATH  Google Scholar 

  17. Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Sampaio, A.C.A.: An Algebraic Approach To Compiler Design. World Scientific, Singapore (1997)

    Book  MATH  Google Scholar 

  19. Solin, K.: An Outline of a Dually Nondeterministic Refinement Algebra with Negation. In: P. Mosses, J. Power, M. Seisenberger (eds.): CALCO Young Researchers Workshop 2005, Selected Papers. Univ. of Wales, Swansea, Technical Report CSR 18-2005 (2005)

    Google Scholar 

  20. Solin, K., von Wright, J.: Refinement Algebra with Operators for Enabledness and Termination. MPC (2006) (accepted)

    Google Scholar 

  21. von Wright, J.: From Kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, p. 233. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51 (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Turku Centre for Computer Science, Lemminkäinengatan 14 A, FIN-20520, Åbo, Finland

    Kim Solin

Authors
  1. Kim Solin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, The University of Manchester,  

    Renate A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Solin, K. (2006). On Two Dually Nondeterministic Refinement Algebras. In: Schmidt, R.A. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2006. Lecture Notes in Computer Science, vol 4136. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11828563_25

Download citation

  • DOI: https://doi.org/10.1007/11828563_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37873-0

  • Online ISBN: 978-3-540-37874-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation