{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T17:22:31Z","timestamp":1774977751380,"version":"3.50.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,29]],"date-time":"2021-07-29T00:00:00Z","timestamp":1627516800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,12]]},"abstract":"Abstract<\/jats:title>\n \n We propose\n \n \n \n \n \n \u03b5<\/mml:mi>\n \u2193<\/mml:mo>\n <\/mml:msup>\n \n (<\/mml:mo>\n \n D<\/mml:mi>\n \u2192<\/mml:mo>\n <\/mml:mover>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -logic as a formal foundation for the specification and\ndevelopment of event-based systems with data states. The framework is presented\nas an institution in the sense of Goguen and Burstall and the logic itself is\nparametrised by an underlying institution\n \n \n \n \n D<\/mml:mi>\n \u2192<\/mml:mo>\n <\/mml:mover>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n whose structures are used to\nmodel data states.\n \n \n \n \n \n \u03b5<\/mml:mi>\n \u2193<\/mml:mo>\n <\/mml:msup>\n \n (<\/mml:mo>\n \n D<\/mml:mi>\n \u2192<\/mml:mo>\n <\/mml:mover>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -logic is intended to cover a broad range of\nabstraction levels from abstract requirements specifications up to constructive\nspecifications. It uses modal diamond and box operators over complex actions\nadopted from dynamic logic. Atomic actions are pairs [inline-graphic not available: see fulltext] where\n e<\/jats:italic>\n is an event and\n \n \n \n \u03c8<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n a state transition predicate capturing the allowed\nreactions to the event. To write concrete specifications of recursive process\nstructures we integrate (control) state variables and binders of hybrid logic.\nThe semantic interpretation relies on event\/data transition systems. For the\npresentation of constructive specifications we propose operational event\/data\nspecifications allowing for familiar, diagrammatic representations by state\ntransition graphs. We show that\n \n \n \n \n \n \u03b5<\/mml:mi>\n \u2193<\/mml:mo>\n <\/mml:msup>\n \n (<\/mml:mo>\n \n D<\/mml:mi>\n \u2192<\/mml:mo>\n <\/mml:mover>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -logic is powerful enough to\ncharacterise the semantics of an operational specification by a single\n \n \n \n \n \n \u03b5<\/mml:mi>\n \u2193<\/mml:mo>\n <\/mml:msup>\n \n (<\/mml:mo>\n \n D<\/mml:mi>\n \u2192<\/mml:mo>\n <\/mml:mover>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -sentence. Thus the whole (formal) development process for\nevent\/data-based systems relies on\n \n \n \n \n \n \u03b5<\/mml:mi>\n \u2193<\/mml:mo>\n <\/mml:msup>\n \n (<\/mml:mo>\n \n D<\/mml:mi>\n \u2192<\/mml:mo>\n <\/mml:mover>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -logic and its semantics as a common\nbasis. It is supported by a variety of implementation constructors which can\nexpress, among others, event refinement and parallel composition. Due to the\ngenericity of the approach, it is also possible to change a data state\ninstitution during system development when needed. All steps of our formal\ntreatment are illustrated by a running example.\n <\/jats:p>","DOI":"10.1007\/s00165-021-00550-7","type":"journal-article","created":{"date-parts":[[2021,7,29]],"date-time":"2021-07-29T11:02:45Z","timestamp":1627556565000},"page":"1209-1248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Hybrid dynamic logic institutions for event\/data-based systems"],"prefix":"10.1145","volume":"33","author":[{"given":"Rolf","family":"Hennicker","sequence":"first","affiliation":[{"name":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Munich, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4050-3249","authenticated-orcid":false,"given":"Alexander","family":"Knapp","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Augsburg, Augsburg, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0646-2017","authenticated-orcid":false,"given":"Alexandre","family":"Madeira","sequence":"additional","affiliation":[{"name":"CIDMA, Mathematics Dep. of U. Aveiro, Aveiro, Portugal"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Abrial J-R (2013) Modeling in event-B: system and software engineering. Cambridge University Press"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bauer SS Hennicker R Wirsing M (2011) Interface theories concurrency and data. Theor Comput Sci 412(28):3101-3121","DOI":"10.1016\/j.tcs.2011.04.007"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bohrer B Platzer A (2018) A hybrid dynamic logic for hybrid-dynamic information flow. In: \nDawar A Gr\u00e4del E (eds)Proc 33rd ann ACM\/IEEE symp logic in computerscience pp 115-124. ACM","DOI":"10.1145\/3209108.3209151"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Br\u00e4uner T (2010) Hybrid logic and its proof-theory. Appl Log Ser. Springer","DOI":"10.1007\/978-94-007-0002-4"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"deAlfaro L Henzinger TA (2001) Interface automata. In: Min Tjoa A Gruhn V (eds) Proc8th Europ software engineering conf 9th ACM SIGSOFT intl. symp. foundations of software engineering pp 109-120. ACM","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_2_6_2","unstructured":"Diaconescu R (2008) Institution-independent model theory. Studies inuniversal logic. Birkh\u00e4user"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Diaconescu R Madeira A (2016) Encoding hybridized institutions into first-order logic. Math Struct Comput Sci 26(5):745-788","DOI":"10.1017\/S0960129514000383"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Diaconescu R Stefaneas PS (2007) Ultraproducts and possible worlds semantics in institutions.Theor Comput Sci 379(1-2):210-230","DOI":"10.1016\/j.tcs.2007.02.068"},{"key":"e_1_2_1_2_9_2","unstructured":"Fajardo R Finger M (2002) Non-normal modalisation. In: Balbiani P Suzuki N-Y Wolter F Zakharyaschev M (eds) Advances in modal logic 4 papers from the fourth conference on ``advances in modal logic '' held in Toulouse France 30 September-2 October 2002 pp83-96. King's College Publications"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Finger M Gabbay DM (1992) Adding a temporal dimension to a logic system. J Log Lang Inform 1(3):203-233","DOI":"10.1007\/BF00156915"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Farrell M Monahan R Power JF (2017) An institution for event-B.In: James P Roggenbach M (eds) Rev sel papers 23rd IFIP WG 1.3 intl ws recent trends in algebraic development techniques vol 10644 of lect notes comp sci pp 104-119. Springer","DOI":"10.1007\/978-3-319-72044-9_8"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Goguen JA Burstall RM (1992) Institutions: abstract model theory for specification and programming. J ACM 39:95-146","DOI":"10.1145\/147508.147524"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Groote JF Mousavi MR (2014) Modeling and analysis of communicatingsystems. MIT Press","DOI":"10.7551\/mitpress\/9946.001.0001"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Goranko V (1994) Temporal logic with reference pointers. In: Proc1st intl conf temporal logic vol 827 of lect notes comp sci pp133-148. Springer","DOI":"10.1007\/BFb0013985"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Gorrieri R Rensink A (2000) Action refinement. In: Bergstra JA Ponse A Smolka SA (eds) Handbook of process algebra pp 1047-1147. Elsevier","DOI":"10.1016\/B978-044482830-9\/50034-5"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Goguen JA Rosu G (2002) Institution morphisms. Formal Asp Comput 13(3-5):274-307","DOI":"10.1007\/s001650200013"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Harel D Kozen D Tiuryn J (2000) Dynamic logic. MIT Press","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Hennicker R Madeira A Knapp A (2019) A hybrid dynamic logic forevent\/data-based systems. In: H\u00e4hnle R van der Aalst WMP (eds) Proc 22nd intl conf fundamental approaches to software engineering vol 11424 of lect notes comp sci pp 79-97. Springer","DOI":"10.1007\/978-3-030-16722-6_5"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Knapp A Mossakowski T Roggenbach M Glauer M (2015) An institution for simple UML state machines. In: Egyed A Schaefer I (eds) Proc 18th intl conf fundamental approaches to software engineering vol 9033 of lect notes comp. sci pp 3-18. Springer","DOI":"10.1007\/978-3-662-46675-9_1"},{"key":"e_1_2_1_2_20_2","unstructured":"Lamport L (2003) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley"},{"key":"e_1_2_1_2_21_2","unstructured":"Lynch NA (2003) Input\/output automata: basic timed hybrid probabilistic dynamic \u2026. In: Amadio RM Lugiez D (eds) Proc 14th intl conf concurrency theory vol 2761 of lect notes comp sci pp 187-188. Springer"},{"key":"e_1_2_1_2_22_2","unstructured":"Mac Lane S (1998) Categories for the working mathematician 2nd edn. Springer"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Madeira A Barbosa LS Hennicker R Martins MA (2018) A logic for the stepwise development of reactive systems. Theor Comput Sci 744:78-96","DOI":"10.1016\/j.tcs.2018.03.004"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Mouelhi S Chouali S Mountassir H (2009) Refinement of interface automata strengthened by action semantics. Electron Notes Theor Comput Sci 253(1):111-126","DOI":"10.1016\/j.entcs.2009.09.031"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Mossakowski T Diaconescu R Tarlecki A (2009) What is a logic translation? Logica Universalis 3(1):95-124","DOI":"10.1007\/s11787-009-0005-2"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Martins MA Madeira A Diaconescu R Barbosa LS (2011) Hybridization of institutions. In: Corradini A Klin B C\u00eerstea C (eds) Proc 4th intl conf algebra and coalgebra in computer science vol 6859 of lect notes comp sci pp 283-297. Springer","DOI":"10.1007\/978-3-642-22944-2_20"},{"key":"e_1_2_1_2_27_2","unstructured":"Mossakowski T Maeder C L\u00fcttich K (2007) The heterogeneous tool\nset (Hets). In: Beckert B (ed) Proc 4th intl verification ws vol\n259 of CEUR ws proc CEUR-WS.org"},{"key":"e_1_2_1_2_28_2","unstructured":"OMG (Object Management Group) (2014) Object constraint language.Standard formal\/14-02-03. OMG"},{"key":"e_1_2_1_2_29_2","unstructured":"OMG (Object Management Group) (2017) Unified modeling language. Standard formal\/17-12-05. OMG"},{"key":"e_1_2_1_2_30_2","unstructured":"Poizat P Royer J-C (2006) A formal architectural description language based on symbolic transition systems and modal logic. J Univ Comput Sci 12(12):1741-1782"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Sannella D Tarlecki A (1988) Toward formal development of programs from algebraic specifications: implementations revisited. Acta Inf 25(3):233-281","DOI":"10.1007\/BF02737104"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Sannella D Tarlecki A (2012) Foundations of algebraic specification and formal software development. EATCS Monographs in Theoretical Computer Science. Springer","DOI":"10.1007\/978-3-642-17336-3"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"ter Beek MH Fantechi A Gnesi S Mazzanti F ( 2008) An action\/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: Leue S Merino P (eds) Sel papers 12th intl ws formal methods for industrial critical systems vol 4916 of lect notes comp sci pp 133-148. Springer","DOI":"10.1007\/978-3-540-79707-4_11"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00550-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00550-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00550-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00550-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,21]],"date-time":"2022-04-21T20:46:33Z","timestamp":1650573993000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00550-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":33,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["10.1007\/s00165-021-00550-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00550-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"12 December 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 May 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}