Computer says no: verdict explainability for runtime monitors using a local proof system

DOI10.1016/J.JLAMP.2020.100636MaRDI QIDQ1996872zbMATH OpenOpenAlexFDO

Authors Adrian Francalanza, Clare Cini

Publication date 26 February 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2020.100636

zbMATH Keywords

correct monitor synthesisexplainabilityinterpretabilitylinear temporal logicproof systemsruntime verification

Mathematics Subject Classification ID

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

Recommendations

• An LTL proof system for runtime verification
• Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
• Runtime verification monitor construction for three-valued PPTL
• Symbolic runtime verification for monitoring under uncertainties and assumptions
• Impartial Anticipation in Runtime-Verification

Cites work

• A brief account of runtime verification
• A framework for parameterized monitorability
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• A theory of monitors (extended abstract)
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• An LTL proof system for runtime verification
• Combining test case generation and runtime verification
• Comparing LTL semantics for runtime verification
• Completing the temporal picture
• Consistently-detecting monitors
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Cut-free sequent systems for temporal logic
• Distributed system contract monitoring
• Handbook of proof theory
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Local model checking for infinite state spaces
• Local model checking in the modal mu-calculus
• Model checking of safety properties
• Monitorability for the Hennessy-Milner logic with recursion
• Monitoring networks through multiparty session types
• Monitors and blame assignment for higher-order session types
• On the complexity of determinizing monitors
• Optimal proofs for linear temporal logic on lasso words
• Reasoning with temporal logic on truncated paths.
• Recognizing safety and liveness
• Runtime verification of temporal properties over out-of-order data streams
• Timed runtime monitoring for multiparty conversations

Cited in

(6)

• A theory of monitors
• An LTL proof system for runtime verification
• Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
• On first-order runtime enforcement of branching-time properties
• Explainable online monitoring of metric temporal logic
• A theory of fine-grained lineage for functions on structured objects

Describes a project that uses

Uses Software

• Easychair

This page was built for publication: Computer says no: verdict explainability for runtime monitors using a local proof system

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