Skip to main content
SpringerLink
Log in

Rule Formats for Bounded Nondeterminism in Structural Operational Semantics

  • Chapter
  • First Online:
Semantics, Logics, and Calculi

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

  • 902 Accesses

Abstract

We present rule formats for structural operational semantics that guarantee that the associated labelled transition system has each of the three following finiteness properties: finite branching, initials finiteness and image finiteness.

This research has been supported by the project ‘Nominal Structural Operational Semantics’ (nr. 141558-051) of the Icelandic Research Fund.

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 EPUB and 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

Notes

  1. 1.

    We beg the reader to bear with us in the repetition of ‘sources’ and ‘source’ in sentences like the above. The ‘sources’ refers to the positive premisses and the ‘source’ to the conclusion of the rule.

  2. 2.

    Notice that ‘bounded’ in ‘bounded quantifiers’ does not have the connotation of ‘finite’ that is present in ‘bounded nondeterminism’. The bounded quantifiers restrict the range of the quantified variable, but this range could still be infinite. Examples 7 and 8 illustrate the difference between universal quantifiers and bounded quantifiers with an infinite range.

  3. 3.

    Recall that in intuitionistic logic a universal quantifier ‘\(\forall x.\)’ is akin to a big lambda ‘\(\varLambda x.\)’, i.e., a binding operator at the level of types.

  4. 4.

    We beg the reader to bear with us in the repetition of ‘sources’, ‘actions’, ‘source’, and ‘action’ in sentences like the above. The ‘sources’ and ‘actions’ refer to the positive premisses, and the ‘source’ and ‘action’ to the conclusion of the rule.

References

  1. Abramsky, S.: Domain theory and the logic of observable properties. Ph.D. thesis, Department of Computer Science, Queen Mary College, University of London (1987)

    Google Scholar 

  2. Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, Chap. 3, pp. 197–292. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  3. Amtoft, T., Nielson, F., Nielson, H.R.: Type and Effect Systems. Imperial College Press, London (1999)

    Book  Google Scholar 

  4. Apt, K.R., Plotkin, G.D.: Countable nondeterminism and random assignment. J. ACM 33(4), 724–767 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  5. Baeten, J.C.M., Vaandrager, F.W.: An algebra for process creation. Acta Inf. 29(4), 303–334 (1992). http://dx.doi.org/10.1007/BF01178776

    Article  MATH  MathSciNet  Google Scholar 

  6. Bloom, B.: CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms (preliminary report). In: Boehm, H.J., Lang, B., Yellin, D.M. (eds.) Conference Record of the 21st ACM Symposium on Principles of Programming Languages, Portland, Oregon, pp. 339–347. ACM Press (1994)

    Google Scholar 

  7. Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  8. Cimini, M., Mousavi, M.R., Reniers, M.A., Gabbay, M.J.: Nominal SOS. Electron. Notes Theoret. Comput. Sci. 286, 103–116 (2012)

    Article  MathSciNet  Google Scholar 

  9. Fokkink, W., Vu, T.D.: Structural operational semantics and bounded nondeterminism. Acta Inf. 39(6–7), 501–516 (2003)

    MATH  MathSciNet  Google Scholar 

  10. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: Longo, G. (ed.) Proceedings of the 14th Symposium on Logic in Computer Science, Trento, Italy, pp. 214–224. IEEE Computer Society Press (1999)

    Google Scholar 

  11. van Gelder, A., Ross, K.A., Schilpf, J.S.: The well-founded semantics for general logic programs. J. ACM 38(3), 620–662 (1991)

    MATH  Google Scholar 

  12. van Glabbeek, R.J.: Bounded nondeterminism and the approximation induction principle in process algebra. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 336–347. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  13. Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100(2), 202–260 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  14. Groote, J.F.: Transition system specifications with negative premises. Theoret. Comput. Sci. 118(2), 263–299 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  15. Heyting, A. (ed.): Constructivity in Mathematics. North-Holland Publishing Company, Amsterdam (1959)

    MATH  Google Scholar 

  16. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)

    Article  MATH  Google Scholar 

  17. Klusener, A.S.: Models and axioms for a fragment of real time process algebra. Ph.D. thesis, Department of Mathematics and Computing Science, Technical University of Eindhoven (1993)

    Google Scholar 

  18. Lévy, A.: A hierarchy of formulas in set theory. Mem. Am. Math. Soc. 57, 76 (1965)

    Google Scholar 

  19. Martin-Löf, P.: Intuitionistic Type Theory. Studies in Proof Theory: Lecture Notes, Bibliopolis, Napoli (1984)

    Google Scholar 

  20. Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  21. Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theoret. Comput. Sci. 373(3), 238–272 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  22. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  23. Nielson, H.R., Nielson, F.: Semantics with Applications: An Appertizer. Springer, London (2007)

    Book  Google Scholar 

  24. Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science, vol. 57. Cambridge University Press, Cambridge (2013)

    Book  Google Scholar 

  25. Plotkin, G.D.: A structural approach to operational semantics. Technacal report. DAIMI FN-19, Department of Computer Science, Aarhus University, Denmark (1981)

    Google Scholar 

  26. Plotkin, G.D.: An operational semantics for CSP. In: Salwicki, A. (ed.) Logic of Programs 1980. LNCS, vol. 148, pp. 250–252. Springer, Heidelberg (1983). http://dx.doi.org/10.1007/3-540-11981-7_17

    Chapter  Google Scholar 

  27. Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60–61, 17–139 (2004)

    MathSciNet  Google Scholar 

  28. Przymusinski, T.C.: The well-founded semantics coincides with the three-valued stable semantics. Fundamenta Informaticae 13(4), 445–463 (1990)

    MATH  MathSciNet  Google Scholar 

  29. Sangiorgi, D., Walker, D.: The pi-calculus: A Theory of Mobile Processes. Cambridge Universtity Press, Cambridge (2001)

    Google Scholar 

  30. de Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theoret. Comput. Sci. 37(3), 245–267 (1985)

    Google Scholar 

  31. Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoret. Comput. Sci. 323(1–3), 473–497 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  32. Vaandrager, F.W.: Expressiveness results for process algebras. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1992. LNCS, vol. 666, pp. 609–638. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank two anonymous referees for their careful reading of our paper and their constructive comments.

Author information

Authors and Affiliations

  1. ICE-TCS, School of Computer Science, Reykjavík University, Menntavegur 1, 101, Reykjavík, Iceland

    Luca Aceto, Álvaro García-Pérez & Anna Ingólfsdóttir

Authors
  1. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Álvaro García-Pérez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anna Ingólfsdóttir
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Aceto .

Editor information

Editors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Christian W. Probst

  2. Imperial College London, London, United Kingdom

    Chris Hankin

  3. Aalborg University, Aalborg, Denmark

    René Rydhof Hansen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Aceto, L., García-Pérez, Á., Ingólfsdóttir, A. (2016). Rule Formats for Bounded Nondeterminism in Structural Operational Semantics. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27810-0_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27809-4

  • Online ISBN: 978-3-319-27810-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation