{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:34:05Z","timestamp":1760142845738,"version":"build-2065373602"},"reference-count":56,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2024,1,8]],"date-time":"2024-01-08T00:00:00Z","timestamp":1704672000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"<jats:p>Recent findings demonstrate how database technology enhances the computation of formal verification tasks expressible in linear time logic for finite traces (LTLf). Human-readable declarative languages also help the common practitioner to express temporal constraints in a straightforward and accessible language. Notwithstanding the former, this technology is in its infancy, and therefore, few optimization algorithms are known for dealing with massive amounts of information audited from real systems. We, therefore, present four novel algorithms subsuming entire LTLf expressions while outperforming previous state-of-the-art implementations on top of KnoBAB, thus postulating the need for the corresponding, leading to the formulation of novel xtLTLf-derived algebraic operators.<\/jats:p>","DOI":"10.3390\/info15010034","type":"journal-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T03:36:58Z","timestamp":1704771418000},"page":"34","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Streamlining Temporal Formal Verification over Columnar Databases"],"prefix":"10.3390","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1844-0851","authenticated-orcid":false,"given":"Giacomo","family":"Bergami","sequence":"first","affiliation":[{"name":"School of Computing, Faculty of Science, Agriculture and Engineering, Newcastle University, Newcastle upon Tyne NE4 5TG, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2024,1,8]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/3503914","article-title":"Toward verified artificial intelligence","volume":"65","author":"Seshia","year":"2022","journal-title":"Commun. ACM"},{"key":"ref_2","unstructured":"Baier, C., and Katoen, J. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_3","first-page":"235","article-title":"Aligning Data-Aware Declarative Process Models and Event Logs","volume":"Volume 12875","author":"Polyvyanyy","year":"2021","journal-title":"Proceedings of the Business Process Management-19th International Conference, BPM 2021"},{"key":"ref_4","first-page":"326","article-title":"Efficient Compliance Checking Using BPMN-Q and Temporal Logic","volume":"Volume 5240","author":"Dumas","year":"2008","journal-title":"Proceedings of the Business Process Management, 6th International Conference, BPM 2008"},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"1009","DOI":"10.1016\/j.is.2011.04.002","article-title":"Process compliance analysis based on behavioural profiles","volume":"36","author":"Weidlich","year":"2011","journal-title":"Inf. Syst."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"e346","DOI":"10.7717\/peerj-cs.346","article-title":"Data augmentation based malware detection using convolutional neural networks","volume":"7","author":"Catak","year":"2021","journal-title":"PeerJ Comput. Sci."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Yazi, A.F., \u00c7atak, F.\u00d6., and G\u00fcl, E. (2019, January 24\u201326). Classification of Methamorphic Malware with Deep Learning (LSTM). Proceedings of the 27th Signal Processing and Communications Applications Conference, SIU 2019, Sivas, Turkey.","DOI":"10.1109\/SIU.2019.8806571"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"105132","DOI":"10.1109\/ACCESS.2019.2932260","article-title":"Repair Process Models Containing Non-Free-Choice Structures Based on Logic Petri Nets","volume":"7","author":"Zheng","year":"2019","journal-title":"IEEE Access"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1186\/s12911-020-01323-7","article-title":"Modeling clinical activities based on multi-perspective declarative process mining with openEHR\u2019s characteristic","volume":"20-S","author":"Xu","year":"2020","journal-title":"BMC Med. Inform. Decis. Mak."},{"key":"ref_10","unstructured":"van Dongen, B. (2024, January 03). Real-Life Event Logs-Hospital Log. Available online: https:\/\/data.4tu.nl\/articles\/_\/12716513\/1."},{"key":"ref_11","first-page":"145","article-title":"FoodBroker-Generating Synthetic Datasets for Graph-Based Business Analytics","volume":"Volume 8991","author":"Rabl","year":"2014","journal-title":"Proceedings of the Big Data Benchmarking-5th International Workshop, WBDB 2014"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/s10844-022-00716-6","article-title":"Forecasting and explaining emergency department visits in a public hospital","volume":"59","author":"Petsis","year":"2022","journal-title":"J. Intell. Inf. Syst."},{"key":"ref_13","unstructured":"Rossi, F. (2013, January 3\u20139). Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. Proceedings of the IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Pesi\u0107, M., Schonenberg, H., and van der Aalst, W.M. (2007, January 15\u201319). DECLARE: Full Support for Loosely-Structured Processes. Proceedings of the 11th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2007), Annapolis, MD, USA.","DOI":"10.1109\/EDOC.2007.14"},{"key":"ref_15","first-page":"4:1","article-title":"Temporal Big Data Analytics: New Frontiers for Big Data Analytics Research","volume":"Volume 206","author":"Combi","year":"2021","journal-title":"Proceedings of the 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Liu, L., and \u00d6zsu, M.T. (2018). Encyclopedia of Database Systems, Springer. [2nd ed.].","DOI":"10.1007\/978-1-4614-8265-9"},{"key":"ref_17","first-page":"290","article-title":"Efficient and Customisable Declarative Process Mining with SQL","volume":"Volume 9694","author":"Nurcan","year":"2016","journal-title":"Advanced Information Systems Engineering, Proceedings of the 28th International Conference, CAiSE 2016, Ljubljana, Slovenia, 13\u201317 June 2016"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"130:1","DOI":"10.1145\/3589275","article-title":"T-Rex: Optimizing Pattern Search on Time Series","volume":"1","author":"Huang","year":"2023","journal-title":"Proc. ACM Manag. Data"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"556","DOI":"10.1109\/TKDE.2011.170","article-title":"Extending BCDM to Cope with Proposals and Evaluations of Updates","volume":"25","author":"Anselma","year":"2013","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"1210","DOI":"10.14778\/2536274.2536278","article-title":"Comprehensive and Interactive Temporal Query Processing with SAP HANA","volume":"6","author":"Kaufmann","year":"2013","journal-title":"Proc. VLDB Endow."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0020-0255(94)00062-G","article-title":"Temporal Modules: An Approach Toward Federated Temporal Databases","volume":"82","author":"Wang","year":"1995","journal-title":"Inf. Sci."},{"key":"ref_22","unstructured":"Pissinou, N., Silberschatz, A., Park, E.K., and Makki, K. (December, January 28). Algebraic Query Languages on Temporal Databases with Multiple Time Granularities. Proceedings of the CIKM \u201995, 1995 International Conference on Information and Knowledge Management, Baltimore, MD, USA."},{"key":"ref_23","first-page":"17:1","article-title":"Time2State: An Unsupervised Framework for Inferring the Latent States in Time Series Data","volume":"1","author":"Wang","year":"2023","journal-title":"Proc. ACM Manag. Data"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"117176","DOI":"10.1016\/j.eswa.2022.117176","article-title":"A dynamic soft sensor of industrial fuzzy time series with propositional linear temporal logic","volume":"201","author":"Huo","year":"2022","journal-title":"Expert Syst. Appl."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"4393","DOI":"10.1109\/TII.2021.3123194","article-title":"Programmable Logic Controllers Past Linear Temporal Logic for Monitoring Applications in Industrial Control Systems","volume":"18","author":"Mao","year":"2022","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Fionda, V., Greco, G., and Mastratisi, M.A. (2021, January 1\u20133). Reasoning about Smart Contracts Encoded in LTL. Proceedings of the AIxIA, Milan, Italy.","DOI":"10.1007\/978-3-031-08421-8_9"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (November, January 31). The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), Providence, RI, USA.","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Bergami, G., Appleby, S., and Morgan, G. (2023). Quickening Data-Aware Conformance Checking through Temporal Algebras. Information, 14.","DOI":"10.20944\/preprints202301.0254.v1"},{"key":"ref_29","unstructured":"Bellatreche, L., Kechar, M., and Bahloul, S.N. (2021, January 14\u201316). Bringing Common Subexpression Problem from the Dark to Light: Towards Large-Scale Workload Optimizations. Proceedings of the IDEAS, Montreal, QC, Canada."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Appleby, S., Bergami, G., and Morgan, G. (2022, January 22\u201324). Running Temporal Logical Queries on the Relational Model. Proceedings of the 26th International Database Engineered Applications Symposium, Budapest, Hungary.","DOI":"10.1145\/3548785.3548786"},{"key":"ref_31","unstructured":"Atzeni, P., Ceri, S., Paraboschi, S., and Torlone, R. (1999). Database Systems\u2014Concepts, Languages and Architectures, McGraw-Hill Book Company."},{"key":"ref_32","unstructured":"Elmasri, R., and Navathe, S.B. (2015). Fundamentals of Database Systems, Pearson. [7th ed.]."},{"key":"ref_33","unstructured":"Dittrich, J. (2016). Patterns in Data Management: A Flipped Textbook, CreateSpace Independent Publishing Platform."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Bergami, G., Appleby, S., and Morgan, G. (2023). Specification Mining over Temporal Data. Computers, 12.","DOI":"10.3390\/computers12090185"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/j.eswa.2016.08.040","article-title":"Conformance checking based on multi-perspective declarative process models","volume":"65","author":"Burattin","year":"2016","journal-title":"Expert Syst. Appl."},{"key":"ref_36","first-page":"684","article-title":"First-Order vs. Second-Order Encodings for \\textsc ltl_f -to-Automata Translation","volume":"Volume 11436","author":"Gopal","year":"2019","journal-title":"Theory and Applications of Models of Computation, Proceedings of the 15th Annual Conference, TAMC 2019, Kitakyushu, Japan, 13\u201316 April 2019"},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"103369","DOI":"10.1016\/j.artint.2020.103369","article-title":"SAT-based explicit LTLf satisfiability checking","volume":"289","author":"Li","year":"2020","journal-title":"Artif. Intell."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/MCI.2017.2670420","article-title":"IEEE 1849: The XES Standard: The Second IEEE Standard Sponsored by IEEE Computational Intelligence Society [Society Briefs]","volume":"12","author":"Acampora","year":"2017","journal-title":"IEEE Comput. Intell. Mag."},{"key":"ref_39","unstructured":"Maggi, F.M., Bose, R.P.J.C., and van der Aalst, W.M.P. (2012). Advanced Information Systems Engineering, Springer."},{"key":"ref_40","doi-asserted-by":"crossref","unstructured":"Polyvyanyy, A. (2022). Process Querying Methods, Springer.","DOI":"10.1007\/978-3-030-92875-9"},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Polyvyanyy, A. (2022). Process Querying Methods, Springer.","DOI":"10.1007\/978-3-030-92875-9"},{"key":"ref_42","first-page":"40","article-title":"MonetDB: Two Decades of Research in Column-oriented Database Architectures","volume":"35","author":"Idreos","year":"2012","journal-title":"IEEE Data Eng. Bull."},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Green, T.J., Karvounarakis, G., and Tannen, V. (2007, January 11\u201313). Provenance Semirings. Proceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, New York, NY, USA.","DOI":"10.1145\/1265530.1265535"},{"key":"ref_44","unstructured":"Sch\u00f6nig, S. (2015). SQL Queries for Declarative Process Mining on Event Logs of Relational Databases. arXiv."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"1648","DOI":"10.14778\/1687553.1687618","article-title":"Database Architecture Evolution: Mammals Flourished long before Dinosaurs became Extinct","volume":"2","author":"Boncz","year":"2009","journal-title":"Proc. VLDB Endow."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","article-title":"Maintaining Knowledge about Temporal Intervals","volume":"26","author":"Allen","year":"1983","journal-title":"Commun. ACM"},{"key":"ref_47","doi-asserted-by":"crossref","unstructured":"Revesz, P.Z. (2010). Introduction to Databases\u2014From Biological to Spatio-Temporal, Springer. Texts in Computer Science.","DOI":"10.1007\/978-1-84996-095-3"},{"key":"ref_48","unstructured":"Kvet, M. (2023). Developing Robust Date and Time Oriented Applications in Oracle Cloud: A Comprehensive Guide to Efficient Date and Time Management in Oracle Cloud, Packt Publishing."},{"key":"ref_49","unstructured":"Tuzhilin, A., and Kedem, Z. (1989). Using Temporal Logic and Datalog to Query Databases Evolving in Time, New York University."},{"key":"ref_50","doi-asserted-by":"crossref","unstructured":"Apers, P., Bouzeghoub, M., and Gardarin, G. (1996). Advances in Database Technology\u2014EDBT \u201996, Proceedings of the 5th International Conference on Extending Database Technology, Avignon, France, 25\u201329 March 1996, Springer.","DOI":"10.1007\/BFb0014139"},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Liu, L., and \u00d6zsu, M.T. (2009). Encyclopedia of Database Systems, Springer.","DOI":"10.1007\/978-0-387-39940-9"},{"key":"ref_52","doi-asserted-by":"crossref","first-page":"983","DOI":"10.1002\/(SICI)1097-024X(199708)27:8<983::AID-SPE117>3.0.CO;2-#","article-title":"Introspective Sorting and Selection Algorithms","volume":"27","author":"Musser","year":"1997","journal-title":"Softw. Pract. Exp."},{"key":"ref_53","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P. (2023). Object-Centric Process Mining: Unraveling the Fabric of Real Processes. Mathematics, 11.","DOI":"10.3390\/math11122691"},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/s00778-021-00667-4","article-title":"Distributed temporal graph analytics with GRADOOP","volume":"31","author":"Rost","year":"2022","journal-title":"VLDB J."},{"key":"ref_55","doi-asserted-by":"crossref","unstructured":"Khayatbashi, S., Hartig, O., and Jalali, A. (2023, January 6\u20139). Transforming Event Knowledge Graph to Object-Centric Event Logs: A Comparative Study for Multi-dimensional Process Analysis. Proceedings of the 42nd International Conference on Conceptual Modeling, Lisbon, Portugal.","DOI":"10.1007\/978-3-031-47262-6_12"},{"key":"ref_56","first-page":"147","article-title":"Efficient Checking of Timed Ordered Anti-patterns over Graph-Encoded Event Logs","volume":"Volume 13761","author":"Yousef","year":"2022","journal-title":"Model and Data Engineering: Proceedings of the 11th International Conference, MEDI 2022, Cairo, Egypt, 21\u201324 November 2022"}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/15\/1\/34\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:42:27Z","timestamp":1760103747000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/15\/1\/34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,8]]},"references-count":56,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2024,1]]}},"alternative-id":["info15010034"],"URL":"https:\/\/doi.org\/10.3390\/info15010034","relation":{},"ISSN":["2078-2489"],"issn-type":[{"type":"electronic","value":"2078-2489"}],"subject":[],"published":{"date-parts":[[2024,1,8]]}}}