Skip to main content
SpringerLink
Log in

Modular Semantics for Transition System Specifications with Negative Premises

  • Conference paper
CONCUR 2013 – Concurrency Theory (CONCUR 2013)

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

Included in the following conference series:

  • 995 Accesses

Abstract

Transition rules with negative premises are needed in the structural operational semantics of programming and specification constructs such as priority and interrupt, as well as in timed extensions of specification languages. The well-known proof-theoretic semantics for transition system specifications involving such rules is based on well-supported proofs for closed transitions. Dealing with open formulae by considering all closed instances is inherently non-modular – proofs are not necessarily preserved by disjoint extensions of the transition system specification.

Here, we conservatively extend the notion of well-supported proof to open transition rules. We prove that the resulting semantics is modular, consistent, and closed under instantiation. Our results provide the foundations for modular notions of bisimulation such that equivalence can be proved with reference only to the relevant rules, without appealing to all existing closed instantiations of terms.

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. Aceto, L., Cimini, M., Ingólfsdóttir, A.: Proving the validity of equations in GSOS languages using rule-matching bisimilarity. MSCS 22(2), 291–331 (2012)

    MATH  Google Scholar 

  2. Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, ch. 3, pp. 197–292. Elsevier (2001)

    Google Scholar 

  3. Aceto, L., Ingolfsdottir, A.: On the expressibility of priority. Inf. Process. Lett. 109(1), 83–85 (2008)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  5. Bloom, B., Fokkink, W., van Glabbeek, R.J.: Precongruence formats for decorated trace semantics. ACM Trans. Comput. Logic 5(1), 26–78 (2004)

    Article  Google Scholar 

  6. Bol, R., Groote, J.F.: The meaning of negative premises in transition system specifications. JACM 43(5), 863–914 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  7. Churchill, M., Mosses, P.D.: Modular bisimulation theory for computations and values. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 97–112. Springer, Heidelberg (2013)

    Google Scholar 

  8. Clark, K.L.: Negation as failure. In: Proc. ADBT 1977, pp. 293–322. Plemum Press (1978)

    Google Scholar 

  9. Fokkink, W.J., van Glabbeek, R.J.: Ntyft/ntyxt rules reduce to ntree rules. I&C 126(1), 1–10 (1996)

    MATH  Google Scholar 

  10. Fokkink, W.J., Verhoef, C.: A conservative look at operational semantics with variable binding. I&C 146(1), 24–54 (1998)

    MathSciNet  MATH  Google Scholar 

  11. van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. Tech. Report, Stanford (STAN-CS-TN-95-16) (1995)

    Google Scholar 

  12. van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. JLAP 60-61, 229–258 (2004)

    Google Scholar 

  13. Groote, J.F.: Transition system specifications with negative premises. TCS 118(2), 263–299 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  14. Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. I&C 100(2), 202–260 (1992)

    MathSciNet  MATH  Google Scholar 

  15. Mosses, P.D., Mousavi, M.R., Reniers, M.A.: Robustness of equations under operational extensions. In: Proc. EXPRESS 2010. EPTCS, vol. 41, pp. 106–120 (2010)

    Google Scholar 

  16. Mousavi, M., Reniers, M.A., Groote, J.F.: SOS rule formats and meta-theory: 20 years after. TCS 373, 238–272 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  17. Plotkin, G.D.: A structural approach to operational semantics. JLAP 60-61, 17–139 (2004)

    Google Scholar 

  18. Rensink, A.: Bisimilarity of open terms. I&C 156, 345–385 (2000)

    MathSciNet  MATH  Google Scholar 

  19. de Simone, R.: Higher-level synchronizing devices in MEIJE-SCCS. TCS 37, 245–267 (1985)

    Article  MATH  Google Scholar 

  20. Verhoef, C.: A congruence theorem for structured operational semantics with predicates and negative premises. Nord. J. of Comp. 2(2), 274–302 (1995)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Swansea University, UK

    Martin Churchill & Peter D. Mosses

  2. Halmstad University, Sweden

    Mohammad Reza Mousavi

  3. Eindhoven University of Technology, Netherlands

    Mohammad Reza Mousavi

Authors
  1. Martin Churchill
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter D. Mosses
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mohammad Reza Mousavi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Facultad de Matemáticas, Astronomía y Física, Universidad Nacional de Córdoba – CONICET, Medina Allende s/n,, X5000HUA, Córdoba, Argentina

    Pedro R. D’Argenio

  2. Departamento de Computación,, Universidad de Buenos Aires - Conicet, Intendente Güirales 2160, C1428EGA, Ciudad Autónoma de Buenos Aires, Argentina

    Hernán Melgratti

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Churchill, M., Mosses, P.D., Mousavi, M.R. (2013). Modular Semantics for Transition System Specifications with Negative Premises. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40184-8_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40183-1

  • Online ISBN: 978-3-642-40184-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation