{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T08:12:01Z","timestamp":1768551121569,"version":"3.49.0"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,6,30]],"date-time":"2021-06-30T00:00:00Z","timestamp":1625011200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,30]],"date-time":"2021-06-30T00:00:00Z","timestamp":1625011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10009-021-00625-z","type":"journal-article","created":{"date-parts":[[2021,6,30]],"date-time":"2021-06-30T18:03:05Z","timestamp":1625076185000},"page":"579-600","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["What can we monitor over unreliable channels?"],"prefix":"10.1007","volume":"23","author":[{"given":"Sean","family":"Kauffman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Fischmeister","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,30]]},"reference":[{"key":"625_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Baier, C., Iyer, P., Jonsson, B.: Reasoning about probabilistic lossy channel systems. In: International Conference on Concurrency Theory (CONCUR\u201920), LNCS, vol. 1877, pp. 320\u2013333. Springer (2000)","DOI":"10.1007\/3-540-44618-4_24"},{"issue":"2","key":"625_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91\u2013101 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0053","journal-title":"Inf. Comput."},{"key":"625_CR3","doi-asserted-by":"publisher","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K. (2019). Adventures in monitorability: from branching to linear time and back again. In: Symposium on Principles of Programming Languages (POPL\u201919), vol.\u00a03. ACM Press. https:\/\/doi.org\/10.1145\/3290365","DOI":"10.1145\/3290365"},{"key":"625_CR4","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Computer Security Foundations Symposium (CSF\u201916), pp. 239\u2013252. IEEE (2016). https:\/\/doi.org\/10.1109\/CSF.2016.24","DOI":"10.1109\/CSF.2016.24"},{"issue":"4","key":"625_CR5","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0020-0190(86)90132-8","volume":"23","author":"B Alpern","year":"1986","unstructured":"Alpern, B., Demers, A.J., Schneider, F.B.: Safety without stuttering. Inf. Process. Lett. 23(4), 177\u2013180 (1986). https:\/\/doi.org\/10.1016\/0020-0190(86)90132-8","journal-title":"Inf. Process. Lett."},{"key":"625_CR6","unstructured":"ARM Limited (2019) Embedded trace macrocell architecture specification.http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.ihi0014q\/"},{"key":"625_CR7","doi-asserted-by":"publisher","unstructured":"Baader, F., Bauer, A., Tiu, A.: Matching trace patterns with regular policies. In: International Conference on Language and Automata Theory and Applications (LATA\u201909), LNAI, vol .5457, pp. 105\u2013116. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00982-2_9","DOI":"10.1007\/978-3-642-00982-2_9"},{"key":"625_CR8","doi-asserted-by":"publisher","unstructured":"Baier, C., Engelen, B.: Establishing Qualitative Properties for Probabilistic Lossy Channel Systems, LNCS, vol. 1601, pp 34\u201352. Springer (1999) https:\/\/doi.org\/10.1007\/3-540-48778-6_3","DOI":"10.1007\/3-540-48778-6_3"},{"key":"625_CR9","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Verification, Model Checking, and Abstract Interpretation (VMCAI\u201904), LNCS, vol. 2937, pp. 44\u201357. Springer (2009)","DOI":"10.1007\/978-3-540-24622-0_5"},{"issue":"5","key":"625_CR10","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"KA Bartlett","year":"1969","unstructured":"Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260\u2013261 (1969). https:\/\/doi.org\/10.1145\/362946.362970","journal-title":"Commun. ACM"},{"key":"625_CR11","doi-asserted-by":"publisher","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: Runtime verification of temporal properties over out-of-order data streams. In: Computer Aided Verification (CAV\u201917), LNCS, vol. 10426, pp. 356\u2013376. Springer(2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_18","DOI":"10.1007\/978-3-319-63387-9_18"},{"key":"625_CR12","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Klaedtke, F., Marinovic, S., Zalinescu, E.: Monitoring compliance policies over incomplete and disagreeing logs. In: International Conference on Runtime Verification (RV\u201912), LNCS, vol. 7687, pp. 151\u2013167. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_17","DOI":"10.1007\/978-3-642-35632-2_17"},{"key":"625_CR13","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201906), LNCS, vol. 4337, pp. 260\u2013272. Springer (2006). https:\/\/doi.org\/10.1007\/11944836_25","DOI":"10.1007\/11944836_25"},{"issue":"3","key":"625_CR14","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. J. Logic Comput. 20(3), 651\u2013674 (2010). https:\/\/doi.org\/10.1093\/logcom\/exn075","journal-title":"J. Logic Comput."},{"key":"625_CR15","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1-14:64 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","DOI":"10.1145\/2000799.2000800"},{"key":"625_CR16","unstructured":"Belina, F., Hogrefe, D., Sarma, A.: SDL with Applications from Protocol Specification. Prentice-Hall, Inc (1991)"},{"issue":"2","key":"625_CR17","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983). https:\/\/doi.org\/10.1145\/322374.322380","journal-title":"J. ACM"},{"issue":"1","key":"625_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0169-7552(87)90084-5","volume":"14","author":"S Budkowski","year":"1987","unstructured":"Budkowski, S., Dembinski, P.: An introduction to Estelle: a specification language for distributed systems. Comput. Netw. ISDN Syst. 14(1), 3\u201323 (1987). https:\/\/doi.org\/10.1016\/0169-7552(87)90084-5","journal-title":"Comput. Netw. ISDN Syst."},{"issue":"1","key":"625_CR19","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G C\u00e9c\u00e9","year":"1996","unstructured":"C\u00e9c\u00e9, G., Finkel, A., Iyer, S.P.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124(1), 20\u201331 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0003","journal-title":"Inf. Comput."},{"key":"625_CR20","doi-asserted-by":"crossref","unstructured":"Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: International Colloquium on Automata, Languages and Programming (ICALP\u201992), LNCS, vol. 623, pp. 474\u2013486. Springer (1992)","DOI":"10.1007\/3-540-55719-9_97"},{"key":"625_CR21","doi-asserted-by":"publisher","unstructured":"Chen, Z., Wu. Y., Wei. O., Sheng. B.: Deciding weak monitorability for runtime verification. In: International Conference on Software Engineering (ICSE\u201918), pp. 163\u2013164. ACM Press (2018). https:\/\/doi.org\/10.1145\/3183440.3195077","DOI":"10.1145\/3183440.3195077"},{"key":"625_CR22","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: International Conference on Runtime Verification (RV\u201919), LNCS, vol. 11757, pp. 165\u2013184. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_10","DOI":"10.1007\/978-3-030-32079-9_10"},{"key":"625_CR23","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: International Conference on Principles of Security and Trust (POST\u201914), LNCS, vol. 8414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"625_CR24","doi-asserted-by":"publisher","unstructured":"d\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of $$\\omega $$-languages. In: Computer Aided Verification (CAV\u201905), LNCS, vol. 3576, pp. 364\u2013378. Springer (2005). https:\/\/doi.org\/10.1007\/11513988_36","DOI":"10.1007\/11513988_36"},{"key":"625_CR25","doi-asserted-by":"publisher","unstructured":"Diekert, V., Gastin, P.: First-Order Definable Languages, pp. 261\u2013306. Amsterdam University Press (2008). https:\/\/doi.org\/10.2307\/j.ctt46mv83.12","DOI":"10.2307\/j.ctt46mv83.12"},{"key":"625_CR26","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.tcs.2014.02.052","volume":"537","author":"V Diekert","year":"2014","unstructured":"Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theoret. Comput. Sci. 537, 29\u201341 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.02.052","journal-title":"Theoret. Comput. Sci."},{"key":"625_CR27","doi-asserted-by":"publisher","unstructured":"Diekert, V., Muscholl, A., Walukiewicz, I.: A note on monitors and b\u00fcchi automata. In: International Colloquium on Theoretical Aspects of Computing (ICTAC\u201915), LNCS, vol. 9399, pp. 39\u201357. Springer (2015).https:\/\/doi.org\/10.1007\/978-3-319-25150-9_3","DOI":"10.1007\/978-3-319-25150-9_3"},{"key":"625_CR28","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering (ICSE\u201999), pp. 411\u2013420. ACM Press (1999)","DOI":"10.1145\/302405.302672"},{"key":"625_CR29","doi-asserted-by":"publisher","unstructured":"Edwards, C.D., Bell, D.J., Gladden, R.E., Ilott, P.A., Jedrey, T.C., Johnston, M.D., Maxwell, J.L., Mendoza, R., McSmith, G.W., Potts, C.L., Schratz, B.C., Shihabi, M.M., Srinivasan, J.M., Varghese, P., Sanders, S.S., Denis, M.: Relay support for the mars science laboratory mission. In: Conference on Aerospace, pp. 1\u201314. IEEE (2013). https:\/\/doi.org\/10.1109\/AERO.2013.6497325","DOI":"10.1109\/AERO.2013.6497325"},{"key":"625_CR30","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime verification of safety-progress properties. In: International Conference on Runtime Verification (RV\u201909), LNCS, vol. 5779, pp. 40\u201359. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04694-0_4","DOI":"10.1007\/978-3-642-04694-0_4"},{"issue":"3","key":"625_CR31","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? Int. J. Softw. Tools Technol. Transf. 14(3), 349\u2013382 (2012). https:\/\/doi.org\/10.1007\/s10009-011-0196-8","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"625_CR32","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BF02277857","volume":"7","author":"A Finkel","year":"1994","unstructured":"Finkel, A.: Decidability of the termination problem for completely specified protocols. Distrib. Comput. 7(3), 129\u2013135 (1994). https:\/\/doi.org\/10.1007\/BF02277857","journal-title":"Distrib. Comput."},{"issue":"1","key":"625_CR33","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10703-017-0273-z","volume":"51","author":"A Francalanza","year":"2017","unstructured":"Francalanza, A., Aceto, L., Ingolfsdottir, A.: Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87\u2013116 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0273-z","journal-title":"Formal Methods Syst. Des."},{"key":"625_CR34","doi-asserted-by":"publisher","unstructured":"Garg, D., Jia, L., Datta, A.: olicy auditing over incomplete logs: Theory, implementation and applications. In: Conference on Computer and Communications Security (CCS\u201911), pp. 151\u2013162. ACM Press (2011). https:\/\/doi.org\/10.1145\/2046707.2046726","DOI":"10.1145\/2046707.2046726"},{"key":"625_CR35","doi-asserted-by":"publisher","unstructured":"Gondi, K., Patel, Y., Sistla, A.P.: Monitoring the full range of $$\\omega $$-regular properties of stochastic systems. In: Verification, Model Checking, and Abstract Interpretation (VMCAI\u201909), LNCS, vol. 5403, pp. 105\u2013119. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_12","DOI":"10.1007\/978-3-540-93900-9_12"},{"key":"625_CR36","doi-asserted-by":"publisher","unstructured":"Halbwachs, N., H\u00e9ry, J.F., Laleuf, J.C., Nicollin, X.: Stability of discrete sampled systems. In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u201920), LNCS, vol. 1926, pp. 1\u201311. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-45352-0_1","DOI":"10.1007\/3-540-45352-0_1"},{"key":"625_CR37","unstructured":"Hopcroft, J.E., Karp, R.M.: A Linear Algorithm for Testing Equivalence of Finite Automata, Technical Report. Cornell University (1971)"},{"key":"625_CR38","unstructured":"ISO, IEC 13239:2002, : Information Technology\u2014Telecommunications and Information Exchange Between Systems\u2014High-Level Data Link Control (HDLC) Procedures Standard, International Organization for Standardization, Geneva, CH (2002)"},{"key":"625_CR39","doi-asserted-by":"publisher","unstructured":"Iyer, P., Narasimha, M.: Probabilistic lossy channel systems. In: International Joint Conference on Theory and Practice of Software Development (TAPSOFT\u201997), LNCS, vol. 1214, pp. 667\u2013681. Springer(1997). https:\/\/doi.org\/10.1007\/BFb0030633","DOI":"10.1007\/BFb0030633"},{"key":"625_CR40","doi-asserted-by":"publisher","unstructured":"Joshi, Y., Tchamgoue, G.M., Fischmeister, S.: Runtime verification of LTL on lossy traces. In: Symposium on Applied Computing (SAC\u201917), pp. 1379\u20131386. ACM Press (2017). https:\/\/doi.org\/10.1145\/3019612.3019827","DOI":"10.1145\/3019612.3019827"},{"key":"625_CR41","doi-asserted-by":"publisher","unstructured":"Kauffman, S., Havelund, K., Fischmeister, S.: Monitorability over unreliable channels. In: International Conference on Runtime Verification (RV\u201919), LNCS, vol. 11757, pp. 256\u2013272. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-32079-9_15","DOI":"10.1007\/978-3-030-32079-9_15"},{"issue":"3","key":"625_CR42","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001a). https:\/\/doi.org\/10.1023\/A:1011254632723","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"625_CR43","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic 2(3), 408\u2013429 (2001b). https:\/\/doi.org\/10.1145\/377978.377993","journal-title":"ACM Trans. Comput. Logic"},{"key":"625_CR44","first-page":"657","volume":"83","author":"L Lamport","year":"1983","unstructured":"Lamport, L.: What good is temporal logic? IFIP Congress Elsevier Inf. Process. 83, 657\u2013668 (1983)","journal-title":"IFIP Congress Elsevier Inf. Process."},{"key":"625_CR45","doi-asserted-by":"publisher","unstructured":"Leucker, M., S\u00e1nchez, C., Scheffel, T., Schmitz, M., Thoma, D.: Runtime verification for timed event streams with partial information. In: International Conference on Runtime Verification (RV\u201919), LNCS, vol. 11757, pp. 273\u2013291. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_16","DOI":"10.1007\/978-3-030-32079-9_16"},{"key":"625_CR46","doi-asserted-by":"publisher","unstructured":"Li, M., Liu, M., Ding, L., Rundensteiner, E.A., Mani, M.: Event stream processing with out-of-order data arrival. In: International Conference on Distributed Computing Systems Workshops (ICDCSW\u201907), pp. 67\u201367. IEEE(2007). https:\/\/doi.org\/10.1109\/ICDCSW.2007.35","DOI":"10.1109\/ICDCSW.2007.35"},{"key":"625_CR47","doi-asserted-by":"publisher","unstructured":"Lomuscio, A., Penczek, W., Qu, H.: Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In: Interantional Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201910), pp. 659\u2013666. ACM Press (2010). https:\/\/doi.org\/10.3233\/FI-2010-276","DOI":"10.3233\/FI-2010-276"},{"key":"625_CR48","doi-asserted-by":"publisher","unstructured":"Lozes, \u00c9., Villard, J.L.: Reliable contracts for unreliable half-duplex communications. In: Web Services and Formal Methods (WS-FM\u201912), LNCS, vol. 7176, pp. 2\u201316. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-29834-9_2","DOI":"10.1007\/978-3-642-29834-9_2"},{"key":"625_CR49","doi-asserted-by":"publisher","unstructured":"Peled, D., Havelund, K.: Refining the safety\u2013liveness classification of temporal properties according to monitorability. In: Models, Mindsets, Meta: The What, the How, and the Why Not? Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, LNCS, vol. 11200, pp. 218\u2013234. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-22348-9_14","DOI":"10.1007\/978-3-030-22348-9_14"},{"issue":"5","key":"625_CR50","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett. 63(5), 243\u2013246 (1997). https:\/\/doi.org\/10.1016\/S0020-0190(97)00133-6","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"625_CR51","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1023\/B:TELS.0000014793.19622.0e","volume":"25","author":"W Peng","year":"2004","unstructured":"Peng, W., Makki, K.: Lossy communicating finite state machines. Telecommun. Syst. 25(3), 433\u2013448 (2004). https:\/\/doi.org\/10.1023\/B:TELS.0000014793.19622.0e","journal-title":"Telecommun. Syst."},{"key":"625_CR52","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Formal Methods (FM\u201906), LNCS, vol. 4085, pp. 573\u2013586. Springer (2006). https:\/\/doi.org\/10.1007\/11813040_38","DOI":"10.1007\/11813040_38"},{"key":"625_CR53","doi-asserted-by":"publisher","unstructured":"Purandare, R., Dwyer, M.B., Elbaum, S.: Monitor optimization via stutter-equivalent loop transformation. In: International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA\u201910), pp. 270\u2013285. ACM Press (2010). https:\/\/doi.org\/10.1145\/1869459.1869483","DOI":"10.1145\/1869459.1869483"},{"key":"625_CR54","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of $$\\omega $$-automata. In: Annual Symposium on Foundations of Computer Science, pp. 319\u2013327. IEEE (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"issue":"5","key":"625_CR55","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495\u2013511 (1994). https:\/\/doi.org\/10.1007\/BF01211865","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"625_CR56","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985). https:\/\/doi.org\/10.1145\/3828.3837","journal-title":"J. ACM"},{"key":"625_CR57","doi-asserted-by":"publisher","unstructured":"Sistla, A.P., \u017defran, M., Feng, Y.: Monitorability of stochastic dynamical systems. In: Computer Aided Verification (CAV\u201911), LNCS, vol. 6806, pp. 720\u2013736. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_58","DOI":"10.1007\/978-3-642-22110-1_58"},{"key":"625_CR58","doi-asserted-by":"publisher","unstructured":"Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: International Conference on Runtime Verification (RV\u201911), LNCS, vol. 7186, pp. 193\u2013207. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_15","DOI":"10.1007\/978-3-642-29860-8_15"},{"key":"625_CR59","doi-asserted-by":"publisher","unstructured":"Stucki, S., S\u00e1nchez, C., Schneider, G., Bonakdarpour, B.: Gray-box monitoring of hyperproperties. In: Formal Methods (FM\u201919), LNCS, vol. 11800, pp. 406\u2013424. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_25","DOI":"10.1007\/978-3-030-30942-8_25"},{"key":"625_CR60","doi-asserted-by":"publisher","unstructured":"Wang, Z., Zaki, M.H., Tahar, S.: Statistical runtime verification of analog and mixed signal designs. In: International Conference on Signals, Circuits and Systems (SCS\u201909), pp. 1\u20136. IEEE (2009). https:\/\/doi.org\/10.1109\/ICSCS.2009.5412620","DOI":"10.1109\/ICSCS.2009.5412620"},{"key":"625_CR61","doi-asserted-by":"publisher","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Symposium on Principles of Programming Languages (POPL\u201986), pp. 184\u2013193. ACM Press (1986). https:\/\/doi.org\/10.1145\/512644.512661","DOI":"10.1145\/512644.512661"},{"key":"625_CR62","doi-asserted-by":"publisher","unstructured":"Wu, E., Diao, Y., Rizvi, S.: High-performance complex event processing over streams. In: International Conference on Management of Data (SIGMOD\u201906), pp. 407\u2013418. ACM Press (2006). https:\/\/doi.org\/10.1145\/1142473.1142520","DOI":"10.1145\/1142473.1142520"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00625-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00625-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00625-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T14:07:40Z","timestamp":1634825260000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00625-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,30]]},"references-count":62,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["625"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00625-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,30]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}