{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:53Z","timestamp":1762459313755},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319238197"},{"type":"electronic","value":"9783319238203"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-23820-3_5","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T14:21:39Z","timestamp":1442672499000},"page":"71-86","source":"Crossref","is-referenced-by-count":18,"title":["On Verifying Hennessy-Milner Logic with Recursion at Runtime"],"prefix":"10.1007","author":[{"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Aceto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Ingolfsdottir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,15]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-49019-1_4","volume-title":"Foundations of Software Science and Computation Structures","author":"L Aceto","year":"1999","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: Testing Hennessy-Milner logic with recursion. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 41\u201355. Springer, Heidelberg (1999)"},{"key":"5_CR3","doi-asserted-by":"publisher","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, New York (2007)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126\u2013138. Springer, Heidelberg (2007)"},{"issue":"3","key":"5_CR6","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Logic Comput. 20(3), 651\u2013674 (2010)","journal-title":"Logic Comput."},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM 20(4), 14 (2011)","journal-title":"TOSEM"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor systems. In: FOCLASA, vol. 175, pp. 54\u201368 (2014)","DOI":"10.4204\/EPTCS.175.4"},{"key":"5_CR9","unstructured":"Cerone, A., Hennessy, M.: Process behaviour: formulae vs. tests. In: EXPRESS. EPTCS, vol. 41, pp. 31\u201345 (2010)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, Languages and Programming","author":"E Chang","year":"1992","unstructured":"Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474\u2013486. Springer, Heidelberg (1992)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1007\/978-3-662-46681-0_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Cini","year":"2015","unstructured":"Cini, C., Francalanza, A.: An LTL proof system for runtime verification. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 581\u2013595. Springer, Heidelberg (2015)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G., Schneider, G.: LARVA \u2013 safer monitoring of real-time Java programs (Tool paper). In: SEFM, pp. 33\u201337 (2009)","DOI":"10.1109\/SEFM.2009.13"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"issue":"3","key":"5_CR14","doi-asserted-by":"publisher","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.: What can you verify and enforce at runtime? STTT 14(3), 349\u2013382 (2012)","journal-title":"STTT"},{"issue":"5\u20137","key":"5_CR15","first-page":"186","volume":"82","author":"A Francalanza","year":"2013","unstructured":"Francalanza, A., Gauci, A., Pace, G.J.: Distributed system contract monitoring. JLAP 82(5\u20137), 186\u2013215 (2013)","journal-title":"JLAP"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. In: Formal Methods in System Design (FMSD), pp. 1\u201336 (2014)","DOI":"10.1007\/s10703-014-0217-9"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Geilen, M.: On the construction of monitors for temporal logic properties. In: RV. ENTCS, vol. 55, pp. 181\u2013199 (2001)","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"5_CR18","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \n                      \n                        \n                      \n                      $$\\mu $$\n                      \n                        \n                          \u03bc\n                        \n                      \n                    -calculus. TCS 27, 333\u2013354 (1983)","journal-title":"TCS"},{"issue":"5","key":"5_CR20","first-page":"293","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. JLAP 78(5), 293\u2013303 (2009)","journal-title":"JLAP"},{"issue":"1","key":"5_CR21","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. TCS 83(1), 97\u2013130 (1991)","journal-title":"TCS"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1982)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/11813040_38","volume-title":"FM 2006: Formal Methods","author":"A Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573\u2013586. Springer, Heidelberg (2006)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/978-3-540-40965-6_17","volume-title":"Advances in Computing Science","author":"K Sen","year":"2003","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Generating optimal linear temporal logic monitors by coinduction. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 260\u2013275. Springer, Heidelberg (2003)"},{"key":"5_CR25","unstructured":"detectEr Project. \n                      http:\/\/www.cs.um.edu.mt\/svrg\/Tools\/detectEr\/"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23820-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:43:16Z","timestamp":1559263396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-23820-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319238197","9783319238203"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23820-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}