A Sound and Complete Deductive System for CTL* Verification

DOI10.1093/JIGPAL/JZN018MaRDI QIDQ5504119zbMATH OpenOpenAlexFDO

Authors Amir Pnueli, Dov Gabbay

Publication date 21 January 2009

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL http://orbilu.uni.lu/handle/10993/26059

Mathematics Subject Classification ID

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

Recommendations

• A compositional approach to CTL^* verification
• scientific article; zbMATH DE number 1927551
• Verification of temporal properties
• Probabilistic \(\mathrm{CTL}^*\): the deductive way
• CTL model checking in deduction modulo

Cited in

(11)

• A compositional approach to CTL^* verification
• Twenty years of rewriting logic
• Probabilistic \(\mathrm{CTL}^*\): the deductive way
• Completeness and Decidability Results for CTL in Coq
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• CTL model checking in deduction modulo
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• scientific article; zbMATH DE number 1927551 (Why is no real title available?)
• Cognitive economics and the logic of abduction
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• Deductive verification of alternating systems

This page was built for publication: A Sound and Complete Deductive System for CTL* Verification

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