Monitoring Metric First-Order Temporal Properties

DOI10.1145/2699444zbMath1333.68177OpenAlexW2267240189MaRDI QIDQ2796403

Felix Klaedtke, Eugen Zălinescu, Samuel Müller, David A. Basin

Publication date: 24 March 2016

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2699444

zbMATH Keywords

temporal databasesautomatic structuresruntime verificationsecurity policiescompliance checking

Mathematics Subject Classification ID

Database theory (68P15) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (22)

Efficient Runtime Verification of First-Order Temporal Properties ⋮ Algorithms for monitoring real-time properties ⋮ On the complexity of monitoring Orchids signatures, and recurrence equations ⋮ Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic ⋮ Monitoring first-order interval logic ⋮ Decentralized runtime verification of message sequences in message-based systems ⋮ Temporal Minimal-World Query Answering over Sparse ABoxes ⋮ Real-time policy enforcement with metric first-order temporal logic ⋮ VeriMon: a formally verified monitoring tool ⋮ Linear Time Monitoring for One Variable TPTL ⋮ Efficient Evaluation of Arbitrary Relational Calculus Queries ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ First-order temporal logic monitoring with BDDs ⋮ Adaptive Online First-Order Monitoring ⋮ Multi-head Monitoring of Metric Temporal Logic ⋮ Almost Event-Rate Independent Monitoring of Metric Temporal Logic ⋮ Scalable offline monitoring of temporal specifications ⋮ Almost event-rate independent monitoring ⋮ A survey of challenges for runtime verification from advanced application domains (beyond software) ⋮ Extended Nested Dual System Groups, Revisited ⋮ An automata-theoretic approach to model-checking systems and specifications over infinite data domains ⋮ A formally verified, optimized monitor for metric first-order dynamic logic

Uses Software

• MapReduce
• MONA
• Java-MOP
• PostgreSQL
• MonPoly
• LOLA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decentralised LTL monitoring
• Scalable offline monitoring of temporal specifications
• Defining liveness
• Monitoring dynamic integrity constraints based on temporal logic
• Sooner is safer than later
• Finite presentations of infinite structures: Automata and interpretations
• Checking finite traces using alternating automata
• On the feasibility of checking temporal integrity constraints
• Semantics and Algorithms for Parametric Monitoring
• MONA IMPLEMENTATION SECRETS
• A First-Order Policy Language for History-Based Transaction Monitoring
• Querying ATSQL databases with temporal logic
• Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking
• Comparing LTL Semantics for Runtime Verification
• Rule Systems for Run-time Monitoring: from EAGLE to RULER
• From Philosophical to Industrial Logics
• Specifying and Reasoning About Dynamic Access-Control Policies
• Runtime Verification Using a Temporal Description Logic
• A really temporal logic
• Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• The Recursive Unsolvability of the Decision Problem for the Class of Definite Formulas
• Verification, Model Checking, and Abstract Interpretation
• Symbolic model checking with rich assertional languages

This page was built for publication: Monitoring Metric First-Order Temporal Properties