Skip to main content
SpringerLink
Log in

Institutions for Behavioural Dynamic Logic with Binders

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2017 (ICTAC 2017)

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

Included in the following conference series:

Abstract

Dynamic logic with binders \(\mathcal {D}^{\downarrow }\) has been introduced as an institution for the development of reactive systems based on model class semantics. The satisfaction relation of this logic was, however, not abstract enough to enjoy the modal invariance property (bisimilar models should satisfy the same sentences). We recently overcame this problem by proposing an observational satisfaction relation where the equality on states is interpreted by bisimilarity of states. This entailed, however, a price to pay - the satisfaction condition required for institutions was lost. This paper works on this limitation by establishing a behavioural semantics for \(\mathcal {D}^{\downarrow }\) parametric to behavioural structures - families of equivalence relations on the states of each model. Such structures are taken in consideration in the signature category and, in particular, for the definition of signature morphisms. We show that with these changes we get again an institution with a behavioural model class semantics. The framework is instantiated with specific behavioural structures, resulting in the novel Institution of Crucial Actions.

This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within projects POCI-01-0145-FEDER-016692 and UID/MAT/04106/2013, and by the individual grant SFRH/BPD/103004/2014.

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.

    Thus the information in signatures is used to constrain models as in [3]. In contrast, in Hiden Algebra [7] restrictions concern only signature morphisms but not models.

  2. 2.

    For sake of uniformity, we still use along the section the relational notation to present this function, i.e. we use \((w,w')\in \mathcal {BB}h\) to represent \(\mathcal {BB}h (w)=w'\).

References

  1. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: the common algebraic specification language. Theor. Comput. Sci. 286(2), 153–196 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Barbuti, R., Francesco, N.D., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. J. Comput. Syst. Sci. 59(3), 537–556 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program. 67(1–2), 3–51 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  4. Braüner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series. Springer, Dordrecht (2010). doi:10.1007/978-94-007-0002-4

    MATH  Google Scholar 

  5. Goguen, J.: Types as theories. In: George Michael Reed, A.W.R., Wachter, R.F., (eds.) Topology and Category Theory in Computer Science (1991)

    Google Scholar 

  6. Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Goguen, J.A., Malcolm, G.: A hidden agenda. Theor. Comput. Sci. 245(1), 55–101 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  8. Goguen, J., Roşu, G.: Hiding more of hidden algebra. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1704–1719. Springer, Heidelberg (1999). doi:10.1007/3-540-48118-4_40

    Google Scholar 

  9. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)

    MATH  Google Scholar 

  10. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  11. Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1999. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998). doi:10.1007/3-540-49253-4_20

    Chapter  Google Scholar 

  12. Hennicker, R., Madeira, A.: Behavioural semantics for the dynamic logic with binders. In: Roggenbach, M. (ed.) Recent Trends in Algebraic Development Methods - Selected Papers of WADT 2016. Springer (2016, to appear)

    Google Scholar 

  13. Madeira, A., Barbosa, L.S., Hennicker, R., Martins, M.A.: Dynamic logic with binders and its application to the development of reactive systems. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 422–440. Springer, Cham (2016). doi:10.1007/978-3-319-46750-4_24

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  15. Misiak, M.: Behavioural semantics of algebraic specifications in arbitrary logical systems. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 144–161. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31959-7_9

    Chapter  Google Scholar 

  16. Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_40

    Chapter  Google Scholar 

  17. Tarlecki, A.: Towards heterogeneous specifications. In: Frontiers of Combining Systems (FroCoS 1998). Applied Logic Series, pp. 337–360. Kluwer Academic Publishers (1998)

    Google Scholar 

Download references

Acknowledgement

We would like to thank the anonymous reviewers of this paper for their careful reviews with many useful comments and suggestions.

Author information

Authors and Affiliations

  1. Ludwig-Maximilians-Universität München, Munich, Germany

    Rolf Hennicker

  2. HASLab, INESC TEC, University of Minho, Braga, Portugal

    Alexandre Madeira

  3. CIDMA, University of Aveiro, Aveiro, Portugal

    Alexandre Madeira

Authors
  1. Rolf Hennicker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandre Madeira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexandre Madeira .

Editor information

Editors and Affiliations

  1. Vietnam National University, Hanoi, Vietnam

    Dang Van Hung

  2. University of New Mexico, Albuquerque, New Mexico, USA

    Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Hennicker, R., Madeira, A. (2017). Institutions for Behavioural Dynamic Logic with Binders. In: Hung, D., Kapur, D. (eds) Theoretical Aspects of Computing – ICTAC 2017. ICTAC 2017. Lecture Notes in Computer Science(), vol 10580. Springer, Cham. https://doi.org/10.1007/978-3-319-67729-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67729-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67728-6

  • Online ISBN: 978-3-319-67729-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation