research-article

Monitoring Metric First-Order Temporal Properties

Authors:

Felix Klaedtke,

Samuel Müller,

Eugen ZălinescuAuthors Info & Claims

Journal of the ACM (JACM), Volume 62, Issue 2

Article No.: 15, Pages 1 - 45

https://doi.org/10.1145/2699444

Published: 06 May 2015 Publication History

Abstract

Runtime monitoring is a general approach to verifying system properties at runtime by comparing system events against a specification formalizing which event sequences are allowed. We present a runtime monitoring algorithm for a safety fragment of metric first-order temporal logic that overcomes the limitations of prior monitoring algorithms with respect to the expressiveness of their property specification languages. Our approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinite domains, and the arbitrary nesting of both past and bounded future operators. Furthermore, we show how to use and optimize our approach for the common case where structures consist of only finite relations, over possibly infinite domains. We also report on case studies from the domain of security and compliance in which we empirically evaluate the presented algorithms. Taken together, our results show that metric first-order temporal logic can serve as an effective specification language for expressing and monitoring a wide variety of practically relevant system properties.

References

[1]

107th Congress. 2001. Uniting and strengthening America by Providing Appropriate Tools Required to Intercept and Obstruct Terrorism Act of 2001 (USA PATRIOT ACT). Public Law 107-56.

[2]

Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases. Addison-Wesley Longman Publishing Co., Inc., Boston, MA.

Digital Library

[3]

Bowen Alpern and Fred B. Schneider. 1985. Defining liveness. Inform. Process. Lett. 21, 4, 181--185.

[4]

Rajeev Alur and Thomas A. Henzinger. 1992. Logics and models of real time: A survey. In Proceedings of the 1991 REX Workshop on Real Time: Theory in Practice. Lecture Notes in Computer Science, vol. 600. Springer, Heidelberg, Germany, 74--106.

Digital Library

[5]

Rajeev Alur and Thomas A. Henzinger. 1994. A really temporal logic. J. ACM 41, 1, 181--204.

Digital Library

[6]

Arvind Arasu, Shivnath Babu, and Jennifer Widom. 2006. The CQL continuous query language: Semantic foundations and query execution. VLDB J. 15, 2, 121--142.

Digital Library

[7]

Franz Baader, Andreas Bauer, and Marcel Lippmann. 2009. Runtime verification using a temporal description logic. In Proceedings of the 7th International Symposium on Frontiers of Combining Systems. Lecture Notes in Computer Science, vol. 5749. Springer, Heidelberg, Germany, 149--164.

Digital Library

[8]

Luciano Baresi, Domenico Bianculli, Sam Guinea, and Paola Spoletini. 2009. Keep it small, keep it real: Efficient run-time verification of web service compositions. In Proceedings of the Joint Conference on Formal Techniques for Distributed Systems, (11th IFIP WG 6.1 International Conference on Formal Method for Open Object-Based Distributed Systems and 29th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems). Lecture Notes in Computer Science, vol. 5522. Springer, Heidelberg, Germany, 26--40.

Digital Library

[9]

Howard Barringer, Yliés Falcone, Klaus Havelund, Giles Reger, and David E. Rydeheard. 2012. Quantified event automata: Towards expressive and efficient runtime monitors. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 7436. Springer, Heidelberg, Germany, 68--84.

[10]

Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. 2004. Rule-based runtime verification. In Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer, Heidelberg, Germany, 44--57.

[11]

Howard Barringer, Alex Groce, Klaus Havelund, and Margaret H. Smith. 2010a. Formal analysis of log files. J. Aero. Comput. Inf. Commun. 7, 11, 365--390.

[12]

Howard Barringer and Klaus Havelund. 2011. TraceContract: A scala DSL for trace analysis. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 6664. Springer, Heidelberg, Germany, 57--72.

Digital Library

[13]

Howard Barringer, David E. Rydeheard, and Klaus Havelund. 2010b. Rule systems for run-time monitoring: From Eagle to RuleR. J. Logic Comput. 20, 3, 675--706.

Digital Library

[14]

Adam Barth, Anupam Datta, John C. Mitchell, and Helen Nissenbaum. 2006. Privacy and contextual integrity: Framework and applications. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, Los Alamitos, CA, 184--198.

Digital Library

[15]

David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke, and Heiko Mantel. 2014. Scalable offline monitoring. In Proceedings of the 5th International Conference on Runtime Verification. Lecture Notes in Computing Science, vol. 8734. Springer, Heidelberg, Germany, 31--47.

[16]

David Basin, Matúš Harvan, Felix Klaedtke, and Eugen Zălinescu. 2012a. MONPOLY: Monitoring usage-control policies. In Proceedings of the 2nd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7186. Springer, Heidelberg, Germany, 360--364.

Digital Library

[17]

David Basin, Matúš Harvan, Felix Klaedtke, and Eugen Zălinescu. 2013a. Monitoring data usage in distributed systems. IEEE Trans. Softw. Eng. 39, 10, 1403--1426.

Digital Library

[18]

David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu. 2013b. Monitoring compliance policies over incomplete and disagreeing logs. In Proceedings of the 3rd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7687, Springer, Heidelberg, Germany, 151--167.

[19]

David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu. 2013c. Monitoring of temporal first-order properties with aggregations. In Proceedings of the 4th International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 8174. Springer, Heidelberg, Germany, 40--58.

[20]

David Basin, Felix Klaedtke, and Samuel Müller. 2010a. Monitoring security policies with metric first-order temporal logic. In Proceedings of the 15th ACM Symposium on Access Control Models and Technologies. ACM, New York, 23--33.

Digital Library

[21]

David Basin, Felix Klaedtke, and Samuel Müller. 2010b. Policy monitoring in first-order temporal logic. In Proceedings of the 22nd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174. Springer, Heidelberg, Germany, 1--18.

Digital Library

[22]

David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann. 2008. Runtime monitoring of metric first-order temporal properties. In Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs). LIPIcs, vol. 2. Schloss Dagstuhl - Leibniz Center for Informatics, 49--60.

[23]

David Basin, Felix Klaedtke, and Eugen Zălinescu. 2012b. Algorithms for monitoring real-time properties. In Proceedings of the 2nd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7186. Springer, Heidelberg, Germany, 260--275.

Digital Library

[24]

Andreas Bauer and Yliés Falcone. 2012. Decentralised LTL monitoring. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 7436. Springer, Heidelberg, Germany, 85--100.

[25]

Andreas Bauer, Rajeev Goré, and Alwen Tiu. 2009. A first-order policy language for history-based transaction monitoring. In Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing. Lecture Notes in Computer Science, vol. 5684. Springer, Heidelberg, Germany, 96--111.

Digital Library

[26]

Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20, 4.

Digital Library

[27]

Achim Blumensath and Erich Grädel. 2004. Finite presentations of infinite structures: Automata and interpretations. Theoret Comput. Syst. 37, 6, 641--674.

[28]

Jan Chomicki. 1995. Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. 20, 2, 149--186.

Digital Library

[29]

Jan Chomicki and Damian Niwiński. 1995. On the feasibility of checking temporal integrity constraints. J. Comput. Syst. Sci. 51, 3, 523--535.

Digital Library

[30]

Jan Chomicki and David Toman. 1995. Implementing temporal integrity constraints using an active DBMS. IEEE Trans. Knowl. Data Eng. 7, 4, 566--582.

Digital Library

[31]

Jan Chomicki, David Toman, and Michael H. Böhlen. 2001. Querying ATSQL databases with temporal logic. ACM Trans. Database Syst. 26, 2, 145--178.

Digital Library

[32]

Edmund M. Clarke and E. Allen Emerson. 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedinggs of the 1981 Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 131. Springer, Heidelberg, Germany, 52--71.

Digital Library

[33]

Gianpaolo Cugola and Alessandro Margara. 2012. Processing flows of information: From data stream to complex event processing. ACM Comput. Surv. 44, 3.

Digital Library

[34]

Ben D'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, and Zohar Manna. 2005. LOLA: Runtime monitoring of synchronous systems. In Proceedings of the 12th International Symposium on Temporal Representation and Reasoning. IEEE Computer Society, Los Alamitos, CA, 166--174.

Digital Library

[35]

Jeffrey Dean and Sanjay Ghemawat. 2008. MapReduce: Simplified data processing on large clusters. Commun. ACM 51, 1, 107--113.

Digital Library

[36]

Department of the Treasury. 1970. Bank Secrecy Act of 1970 (BSA). 31 USC 5311-5332 and 31 CFR 103.

[37]

Robert A. Di Paola. 1969. The recursive unsolvability of the decision problem for the class of definite formulas. J. ACM 16, 2, 324--327.

Digital Library

[38]

Nikhil Dinesh, Aravind Joshi, Insup Lee, and Oleg Sokolsky. 2008. Checking traces for regulatory conformance. In Proceedings of the 8th Workshop on Runtime Verification. Lecture Notes in Computer Science, vol. 5289. Springer, Heidelberg, Germany, 86--103.

Digital Library

[39]

Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2007. Obligations and their interaction with programs. In Proceedings of the 12th European Symposium on Research in Computer Security. Lecture Notes in Computer Science, vol. 4734. Springer, Heidelberg, Germany, 375--289.

Digital Library

[40]

Herbert B. Enderton. 1972. A Mathematical Introduction to Logic. Academic Press, San Diego, CA.

[41]

David F. Ferraiolo, Ravi S. Sandhu, Serban I. Gavrila, D. Richard Kuhn, and Ramaswamy Chandramouli. 2001. Proposed NIST standard for role-based access control. ACM Trans. Inform. Syst. Secur. 4, 3, 224--274.

Digital Library

[42]

Bernd Finkbeiner and Henny Sipma. 2004. Checking finite traces using alternating automata. Form. Method. Syst. Des. 24, 2, 101--127.

Digital Library

[43]

Deepak Garg, Limin Jia, and Anupam Datta. 2011. Policy auditing over incomplete logs: theory, implementation and applications. In Proceedings of the 18th ACM Conference on Computer and Communications Security. ACM, New York, 151--162.

Digital Library

[44]

Dimitra Giannakopoulou and Klaus Havelund. 2001. Automata-based verification of temporal properties on running programs. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, Los Alamitos, CA, 412--416.

Digital Library

[45]

Christopher Giblin, Alice Y. Liu, Samuel Müller, Birgit Pfitzmann, and Xin Zhou. 2005. Regulations expressed as logical models (REALM). In Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems (Frontiers Artificial Intelligence Appl.). Frontiers in Artificial Intelligence and Applications, vol. 134. IOS Press, Amsterdam, The Netherlands, 37--48.

Digital Library

[46]

Sylvain Hallé and Roger Villemaire. 2012. Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5, 2, 192--206.

Digital Library

[47]

Klaus Havelund and Grigore Roşu. 2004. Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Trans. 6, 2, 158--173.

Digital Library

[48]

Klaus Havelund and Willem Visser. 2002. Program model checking as a new trend. Int. J. Softw. Tools Technol. Trans. 4, 1, 8--20.

[49]

Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. 1995. Mona: Monadic second-order logic in practice. In Proceedings of the 1st International Workshop on Tools and Algorithms for Contruction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1019. Springer, Heidelberg, Germany, 89--110.

Digital Library

[50]

Thomas A. Henzinger. 1990. Half-order modal logic: how to prove real-time properties. In Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing. ACM Press, New York, 281--296.

Digital Library

[51]

Thomas A. Henzinger. 1992. Sooner is safer than later. Inform. Process. Lett. 43, 3, 135--141.

Digital Library

[52]

Manuel Hilty, David Basin, and Alexander Pretschner. 2005. On obligations. In Proceedings of the 10th European Symposium on Research in Computer Security. Lecture Notes in Computer Science, vol. 3679. Springer, Heidelberg, Germany, 98--117.

Digital Library

[53]

IEEE Std 1800-2009 2009. Standard for SystemVerilog--Unified Hardware Design, Specification, and Verification Language. (December 2009). http://ieeexplore.ieee.org/xpls/abs&lowbar;all.jsp&quest;arnumber=5354441&tag==1.

[54]

IEEE Std 1850-2010 2012. Standard for Property Specification Language (PSL). (June 2012).http://ieeexplore.ieee.org/xpl/articleDetails.jsp&quest;arnumber=6228486.

[55]

Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, and Elad Shahar. 2001. Symbolic model checking with rich assertional languages. Theoret. Comput. Sci. 256, 1--2, 93--112.

Digital Library

[56]

Bakhadyr Khoussainov and Anil Nerode. 1995. Automatic presentations of structures. In Proceedings of the International Workshop on Logical and Computational Complexity. Lecture Notes in Computer Science, vol. 960. Springer, Heidelberg, Germany, 367--392.

Digital Library

[57]

Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. 2002. MONA implementation secrets. Int. J. Found. Comput. Sci. 13, 4, 571--586.

[58]

Ron Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-Time Syst. 2, 4, 255--299.

Digital Library

[59]

Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. 1985. The glory of the past. In Proceedings of the Conference on Logic of Programs. Lecture Notes in Computer Science, vol. 193. Springer, Heidelberg, Germany, 196--218.

Digital Library

[60]

Udo Walter Lipeck and Gunter Saake. 1987. Monitoring dynamic integrity constraints based on temporal logic. Inf. Syst. 12, 3, 255--269.

Digital Library

[61]

Fabrizio Maria Maggi, Marco Montali, Michael Westergaard, and Wil M. P. van der Aalst. 2011. Monitoring business constraints with linear temporal logic: An approach based on colored automata. In Proceedings of the 9th International Conference on Business Process Management. Lecture Notes in Computer Science, vol. 6896. Springer, Heidelberg, Germany, 132--147.

Digital Library

[62]

Oded Maler and Dejan Nickovic. 2013. Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Trans. 15, 247--268. Issue 3.

Digital Library

[63]

Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, and Grigore Roşu. 2012. An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Trans. 14, 3, 249--289.

Digital Library

[64]

MonPoly. 2013. MonPoly source code and examples. http://sourceforge.net/projects/monpoly.

[65]

Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society, Los Alamitos, CA, 46--57.

Digital Library

[66]

Amir Pnueli and Aleksandr Zaks. 2006. PSL Model checking and run-time verification via testers. In Proceedings of the 14th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085. Springer, Heidelberg, Germany, 573--586.

Digital Library

[67]

PostgreSQL Global Development Group. 2012. PostgreSQL, Version 9.1.4. http://www.postgresql.org/.

[68]

Thomas Reinbacher, Matthias Fuegger, and Jörg Brauer. 2013. Real-time runtime verification on chip. In Proceedings of the 3rd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7687. Springer, Heidelberg, Germany, 110--125.

[69]

Muriel Roger and Jean Goubault-Larrecq. 2001. Log auditing through model-checking. In Proceedings of the 14th IEEE Computer Security Foundations Workshop. IEEE Computer Society, Los Alamitos, CA, 220--234.

Digital Library

[70]

Grigore Roşu and Feng Chen. 2012. Semantics and algorithms for parametric monitoring. Log. Method. Comput. Sci. 8, 1.

[71]

Grigore Roşu and Klaus Havelund. 2005. Rewriting-based techniques for runtime verification. Automat. Softw. Eng. 12, 2, 151--197.

Digital Library

[72]

A. Prasad Sistla and Ouri Wolfson. 1995. Temporal triggers in active databases. IEEE Trans. Knowl. Data Eng. 7, 3, 471--486.

Digital Library

[73]

Volker Stolz and Eric Bodden. 2006. Temporal assertions using Aspect. In Proceedings of the 5th Workshop on Runtime Verification. Electronic Notes in Theoretical Computer Science, vol. 144, Elsevier Science, Inc., Amsterdam, The Netherlands, 109--124.

Digital Library

[74]

Prasanna Thati and Grigore Roşu. 2005. Monitoring algorithms for metric temporal logic specifications. In Proceedings of the 4th Workshop on Runtime Verification. Electronic Notes in Theoretical Computer Science, vol. 113, Elsevier Science Inc., Amsterdam, The Netherlands, 145--162.

Digital Library

[75]

Allen Van Gelder and Rodney W. Topor. 1991. Safety and translation of relational calculus. ACM Trans. Database Syst. 16, 2, 235--278.

Digital Library

[76]

Moshe Y. Vardi. 2009. From philosophical to industrial logics. In Proceedings of the 3rd Indian Conference on Logic and its Applications. Lecture Notes in Computer Science, vol. 5378. Springer, Heidelberg, Germany, 89--115.

Digital Library

[77]

Xinwen Zhang, Francesco Parisi-Presicce, Ravi Sandhu, and Jaehong Park. 2005. Formal model and policy specification of usage control. ACM Trans. Inform. Syst. Secur. 8, 4, 351--387.

Digital Library

Cited By

Park Gvan der Aalst W(2025)Operational process monitoring: An object-centric approachComputers in Industry10.1016/j.compind.2024.104170164(104170)Online publication date: Jan-2025
https://doi.org/10.1016/j.compind.2024.104170
Basin DDebois SHildebrandt T(2024)Proactive enforcement of provisions and obligationsJournal of Computer Security10.3233/JCS-21007832:3(247-289)Online publication date: 17-Jun-2024
https://doi.org/10.3233/JCS-210078
Zhang YXu SChen HAslam Bhatt UHuang M(2024)Context-aware environment online monitoring for safety autonomous vehicle systems: an automata-theoretic approachJournal of Cloud Computing: Advances, Systems and Applications10.1186/s13677-023-00567-813:1Online publication date: 3-Jan-2024
https://dl.acm.org/doi/10.1186/s13677-023-00567-8
Show More Cited By

Index Terms

Monitoring Metric First-Order Temporal Properties

Recommendations

Monitoring security policies with metric first-order temporal logic
SACMAT '10: Proceedings of the 15th ACM symposium on Access control models and technologies

We show the practical feasibility of monitoring complex security properties using a runtime monitoring approach for metric first-order temporal logic. In particular, we show how a wide variety of security policies can be naturally formalized in this ...
First-Order Temporal Verification in Practice

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems ...
Monitoring Algorithms for Metric Temporal Logic Specifications

Program execution traces can be so large in practical testing and monitoring applications that it would be very expensive, if not impossible, to store them for detailed analysis. Monitoring execution traces without storing them, can be a nontrivial ...

Comments

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 62, Issue 2

May 2015

304 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/2772377

Editor:
Victor Vianu
University of California, San Diego

Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 May 2015

Accepted: 01 December 2014

Revised: 01 February 2014

Received: 01 January 2013

Published in JACM Volume 62, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Nokia Research Center, Switzerland

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

119
Total Citations
View Citations
779
Total Downloads

Downloads (Last 12 months)119
Downloads (Last 6 weeks)11

Reflects downloads up to 06 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Park Gvan der Aalst W(2025)Operational process monitoring: An object-centric approachComputers in Industry10.1016/j.compind.2024.104170164(104170)Online publication date: Jan-2025
https://doi.org/10.1016/j.compind.2024.104170
Basin DDebois SHildebrandt T(2024)Proactive enforcement of provisions and obligationsJournal of Computer Security10.3233/JCS-21007832:3(247-289)Online publication date: 17-Jun-2024
https://doi.org/10.3233/JCS-210078
Zhang YXu SChen HAslam Bhatt UHuang M(2024)Context-aware environment online monitoring for safety autonomous vehicle systems: an automata-theoretic approachJournal of Cloud Computing: Advances, Systems and Applications10.1186/s13677-023-00567-813:1Online publication date: 3-Jan-2024
https://dl.acm.org/doi/10.1186/s13677-023-00567-8
Hekmatnejad MHoxha BDeshmukh JYang YFainekos G(2024)Formalizing and evaluating requirements of perception systems for automated vehicles using spatio-temporal perception logicThe International Journal of Robotics Research10.1177/02783649231223546Online publication date: 24-Jan-2024
https://doi.org/10.1177/02783649231223546
Asadian HFiterau-Brostean PJonsson BSagonas K(2024)Monitor-based Testing of Network Protocol Implementations Using Symbolic ExecutionProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3664521(1-12)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3664521
Ganguly RXue YJonckheere ALjung PSchornstein BBonakdarpour BHerlihy M(2024)Distributed runtime verification of metric temporal propertiesJournal of Parallel and Distributed Computing10.1016/j.jpdc.2023.104801185:COnline publication date: 4-Mar-2024
https://dl.acm.org/doi/10.1016/j.jpdc.2023.104801
Schneider SMaximova MGiese H(2024)Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logicJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100938137(100938)Online publication date: Feb-2024
https://doi.org/10.1016/j.jlamp.2023.100938
Gorostiaga FSánchez C(2024)General monitorability of totally ordered verdict domainsInnovations in Systems and Software Engineering10.1007/s11334-024-00557-2Online publication date: 6-Apr-2024
https://doi.org/10.1007/s11334-024-00557-2
Reese LSilva RTraytel D(2024)TimelyMon: A Streaming Parallel First-Order MonitorRuntime Verification10.1007/978-3-031-74234-7_9(150-160)Online publication date: 12-Oct-2024
https://doi.org/10.1007/978-3-031-74234-7_9
Hublet FLima LBasin DKrstić STraytel D(2024)Proactive Real-Time First-Order EnforcementComputer Aided Verification10.1007/978-3-031-65630-9_8(156-181)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_8
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents