{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T22:22:40Z","timestamp":1773526960531,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T00:00:00Z","timestamp":1490313600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001840","name":"Icelandic Centre for Research","doi-asserted-by":"publisher","award":["163406-051"],"award-info":[{"award-number":["163406-051"]}],"id":[{"id":"10.13039\/501100001840","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10703-017-0273-z","type":"journal-article","created":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T09:43:56Z","timestamp":1490348636000},"page":"87-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":41,"title":["Monitorability for the Hennessy\u2013Milner logic with recursion"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[]},{"given":"Luca","family":"Aceto","sequence":"additional","affiliation":[]},{"given":"Anna","family":"Ingolfsdottir","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,24]]},"reference":[{"key":"273_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in event-B: system and software engineering","author":"J\u00a0R Abrial","year":"2010","unstructured":"Abrial J\u00a0R (2010) Modeling in event-B: system and software engineering. Cambridge University Press, Cambridge"},{"key":"273_CR2","doi-asserted-by":"crossref","unstructured":"Aceto L, Ing\u00f3lfsd\u00f3ttir A (1999) Testing Hennessy\u2013Milner logic with recursion. In: FoSSaCS\u201999. Springer, Berlin, pp 41\u201355","DOI":"10.1007\/3-540-49019-1_4"},{"key":"273_CR3","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 KG, Srba J (2007) Reactive systems: modelling, specification and verification. Cambridge University Press, New York"},{"key":"273_CR4","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Chimento JM, Pace GJ, Schneider G (2015) A specification language for static and runtime verification of data and control properties. In: FM 2015, vol 9109. Springer, Berlin, pp 108\u2013125","DOI":"10.1007\/978-3-319-19249-9_8"},{"key":"273_CR5","doi-asserted-by":"crossref","unstructured":"Andersen JR, Andersen N, Enevoldsen S, Hansen MM, Larsen KG, Olesen SR, Srba J, Wortmann J (2015) CAAL: concurrency workbench, Aalborg Edition. In: ICTAC. Springer, Berlin, pp 573\u2013582","DOI":"10.1007\/978-3-319-25150-9_33"},{"key":"273_CR6","doi-asserted-by":"crossref","unstructured":"Attard DP, Francalanza A (2016) A monitoring tool for a branching-time logic. In: RV, vol 10012 of LNCS. Springer, Berlin, pp 473\u2013481","DOI":"10.1007\/978-3-319-46982-9_31"},{"key":"273_CR7","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, New York"},{"key":"273_CR8","doi-asserted-by":"crossref","unstructured":"Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard DE (2012) Quantified event automata: towards expressive and efficient runtime monitors. In: FM, vol 7436 of LNCS. Springer, Berlin, pp 68\u201384","DOI":"10.1007\/978-3-642-32759-9_9"},{"key":"273_CR9","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: VMCAI, vol 2937 of LNCS, Springer, Berlin, pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"273_CR10","doi-asserted-by":"crossref","unstructured":"Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: RV, vol 4839 of LNCS. Springer, Berlin, pp 126\u2013138","DOI":"10.1007\/978-3-540-77395-5_11"},{"issue":"3","key":"273_CR11","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer A, Leucker M, Schallhart C (2010) Comparing LTL semantics for runtime verification. Log Comput 20(3):651\u2013674","journal-title":"Log Comput"},{"issue":"4","key":"273_CR12","first-page":"14","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. Softw Eng Methodol 20(4):14","journal-title":"Softw Eng Methodol"},{"key":"273_CR13","first-page":"54","volume":"175","author":"I Cassar","year":"2014","unstructured":"Cassar I, Francalanza A (2014) On synchronous and asynchronous monitor instrumentation for actor systems. FOCLASA 175:54\u201368","journal-title":"FOCLASA"},{"key":"273_CR14","doi-asserted-by":"crossref","unstructured":"Cassar I, Francalanza A (2015) Runtime adaptation for actor systems. In: Runtime verification (RV), vol 9333 of LNCS. Springer, Berlin, pp 38\u201354","DOI":"10.1007\/978-3-319-23820-3_3"},{"key":"273_CR15","doi-asserted-by":"crossref","unstructured":"Cassar I, Francalanza A (2016) On implementing a monitor-oriented programming framework for actor systems. In: iFM, vol 9681 of LNCS, pp 176\u2013192","DOI":"10.1007\/978-3-319-33693-0_12"},{"key":"273_CR16","doi-asserted-by":"crossref","unstructured":"Cerone A, Hennessy M (2010) Process behaviour: formulae versus tests. In: EXPRESS, vol 41 of EPTCS, pp 31\u201345","DOI":"10.4204\/EPTCS.41.3"},{"key":"273_CR17","doi-asserted-by":"crossref","unstructured":"Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: ALP LNCS. Springer, Berlin, pp 474\u2013486","DOI":"10.1007\/3-540-55719-9_97"},{"key":"273_CR18","doi-asserted-by":"crossref","unstructured":"Cini C, Francalanza A (2015) An LTL proof system for runtime verification. In: TACAS, vol 9035. Springer, Berlin, pp 581\u2013595","DOI":"10.1007\/978-3-662-46681-0_54"},{"key":"273_CR19","volume-title":"Model checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke EM Jr, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"273_CR20","unstructured":"Della\u00a0Monica D, Francalanza A (2015) Towards a hybrid approach to software verification. In: NWPT, number SCS16001 in RUTR. RU Press, pp 51\u201354"},{"key":"273_CR21","doi-asserted-by":"crossref","unstructured":"Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: CAV, vol 2725 of LNCS. Springer, Berlin, pp 27\u201339","DOI":"10.1007\/978-3-540-45069-6_3"},{"issue":"3","key":"273_CR22","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone Y, Fernandez J-C, Mounier L (2012) What can you verify and enforce at runtime? Softw Tools Technol Transf 14(3):349\u2013382","journal-title":"Softw Tools Technol Transf"},{"key":"273_CR23","unstructured":"Francalanza A (2016) A theory of monitors (extended abstract). In: FoSSaCS, vol 9634 of LNCS. Springer, Berlin, pp 145\u2013161"},{"key":"273_CR24","doi-asserted-by":"crossref","unstructured":"Francalanza A, Aceto L, Ing\u00f3lfsd\u00f3ttir A (2015) On verifying Hennessy\u2013Milner logic with recursion at runtime. In: RV, vol 9333 of LNCS, pp 71\u201386","DOI":"10.1007\/978-3-319-23820-3_5"},{"issue":"5\u20137","key":"273_CR25","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1016\/j.jlap.2013.04.001","volume":"82","author":"A Francalanza","year":"2013","unstructured":"Francalanza A, Gauci A, Pace GJ (2013) Distributed system contract monitoring. J Log Algebr Program 82(5\u20137):186\u2013215","journal-title":"J Log Algebr Program"},{"issue":"3","key":"273_CR26","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2015","unstructured":"Francalanza A, Seychell A (2015) Synthesising correct concurrent runtime monitors. Form Methods Syst Des 46(3):226\u2013261","journal-title":"Form Methods Syst Des"},{"key":"273_CR27","doi-asserted-by":"crossref","unstructured":"Geilen M (2001) On the construction of monitors for temporal logic properties. In: RV, vol 55 of ENTCS, pp 181\u2013199","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"273_CR28","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs"},{"key":"273_CR29","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen D (1983) Results on the propositional $$\\mu $$ \u03bc -calculus. Theor Comput Sci 27:333\u2013354","journal-title":"Theor Comput Sci"},{"issue":"2","key":"273_CR30","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"KG Larsen","year":"1990","unstructured":"Larsen KG (1990) Proof systems for satisfiability in Hennessy\u2013Milner logic with recursion. Theor Comput Sci 72(2):265\u2013288","journal-title":"Theor Comput Sci"},{"issue":"5","key":"273_CR31","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebraic Program 78(5):293\u2013303","journal-title":"J Log Algebraic Program"},{"issue":"1","key":"273_CR32","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna Z, Pnueli A (1991) Completing the temporal picture. Theor Comput Sci 83(1):97\u2013130","journal-title":"Theor Comput Sci"},{"key":"273_CR33","volume-title":"A calculus of communicating systems","author":"R Milner","year":"1982","unstructured":"Milner R (1982) A calculus of communicating systems. Springer, Berlin"},{"key":"273_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM, vol 4085. Springer, Berlin, pp 573\u2013586","DOI":"10.1007\/11813040_38"},{"key":"273_CR35","doi-asserted-by":"crossref","unstructured":"Sen K, Rosu G, Agha G (2003) Generating optimal linear temporal logic monitors by coinduction. In: ASIAN, vol 2896 of LNCS, Springer, Berlin, pp 260\u2013275","DOI":"10.1007\/978-3-540-40965-6_17"},{"key":"273_CR36","doi-asserted-by":"crossref","unstructured":"Shi J, Lahiri SK, Chandra R, Challen G. Wireless protocol validation under uncertainty. In: RV","DOI":"10.1007\/978-3-319-46982-9_22"},{"key":"273_CR37","unstructured":"detectEr Project. http:\/\/www.cs.um.edu.mt\/svrg\/Tools\/detectEr\/"},{"key":"273_CR38","doi-asserted-by":"crossref","unstructured":"Vella A, Francalanza A (2016) Preliminary results towards contract monitorability. In: PrePost, vol 208 of EPTCS, pp 54\u201363","DOI":"10.4204\/EPTCS.208.5"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0273-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0273-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0273-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:58:38Z","timestamp":1750179518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0273-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,24]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["273"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0273-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,24]]}}}