{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T09:10:12Z","timestamp":1701076212976},"reference-count":39,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2023,3,30]],"date-time":"2023-03-30T00:00:00Z","timestamp":1680134400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,6,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Runtime verification is a lightweight formal verification technique used to verify the runtime behaviour of software (resp. hardware) systems. Given a formal property, one or more monitors are synthesized to verify the latter against a system execution. A monitor can only conclude the violation of a property when it observes such a violation. Unfortunately, in safety-critical scenarios, this might happen too late for the system to react properly. In such scenarios, it is advised to use predictive runtime verification, where monitors are capable of anticipating (by using a model of the system) future events before actually observing them. In this work, instead of assuming such a model is given, we describe a runtime verification workflow where the model is learnt and incrementally refined by using process mining techniques. We present the approach and the resulting prototype tool.<\/jats:p>","DOI":"10.1093\/logcom\/exad012","type":"journal-article","created":{"date-parts":[[2023,3,31]],"date-time":"2023-03-31T02:39:45Z","timestamp":1680230385000},"page":"796-817","source":"Crossref","is-referenced-by-count":1,"title":["Incrementally predictive runtime verification"],"prefix":"10.1093","volume":"33","author":[{"given":"Angelo","family":"Ferrando","sequence":"first","affiliation":[{"name":"Department of Computer Science, Bioengineering, Robotics and Systems Engineering , University of Genova, 16146, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giorgio","family":"Delzanno","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Bioengineering, Robotics and Systems Engineering , University of Genova, 16146, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2023,3,30]]},"reference":[{"key":"2023060916151661900_ref1","first-page":"416","article-title":"Business monitoring framework for process discovery with real-life logs","volume-title":"Business Process Management - 12th International Conference, BPM 2014","author":"Abe","year":"2014"},{"key":"2023060916151661900_ref2","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1016\/j.datak.2018.04.007","article-title":"Automated discovery of structured process models from event logs: The discover-and-structure approach","volume":"117","author":"Augusto","year":"2018","journal-title":"Data Knowl. Eng."},{"key":"2023060916151661900_ref3","doi-asserted-by":"crossref","first-page":"686","DOI":"10.1109\/TKDE.2018.2841877","article-title":"Automated discovery of process models from event logs: Review and benchmark","volume":"31","author":"Augusto","year":"2019","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"2023060916151661900_ref4","first-page":"205","article-title":"Prevent: A predictive run-time verification framework using statistical learning","volume-title":"Software Engineering and Formal Methods - 16th International Conference, SEFM 2018","author":"Babaee","year":"2018"},{"key":"2023060916151661900_ref5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","article-title":"Introduction to runtime verification","volume-title":"Lectures on Runtime Verification","author":"Bartocci","year":"2018"},{"key":"2023060916151661900_ref6","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-3-030-32079-9_8","article-title":"Neural predictive monitoring","volume-title":"International Conference on Runtime Verification","author":"Bortolussi","year":"2019"},{"key":"2023060916151661900_ref7","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1007\/s10009-021-00623-1","article-title":"Neural predictive monitoring and a comparison of frequentist and bayesian approaches","volume":"23","author":"Bortolussi","year":"2021","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2023060916151661900_ref8","first-page":"425","volume-title":"On a Decision Method in Restricted Second Order Arithmetic","author":"Richard B\u00fcchi","year":"1990"},{"key":"2023060916151661900_ref9","article-title":"Business process model and notation"},{"key":"2023060916151661900_ref10","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-030-88494-9_7","article-title":"Neural predictive monitoring under partial observability","volume-title":"International Conference on Runtime Verification","author":"Cairoli","year":"2021"},{"key":"2023060916151661900_ref11","first-page":"353","article-title":"Heterogeneous verification of an autonomous curiosity rover","volume-title":"NASA Formal Methods - 12th International Symposium, NFM 2020","author":"Cardoso","year":"2020"},{"key":"2023060916151661900_ref12","first-page":"165","article-title":"Assumption-based runtime verification with partial observability and resets","volume-title":"Runtime Verification - 19th International Conference, RV 2019","author":"Cimatti","year":"2019"},{"key":"2023060916151661900_ref13","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/BFb0058022","article-title":"Model checking","volume-title":"International Conference on Foundations of Software Technology and Theoretical Computer Science","author":"Clarke","year":"1997"},{"key":"2023060916151661900_ref14","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/s10458-020-09487-2","article-title":"Towards a framework for certification of reliable autonomous systems","volume":"35","author":"Fisher","year":"2021","journal-title":"Auton. Agents Multi Agent Syst."},{"key":"2023060916151661900_ref15","first-page":"314","article-title":"Incremental runtime verification of probabilistic systems","volume-title":"International Conference on Runtime Verification","author":"Forejt","year":"2012"},{"key":"2023060916151661900_ref16","article-title":"Process discovery using inductive miner and decomposition","volume-title":"CoRR","author":"Ghawi","year":"2016"},{"key":"2023060916151661900_ref17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0055036","article-title":"Algorithmic verification of linear temporal logic specifications","volume-title":"Automata, Languages and Programming, 25th International Colloquium, ICALP\u201998","author":"Kesten","year":"1998"},{"key":"2023060916151661900_ref18","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke","year":"1963","journal-title":"Acta Philosophica Fennica"},{"key":"2023060916151661900_ref19","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"Prism 4.0: Verification of probabilistic real-time systems","volume-title":"International Conference on Computer Aided Verification","author":"Kwiatkowska","year":"2011"},{"key":"2023060916151661900_ref20","first-page":"311","article-title":"Discovering block-structured process models from event logs\u2014A constructive approach","volume-title":"Application and Theory of Petri Nets and Concurrency - 34th International Conference, PETRI NETS 2013","author":"Leemans","year":"2013"},{"key":"2023060916151661900_ref21","first-page":"82","article-title":"Sliding between model checking and runtime verification","volume-title":"Runtime Verification","author":"Leucker","year":"2012"},{"key":"2023060916151661900_ref22","volume-title":"Automated Theorem Proving: A Logical Basis","author":"Loveland","year":"1978"},{"key":"2023060916151661900_ref23","first-page":"457","article-title":"Predictive monitoring of business processes","volume-title":"Advanced Information Systems Engineering - 26th International Conference, CAiSE 2014","author":"Maggi","year":"2014"},{"key":"2023060916151661900_ref24","volume-title":"Kommunikation mit Automaten","author":"Petri","year":"1962"},{"key":"2023060916151661900_ref25","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1016\/j.jss.2017.06.060","article-title":"Predictive runtime verification of timed properties","volume":"132","author":"Pinisetty","year":"2017","journal-title":"Journal of Systems and Software"},{"key":"2023060916151661900_ref26","first-page":"46","article-title":"The temporal logic of programs","volume-title":"18th Annual Symposium on Foundations of Computer Science","author":"Pnueli","year":"1977"},{"key":"2023060916151661900_ref27","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1109\/5.18626","article-title":"A tutorial on hidden markov models and selected applications in speech recognition","volume":"77","author":"Rabiner","year":"1989","journal-title":"Proceedings of the IEEE"},{"key":"2023060916151661900_ref28","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/B978-0-08-013376-8.50008-3","article-title":"Chapter ii - finite non-deterministic and probabilistic automata","volume-title":"Theory of Automata","author":"ARTO SALOMAA","year":"1969"},{"key":"2023060916151661900_ref29","doi-asserted-by":"crossref","first-page":"85","DOI":"10.22266\/ijies2019.0430.09","article-title":"Graph-based algorithms for discovering a process model containing invisible tasks","volume":"12","author":"Sarno","year":"2019","journal-title":"International Journal of Intelligent Engineering and Systems"},{"key":"2023060916151661900_ref30","doi-asserted-by":"crossref","first-page":"137","DOI":"10.26555\/ijain.v5i2.296","article-title":"A survey of graph-based algorithms for discovering business processes","volume":"5","author":"Sarno","year":"2019","journal-title":"International Journal of Advances in Intelligent Informatics"},{"key":"2023060916151661900_ref31","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-662-49851-4_1","article-title":"Data science in action","volume-title":"Process Mining","author":"Van Der Aalst","year":"2016"},{"key":"2023060916151661900_ref32","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19345-3","volume-title":"Process Mining - Discovery, Conformance and Enhancement of Business Processes","author":"van der Aalst","year":"2011"},{"key":"2023060916151661900_ref33","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2229156.2229157","article-title":"Process mining: Overview and opportunities","volume":"3","author":"van der Aalst","year":"2012","journal-title":"ACM Trans. Manag. Inf. Syst."},{"key":"2023060916151661900_ref34","doi-asserted-by":"crossref","first-page":"1128","DOI":"10.1109\/TKDE.2004.47","article-title":"Workflow mining: Discovering process models from event logs","volume":"16","author":"van der Aalst","year":"2004","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"2023060916151661900_ref35","doi-asserted-by":"crossref","first-page":"127","DOI":"10.22266\/ijies2020.0430.13","article-title":"An improved method of parallel model detection for graph-based process model discovery","volume":"13","author":"Waspada","year":"2020","journal-title":"International Journal of Intelligent Engineering and Systems"},{"key":"2023060916151661900_ref36","first-page":"310","article-title":"Flexible heuristics miner (FHM)","volume-title":"Proceedings of the IEEE Symposium on Computational Intelligence and Data Mining, CIDM 2011","author":"Weijters","year":"2011"},{"key":"2023060916151661900_ref37","doi-asserted-by":"crossref","first-page":"999","DOI":"10.1016\/j.datak.2010.06.001","article-title":"Mining process models with prime invisible tasks","volume":"69","author":"Wen","year":"2010","journal-title":"Data Knowledge and Engineering"},{"key":"2023060916151661900_ref38","first-page":"223","article-title":"A predictive runtime verification framework for cyber-physical systems","volume-title":"Software Security and Reliability-Companion","author":"Kang","year":"2014"},{"key":"2023060916151661900_ref39","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/978-3-642-28891-3_37","article-title":"Runtime verification with predictive semantics","volume-title":"NASA Formal Methods","author":"Zhang","year":"2012"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/33\/4\/796\/50555588\/exad012.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/33\/4\/796\/50555588\/exad012.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,9]],"date-time":"2023-06-09T17:13:58Z","timestamp":1686330838000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/33\/4\/796\/7091907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,30]]},"references-count":39,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2023,3,30]]},"published-print":{"date-parts":[[2023,6,7]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exad012","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,6]]},"published":{"date-parts":[[2023,3,30]]}}}