Optimal proofs for linear temporal logic on lasso words

DOI10.1007/978-3-030-01090-4_3MaRDI QIDQ6109580zbMATH OpenOpenAlexFDO

Authors David Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel

Publication date 28 July 2023

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-01090-4_3

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1956579
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• scientific article; zbMATH DE number 1744956
• scientific article; zbMATH DE number 2081113
• Certifying proofs for SAT-based model checking

Cited in

(7)

• Computer says no: verdict explainability for runtime monitors using a local proof system
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Sampling polynomial trajectories for LTL verification
• MITL verification under timing uncertainty
• On ACTL formulas having linear counterexamples
• How hard is finding shortest counter-example lassos in model checking?
• Explainable online monitoring of metric temporal logic

This page was built for publication: Optimal proofs for linear temporal logic on lasso words

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