scientific article; zbMATH DE number 1927551

MaRDI QIDQ4484475zbMATH OpenFDO

Authors Amir Pnueli, Yonit Kesten

Publication date 12 June 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2421/24210024.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A Sound and Complete Deductive System for CTL* Verification
• A compositional approach to CTL^* verification
• Probabilistic \(\mathrm{CTL}^*\): the deductive way
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Deductive verification of alternating systems

Cited in

(15)

• A complete proof system for propositional projection temporal logic
• A tableau-based decision procedure for CTL\(^*\)
• A compositional approach to CTL\(^*\) verification
• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Completeness and Decidability Results for CTL in Coq
• Probabilistic \(\mathrm{CTL}^*\): the deductive way
• An axiomatization of PCTL*
• scientific article; zbMATH DE number 4191139 (Why is no real title available?)
• CTL model checking in deduction modulo
• A proof system for unified temporal logic
• A decision procedure and complete axiomatization for projection temporal logic
• A Sound and Complete Deductive System for CTL* Verification
• Deductive verification of alternating systems
• Proof-based verification approaches for dynamic properties: application to the information system domain

This page was built for publication:

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