{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:48:52Z","timestamp":1764557332389},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s10703-014-0217-9","type":"journal-article","created":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T14:44:47Z","timestamp":1416581087000},"page":"226-261","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["Synthesising correct concurrent runtime monitors"],"prefix":"10.1007","volume":"46","author":[{"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[]},{"given":"Aldrin","family":"Seychell","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,11,20]]},"reference":[{"key":"217_CR1","doi-asserted-by":"crossref","unstructured":"Aceto L, Ing\u00f3lfsd\u00f3ttir A (1999) Testing Hennessy\u2013Milner logic with recursion. In: FoSSaCS\u201999. Springer, pp 41\u201355","DOI":"10.1007\/3-540-49019-1_4"},{"key":"217_CR2","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":"217_CR3","volume-title":"Programming Erlang","author":"J Armstrong","year":"2007","unstructured":"Armstrong J (2007) Programming Erlang. The Pragmatic Bookshelf, Armstrong"},{"key":"217_CR4","doi-asserted-by":"crossref","unstructured":"Bauer A, Falcone Y (2012) Decentralised LTL monitoring. In: Giannakopoulou D, Mry D (eds) FM. LNCS, vol 7436. Springer, pp 85\u2013100","DOI":"10.1007\/978-3-642-32759-9_10"},{"key":"217_CR5","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhar C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20:14:1\u201314:64","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"217_CR6","doi-asserted-by":"crossref","unstructured":"Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida N (2013) Monitoring networks through multiparty session types. In: FMOODS\/FORTE 2013. LNCS, vol 7892. Springer, pp 50\u201365.","DOI":"10.1007\/978-3-642-38592-6_5"},{"key":"217_CR7","doi-asserted-by":"crossref","unstructured":"Cao T-D, Phan-Quang T-T, Felix P, Castanet R (2010) Automated runtime verification for web services. In: ICWS. IEEE, pp 76\u201382","DOI":"10.1109\/ICWS.2010.19"},{"key":"217_CR8","unstructured":"Carlsson R (2001) An introduction to Core Erlang. In: PLI\u201901 (Erlang Workshop)"},{"key":"217_CR9","doi-asserted-by":"crossref","unstructured":"Cassar I, Francalanza A (2014) On synchronous and asynchronous monitor instrumentation for actor-based systems. In: FOCLASA, EPTCS (to appear)","DOI":"10.4204\/EPTCS.175.4"},{"key":"217_CR10","unstructured":"Cerone A, Hennessy M (2010) Process behaviour: formulae vs. tests. In: EXPRESS\u201910, vol 41 EPTCS, pp 31\u201345"},{"key":"217_CR11","volume-title":"Erlang programming","author":"F Cesarini","year":"2009","unstructured":"Cesarini F, Thompson S (2009) Erlang programming. O\u2019Reilly, Sebastopol"},{"key":"217_CR12","doi-asserted-by":"crossref","unstructured":"Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: ALP. LNCS, vol 623. Springer-Verlag, pp 474\u2013486","DOI":"10.1007\/3-540-55719-9_97"},{"key":"217_CR13","volume-title":"Model checking","author":"E Clarke Jr","year":"1999","unstructured":"Clarke E Jr, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"217_CR14","unstructured":"Colombo C, Francalanza A, Gatt R (2011) Elarva: a monitoring tool for Erlang. In: RV. LNCS, vol 7186. Springer, pp 370\u2013374"},{"key":"217_CR15","doi-asserted-by":"crossref","unstructured":"Colombo C, Francalanza A, Grima I (2012) Simplifying contract-violating traces. In: FLACOS, EPTCS, vol 94, pp 11\u201320","DOI":"10.4204\/EPTCS.94.2"},{"key":"217_CR16","doi-asserted-by":"crossref","unstructured":"Colombo C, Francalanza A, Mizzi R, Pace GJ (2012) polylarva: runtime verification with configurable resource-aware monitoring boundaries. In: SEFM, pp 218\u2013232","DOI":"10.1007\/978-3-642-33826-7_15"},{"key":"217_CR17","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo B, Sankaranarayanan S, S\u00e1nchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z. (2005) Lola: runtime monitoring of synchronous systems. In: TIME, IEEE","DOI":"10.1109\/TIME.2005.26"},{"key":"217_CR18","doi-asserted-by":"crossref","unstructured":"Falcone Y, Jaber M, Nguyen T-H, Bozga M, Bensalem S. (2011) Runtime verification of component-based systems. In: SEFM. LNCS, vol 7041. Springer, pp 204\u2013220","DOI":"10.1007\/978-3-642-24690-6_15"},{"key":"217_CR19","doi-asserted-by":"crossref","unstructured":"Francalanza A, Seychell A (2013) Synthesising correct concurrent runtime monitors in Erlang. Technical Report CS2013-01, University of Malta. https:\/\/www.cs.um.edu.mt\/svrg\/papers.html . Accessed Jan","DOI":"10.1007\/978-3-642-40787-1_7"},{"issue":"5\u20137","key":"217_CR20","first-page":"186","volume":"82","author":"A Francalanza","year":"2013","unstructured":"Francalanza A, Gauci A, Pace GJ (2013) Distributed System contract monitoring. JLAP 82(5\u20137):186\u2013215","journal-title":"JLAP"},{"key":"217_CR21","unstructured":"Francalanza A, Seychell A, Cassar I. DetectEr. https:\/\/bitbucket.org\/casian\/detecter2.0"},{"key":"217_CR22","unstructured":"Fredlund L-\u00c5 (2001) A framework for reasoning about Erlang code. PhD thesis, Royal Institute of Technology, Stockholm, Sweden"},{"issue":"2","key":"217_CR23","first-page":"181","volume":"55","author":"M Geilen","year":"2001","unstructured":"Geilen M (2001) On the construction of monitors for temporal logic properties. ENTCS 55(2):181\u2013199","journal-title":"ENTCS"},{"key":"217_CR24","volume-title":"A distributed picalculus","author":"M Hennessy","year":"2008","unstructured":"Hennessy M (2008) A distributed picalculus. Cambridge University Proess, Cambridge"},{"key":"217_CR25","doi-asserted-by":"crossref","unstructured":"Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32(1):137\u2013161","DOI":"10.1145\/2455.2460"},{"key":"217_CR26","unstructured":"Hewitt C, Bishop P, Steiger R (1973) A universal modular actor formalism for artificial intelligence. In: IJCAI, Morgan Kaufmann, pp 235\u2013245"},{"key":"217_CR27","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. TCS 27:333\u2013354","journal-title":"TCS"},{"key":"217_CR28","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1990) A hierarchy of temporal properties (invited paper, 1989). In: PODC, ACM, pp 377\u2013410","DOI":"10.1145\/93385.93442"},{"issue":"3","key":"217_CR29","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2012","unstructured":"Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2012) An overview of the MOP runtime verification framework. STTT 14(3):249\u2013289","journal-title":"STTT"},{"key":"217_CR30","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and concurrency. Prentice-Hall Inc, Upper Saddle River"},{"key":"217_CR31","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0304-3975(93)90156-N","volume":"114","author":"R Milner","year":"1993","unstructured":"Milner R, Parrow J, Walker D (1993) Modal logics for mobile processes. TCS 114:149\u2013171","journal-title":"TCS"},{"key":"217_CR32","doi-asserted-by":"crossref","unstructured":"Nicola RD, Hennessy MCB (1984) Testing equivalences for processes, TCS, pp 83\u2013133","DOI":"10.1016\/0304-3975(84)90113-0"},{"issue":"2","key":"217_CR33","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.ic.2006.06.002","volume":"205","author":"A Rensink","year":"2007","unstructured":"Rensink A, Vogler W (2007) Fair testing. Inf Comput 205(2):125\u2013198","journal-title":"Inf Comput"},{"key":"217_CR34","unstructured":"Sen K, Rosu G, Agha G (2004) Generating optimal linear temporal logic monitors by coinduction. In: ASIAN. LNCS, vol 2896. Springer-Verlag, pp 260\u2013275"},{"key":"217_CR35","doi-asserted-by":"crossref","unstructured":"Sen K, Vardhan A, Agha G, Ro\u015fu G (2004) Efficient decentralized monitoring of safety in distributed systems. ICSE, pp 418\u2013427","DOI":"10.1109\/ICSE.2004.1317464"},{"key":"217_CR36","doi-asserted-by":"crossref","unstructured":"Svensson H, Fredlund L-\u00c5, Benac Earle C (2010) A unified semantics for future erlang. In: Erlang Workshop, ACM, pp 23\u201332","DOI":"10.1145\/1863509.1863514"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0217-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0217-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0217-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T17:48:56Z","timestamp":1566064136000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0217-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,20]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["217"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0217-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,20]]}}}