Skip to main content
SpringerLink
Log in

Structural Refinement for the Modal nu-Calculus

  • Conference paper
Book cover Theoretical Aspects of Computing – ICTAC 2014 (ICTAC 2014)

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

Included in the following conference series:

Abstract

We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent.

Using our translations, we also transfer the structural operations of composition and quotient from disjunctive modal transition systems to the modal nu-calculus. This shows that the modal nu-calculus supports composition and decomposition of specifications.

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., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems. Cambridge Univ. Press (2007)

    Google Scholar 

  2. Bauer, S.S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., Wąsowski, A.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, vol. 7212, pp. 43–58. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.: Quantitative refinement for weighted modal transition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 60–71. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Bauer, S.S., Fahrenberg, U., Legay, A., Thrane, C.: General quantitative specification theories with modalities. In: Hirsch, E.A., Karhumäki, J., Lepistö, A., Prilutskii, M. (eds.) CSR 2012. LNCS, vol. 7353, pp. 18–30. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  5. Beneš, N., Černá, I., Křetínský, J.: Modal transition systems: Composition and LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 228–242. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Beneš, N., Delahaye, B., Fahrenberg, U., Křetínský, J., Legay, A.: Hennessy-milner logic with greatest fixed points as a complete behavioural specification theory. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 76–90. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275–289. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Th. Comp. Sci. 410(41), 4026–4043 (2009)

    Google Scholar 

  9. Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comp. 218, 54–68 (2012)

    Google Scholar 

  10. Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Log. J. IGPL 8(3), 339–365 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  11. Boudol, G., Larsen, K.G.: Graphical versus logical specifications. Th. Comp. Sci. 106(1), 3–20 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  12. Bradfield, J., Stirling, C.: Modal mu-calculi. In: The Handbook of Modal Logic. Elsevier (2006)

    Google Scholar 

  13. Caires, L., Cardelli, L.: A spatial logic for concurrency. Inf. Comp. 186(2) (2003)

    Google Scholar 

  14. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  15. de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 103–127. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  16. de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Fahrenberg, U., Legay, A., Traonouez, L.-M.: Structural refinement for the modal nu-calculus. CoRR, 1402.2143 (2014), http://arxiv.org/abs/1402.2143

  18. Gebler, D., Fokkink, W.: Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 395–409. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Hart, J.B., Rafter, L., Tsinakis, C.: The structure of commutative residuated lattices. Internat. J. Algebra Comput. 12(4), 509–524 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  20. Hennessy, M.: Acceptance trees. J. ACM 32(4), 896–928 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kozen, D.: Results on the propositional μ-calculus. Th. Comp. Sci. 27 (1983)

    Google Scholar 

  22. Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  23. Larsen, K.G.: Ideal specification formalism = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33–56. Springer, Heidelberg (1990)

    Google Scholar 

  24. Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Th. Comp. Sci. 72(2&3), 265–288 (1990)

    Article  MATH  Google Scholar 

  25. Larsen, K.G.: Efficient local correctness checking. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 30–43. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  26. Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS. IEEE Computer Society (1990)

    Google Scholar 

  27. Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universität München (1997)

    Google Scholar 

  28. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  29. Prior, A.N.: Papers on Time and Tense. Clarendon Press, Oxford (1968)

    Google Scholar 

  30. Raclet, J.-B.: Residual for component specifications. Publication interne 1843, IRISA, Rennes (2007)

    Google Scholar 

  31. Raclet, J.-B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)

    Article  Google Scholar 

  32. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. IEEE Computer Society (2002)

    Google Scholar 

  33. Scott, D., de Bakker, J.W.: A theory of programs. IBM, Vienna (1969) (unpublished manuscript)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria / IRISA, Campus de Beaulieu, 35042, Rennes CEDEX, France

    Uli Fahrenberg, Axel Legay & Louis-Marie Traonouez

Authors
  1. Uli Fahrenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Louis-Marie Traonouez
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, Romanian Academy, Blvd. King Carol I no.8, 700505, Iaşi, Romania

    Gabriel Ciobanu

  2. LORIA, Université de Lorraine, Campus Scientifique, BP 239, 54506, Vandœvre-lès-Nancy, France

    Dominique Méry

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Fahrenberg, U., Legay, A., Traonouez, LM. (2014). Structural Refinement for the Modal nu-Calculus. In: Ciobanu, G., Méry, D. (eds) Theoretical Aspects of Computing – ICTAC 2014. ICTAC 2014. Lecture Notes in Computer Science, vol 8687. Springer, Cham. https://doi.org/10.1007/978-3-319-10882-7_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10882-7_11

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10881-0

  • Online ISBN: 978-3-319-10882-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation