First-order temporal logic monitoring with BDDs

DOI10.1007/S10703-018-00327-4MaRDI QIDQ2225472zbMATH OpenOpenAlexFDO

Authors Klaus Havelund, Dogan Ulus, Doron Peled

Publication date 8 February 2021

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-018-00327-4

zbMATH Keywords

dataBDDspast-time temporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• First-Order Timed Runtime Verification Using BDDs
• Efficient Runtime Verification of First-Order Temporal Properties
• Quantified event automata: towards expressive and efficient runtime monitors
• Monitoring parametric temporal logic
• Monitoring metric first-order temporal properties

Cites work

• scientific article; zbMATH DE number 2080059 (Why is no real title available?)
• Completing the temporal picture
• Computer Aided Verification
• Java-MaC: A run-time assurance approach for Java programs
• Model checking of safety properties
• Monitoring metric first-order temporal properties
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Programming Languages and Systems
• Recognizing safety and liveness
• Rule systems for run-time monitoring: from EAGLE to RULER
• Symbolic model checking: \(10^{20}\) states and beyond
• Verification, Model Checking, and Abstract Interpretation
• abc : An Extensible AspectJ Compiler

Cited in

(17)

• An automata-theoretic approach to model-checking systems and specifications over infinite data domains
• Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation
• Monitoring parametric temporal logic
• Assumption-based runtime verification
• Parametric Trace Slicing and Monitoring
• Monitoring first-order interval logic
• Symbolic monitoring against specifications parametric in time and data
• Preface of the special issue on the conference on formal methods in computer-aided design 2017
• Efficient Runtime Verification of First-Order Temporal Properties
• First-Order Timed Runtime Verification Using BDDs
• Template languages for fault monitoring of timed discrete event processes
• Real-time policy enforcement with metric first-order temporal logic
• VeriMon: a formally verified monitoring tool
• Verified first-order monitoring with recursive rules
• DejaVu
• Linear Time Monitoring for One Variable TPTL
• Quantified event automata: towards expressive and efficient runtime monitors

Describes a project that uses

Uses Software

• LOLA
• Java-MOP
• Eraser
• MONA

This page was built for publication: First-order temporal logic monitoring with BDDs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225472)