An LTL proof system for runtime verification

DOI10.1007/978-3-662-46681-0_54MaRDI QIDQ5194962zbMATH OpenOpenAlexFDO

Authors Clare Cini, Adrian Francalanza

Publication date 17 September 2019

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-46681-0_54

zbMATH Keywords

deductive systemlinear temporal logicproof obligationproof systemproof tree

Mathematics Subject Classification ID

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

Recommendations

• Computer says no: verdict explainability for runtime monitors using a local proof system
• Comparing LTL semantics for runtime verification
• Decentralized asynchronous crash-resilient runtime verification
• Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
• Runtime verification monitor construction for three-valued PPTL

Cited in

(22)

• Computer says no: verdict explainability for runtime monitors using a local proof system
• Declarative stream runtime verification (hLola)
• A theory of monitors
• Certifying proofs for SAT-based model checking
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Probabilistic causes in Markov chains
• Monitorability for the Hennessy-Milner logic with recursion
• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• Comparing LTL semantics for runtime verification
• Runtime verification using a temporal description logic
• Decentralized asynchronous crash-resilient runtime verification
• Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
• Runtime verification monitor construction for three-valued PPTL
• Runtime verification through forward chaining
• On runtime enforcement via suppressions
• \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system
• LMS-Verify: abstraction without regret for verified systems programming
• Decentralized Asynchronous Crash-resilient Runtime Verification
• An Operational Guide to Monitorability
• Decentralized LTL enforcement
• Organising LTL monitors over distributed systems with a global clock
• The ins and outs of first-order runtime verification

This page was built for publication: An LTL proof system for runtime verification

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