Abstract
This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call \(\mathcal {D}^{\downarrow }\)-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
See translator.nrc.pt.
References
Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)
Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 307–321. Springer, Heidelberg (1999)
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)
Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, Cambridge (2010)
Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program. 67(1–2), 3–51 (2006)
Braüner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series, vol. 37. Springer, Netherlands (2010)
Cengarle, M.V.: The temporal logic institution. Technical report 9805, LUM München, Institut für Informatik (1998)
Diaconescu, R.: Institutional semantics for many-valued logics. Fuzzy Sets Syst. 218, 32–52 (2013)
Fiadeiro, J.L., Maibaum, T.S.E.: Temporal theories as modularisation units for concurrent system specification. Formal Asp. Comput. 4(3), 239–272 (1992)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)
Goranko, V.: Temporal logic with reference pointers. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol. 827, pp. 133–148. Springer, Heidelberg (1994). doi:10.1007/BFb0013985
Gorrieri, R., Rensink, A., Zamboni, M.A.: Action refinement. In: Handbook of Proacess Algebra, pp. 1047–1147. Elsevier (2000)
Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Havelund, K.: The Fork Calculus -Towards a Logic for Concurrent ML. Ph.D. thesis, DIKU, University of Copenhagen, Denmark (1994)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1, 271–281 (1972)
Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, Upper Saddle River (1985)
Jones, C.B.: Software Development - A Rigorous Approach. Series in Computer Science. Prentice Hall, Upper Saddle River (1980)
Knijnenburg, P., van Leeuwen, J.: On models for propositional dynamic logic. Theor. Comput. Sci. 91(2), 181–203 (1991)
Larsen, K.G., Thomsen, B.: A modal process logic. In: Third Annual Symposium on Logic in Computer Science, pp. 203–210. IEEE Computer Society (1988)
Madeira, A., Barbosa, L., Hennicker, R., Martins, M.: Dynamic logic with binders and its applications to the developmet of reactive systems (extended with proofs). Technical report (2016). http://alfa.di.uminho.pt/~madeira/main_files/extreport.pdf
Magee, J., Kramer, J.: Concurrency - State Models and Java Programs, 2nd edn. Wiley, Hoboken (2006)
O’Reilly, L., Mossakowski, T., Roggenbach, M.: Compositional modelling and reasoning in an institution for processes and data. In: Mossakowski, T., Kreowski, H.-J. (eds.) WADT 2010. LNCS, vol. 7137, pp. 251–269. Springer, Heidelberg (2012)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). doi:10.1007/BFb0017309
Reggio, G., Astesiano, E., Choppy, C.: Casl-ltl: a casl extension for dynamic reactive systems version 1.0. - summary. Technical report disi-tr-03-36. Technical report, DFKI Lab Bremen (2013)
Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1985)
Roggenbach, M.: CSP-CASL - a new integration of process algebra and algebraic specification. Theor. Comput. Sci. 354(1), 42–71 (2006)
Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited. Acta Inform. 25(3), 233–281 (1988)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs on TCS, an EATCS Series. Springer, Heidelberg (2012)
Sekerinski, E., Sere, K.: Program Development by Refinement: Case Studies Using the B Method. Springer, Heidelberg (2012)
Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)
Acknowledgments
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 Tecnologia within project POCI-01-0145-FEDER-016692 and UID/MAT/04106/2013 at CIDMA. A. Madeira and L. S. Barbosa are further supported by FCT individual grants SFRH/BPD/103004/2014 and SFRH/BSAB/113890/2015, respectively.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Madeira, A., Barbosa, L.S., Hennicker, R., Martins, M.A. (2016). Dynamic Logic with Binders and Its Application to the Development of Reactive Systems. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-46750-4_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46749-8
Online ISBN: 978-3-319-46750-4
eBook Packages: Computer ScienceComputer Science (R0)