Skip to main content
SpringerLink
Log in

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

  • 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:

Abstract

There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations.

In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.

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. 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.) FASE 2012. LNCS, vol. 7212, pp. 43–58. Springer, Heidelberg (2012)

    Google Scholar 

  2. Bauer, S.S., Mayer, P., Legay, A.: MIO workbench: A tool for compositional design with modal input/output interfaces. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 418–421. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. 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. CoRR, abs/1306.0741 (2013)

    Google Scholar 

  4. Beneš, N., Křetínský, J.: Process algebra for modal transition systemses. In: MEMICS, pp. 9–18 (2010)

    Google Scholar 

  5. 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 

  6. 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 

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

    Article  MathSciNet  MATH  Google Scholar 

  8. BMoTras, http://delahaye.benoit.free.fr/BMoTraS.tar

  9. Børjesson, A., Larsen, K.G., Skou, A.: Generality in design and compositional verification using TAV. Formal Meth. Syst. Design 6(3), 239–258 (1995)

    Article  Google Scholar 

  10. Boudol, G., Larsen, K.G.: Graphical versus logical specifications. Theor. Comput. Sci. 106(1), 3–20 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  11. Bruns, G.: An industrial application of modal process logic. Sci. Comput. Program. 29(1-2), 3–22 (1997)

    Article  Google Scholar 

  12. Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194–235 (2003)

    Article  MathSciNet  MATH  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. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Google Scholar 

  15. Darondeau, P., Dubreil, J., Marchand, H.: Supervisory control for modal specifications of services. In: WODES, pp. 428–435 (2010)

    Google Scholar 

  16. D’Ippolito, N., Fischbein, D., Foster, H., Uchitel, S.: MTSA: Eclipse support for modal transition systems construction, analysis and elaboration. In: ETX, pp. 6–10 (2007)

    Google Scholar 

  17. Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebr. Program. 77(1-2), 20–39 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  18. Fecher, H., Steffen, M.: Characteristic mu-calculus formulas for underspecified transition systems. Electr. Notes Theor. Comput. Sci. 128(2), 103–116 (2005)

    Article  Google Scholar 

  19. Fokkink, W., van Glabbeek, R.J., de Wind, P.: Compositionality of Hennessy-Milner logic by structural operational semantics. Theor. Comput. Sci. 354(3), 421–440 (2006)

    Article  MATH  Google Scholar 

  20. Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  21. 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 

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

    Article  MathSciNet  MATH  Google Scholar 

  23. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  24. Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Logic at Botik, pp. 163–180 (1989)

    Google Scholar 

  25. Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  26. Larsen, K.G., Liu, X.: Equation solving using modal transition systems. In: LICS, pp. 108–117 (1990)

    Google Scholar 

  27. Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, pp. 232–246 (1989)

    Google Scholar 

  28. 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 

  29. Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci. 72, 265–288 (1990)

    Article  MATH  Google Scholar 

  30. Larsen, K.G., Liu, X.: Compositionality through an operational semantics of contexts. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 526–539. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  31. Nyman, U.: Modal Transition Systems as the Basis for Interface Theories and Product Lines. PhD thesis, Institut for Datalogi, Aalborg Universitet (2008)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  34. Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Symp. Program., pp. 337–351 (1982)

    Google Scholar 

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

    Article  Google Scholar 

  36. Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Passerone, R.: Why are modalities good for interface theories? In: ACSD, pp. 119–127 (2009)

    Google Scholar 

  37. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)

    Google Scholar 

  38. Uchitel, S., Chechik, M.: Merging partial behavioural models. In: SIGSOFT FSE, pp. 43–52 (2004)

    Google Scholar 

  39. Ward, M., Dilworth, R.P.: Residuated lattices. Trans. AMS 45(3), 335–354 (1939)

    Article  MathSciNet  Google Scholar 

  40. Yetter, D.N.: Quantales and (noncommutative) linear logic. J. Symb. Log. 55(1), 41–64 (1990)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Masaryk University, Brno, Czech Republic

    Nikola Beneš & Jan Křetínský

  2. Irisa / INRIA, Rennes, France

    Benoît Delahaye, Uli Fahrenberg & Axel Legay

  3. Technische Universität München, Germany

    Jan Křetínský

Authors
  1. Nikola Beneš
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benoît Delahaye
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Uli Fahrenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jan Křetínský
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Axel Legay
    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

Beneš, N., Delahaye, B., Fahrenberg, U., Křetínský, J., Legay, A. (2013). 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. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_7

Download citation

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

  • 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