{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:04:07Z","timestamp":1762459447083},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_24","type":"book-chapter","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T22:11:57Z","timestamp":1474409517000},"page":"422-440","source":"Crossref","is-referenced-by-count":5,"title":["Dynamic Logic with Binders and Its Application to the Development of Reactive Systems"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Madeira","sequence":"first","affiliation":[]},{"given":"Luis S.","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Rolf","family":"Hennicker","sequence":"additional","affiliation":[]},{"given":"Manuel A.","family":"Martins","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling, Specification and Verification","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/3-540-48168-0_22","volume-title":"Computer Science Logic","author":"C Areces","year":"1999","unstructured":"Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 307\u2013321. Springer, Heidelberg (1999)"},{"issue":"2","key":"24_CR3","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","volume":"286","author":"E Astesiano","year":"2002","unstructured":"Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Br\u00fcckner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: the common algebraic specification language. Theor. Comput. Sci. 286(2), 153\u2013196 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR4","volume-title":"Process Algebra: Equational Theories of Communicating Processes","author":"JCM Baeten","year":"2010","unstructured":"Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, Cambridge (2010)"},{"issue":"1\u20132","key":"24_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.jlap.2005.09.002","volume":"67","author":"M Bidoit","year":"2006","unstructured":"Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program. 67(1\u20132), 3\u201351 (2006)","journal-title":"J. Log. Algebr. Program."},{"key":"24_CR6","series-title":"Applied Logic Series","volume-title":"Hybrid Logic and Its Proof-Theory","author":"T Bra\u00fcner","year":"2010","unstructured":"Bra\u00fcner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series, vol. 37. Springer, Netherlands (2010)"},{"key":"24_CR7","unstructured":"Cengarle, M.V.: The temporal logic institution. Technical report 9805, LUM M\u00fcnchen, Institut f\u00fcr Informatik (1998)"},{"key":"24_CR8","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1016\/j.fss.2012.11.015","volume":"218","author":"R Diaconescu","year":"2013","unstructured":"Diaconescu, R.: Institutional semantics for many-valued logics. Fuzzy Sets Syst. 218, 32\u201352 (2013)","journal-title":"Fuzzy Sets Syst."},{"issue":"3","key":"24_CR9","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/BF01212304","volume":"4","author":"JL Fiadeiro","year":"1992","unstructured":"Fiadeiro, J.L., Maibaum, T.S.E.: Temporal theories as modularisation units for concurrent system specification. Formal Asp. Comput. 4(3), 239\u2013272 (1992)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"24_CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95\u2013146 (1992)","journal-title":"J. ACM"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BFb0013985","volume-title":"Temporal Logic","author":"V Goranko","year":"1994","unstructured":"Goranko, V.: Temporal logic with reference pointers. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol. 827, pp. 133\u2013148. Springer, Heidelberg (1994). doi: 10.1007\/BFb0013985"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Gorrieri, R., Rensink, A., Zamboni, M.A.: Action refinement. In: Handbook of Proacess Algebra, pp. 1047\u20131147. Elsevier (2000)","DOI":"10.1016\/B978-044482830-9\/50034-5"},{"key":"24_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"24_CR14","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"24_CR15","unstructured":"Havelund, K.: The Fork Calculus -Towards a Logic for Concurrent ML. Ph.D. thesis, DIKU, University of Copenhagen, Denmark (1994)"},{"key":"24_CR16","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1, 271\u2013281 (1972)","journal-title":"Acta Inf."},{"key":"24_CR17","series-title":"Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, Upper Saddle River (1985)"},{"key":"24_CR18","series-title":"Series in Computer Science","volume-title":"Software Development - A Rigorous Approach","author":"CB Jones","year":"1980","unstructured":"Jones, C.B.: Software Development - A Rigorous Approach. Series in Computer Science. Prentice Hall, Upper Saddle River (1980)"},{"issue":"2","key":"24_CR19","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0304-3975(91)90083-E","volume":"91","author":"P Knijnenburg","year":"1991","unstructured":"Knijnenburg, P., van Leeuwen, J.: On models for propositional dynamic logic. Theor. Comput. Sci. 91(2), 181\u2013203 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Third Annual Symposium on Logic in Computer Science, pp. 203\u2013210. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"24_CR21","unstructured":"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"},{"key":"24_CR22","volume-title":"Concurrency - State Models and Java Programs","author":"J Magee","year":"2006","unstructured":"Magee, J., Kramer, J.: Concurrency - State Models and Java Programs, 2nd edn. Wiley, Hoboken (2006)","edition":"2"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-642-28412-0_16","volume-title":"Recent Trends in Algebraic Development Techniques","author":"L O\u2019Reilly","year":"2012","unstructured":"O\u2019Reilly, 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\u2013269. Springer, Heidelberg (2012)"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). doi: 10.1007\/BFb0017309"},{"key":"24_CR25","unstructured":"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)"},{"key":"24_CR26","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets: An Introduction","author":"W Reisig","year":"1985","unstructured":"Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1985)"},{"issue":"1","key":"24_CR27","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1016\/j.tcs.2005.11.007","volume":"354","author":"M Roggenbach","year":"2006","unstructured":"Roggenbach, M.: CSP-CASL - a new integration of process algebra and algebraic specification. Theor. Comput. Sci. 354(1), 42\u201371 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"24_CR28","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF00283329","volume":"25","author":"D Sannella","year":"1988","unstructured":"Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited. Acta Inform. 25(3), 233\u2013281 (1988)","journal-title":"Acta Inform."},{"key":"24_CR29","series-title":"Monographs on TCS, an EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-17336-3","volume-title":"Foundations of Algebraic Specification and Formal Software Development","author":"D Sannella","year":"2012","unstructured":"Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs on TCS, an EATCS Series. Springer, Heidelberg (2012)"},{"key":"24_CR30","volume-title":"Program Development by Refinement: Case Studies Using the B Method","author":"E Sekerinski","year":"2012","unstructured":"Sekerinski, E., Sere, K.: Program Development by Refinement: Case Studies Using the B Method. Springer, Heidelberg (2012)"},{"key":"24_CR31","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"G Winskel","year":"1995","unstructured":"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\u2013148. Oxford University Press, Oxford (1995)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T16:30:07Z","timestamp":1568392207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}