Rewrite rules for CTL^

DOI10.1016/J.JAL.2016.12.003MaRDI QIDQ518745zbMATH OpenOpenAlexFDO

Authors John Christopher McCabe-Dansted, Mark Alexander Reynolds

Publication date 30 March 2017

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jal.2016.12.003

zbMATH Keywords

\(\mathrm{CTL}\)bundled logicnon-local logicrewritetableauverification

Mathematics Subject Classification ID

Temporal logic (03B44) Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 2090074
• A faster tableau for \(\mathrm{CTL}^{\ast}\)
• A tableau-based decision procedure for CTL^*
• The Temporal Logic of Rewriting: A Gentle Introduction
• Decision procedures and expressiveness in the temporal logic of branching time

Cites work

• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• A refutational approach to geometry theorem proving
• A rooted tableau for \(\mathrm{BCTL}^*\)
• A Tableau for Bundled CTL
• A tableau-based decision procedure for CTL^*
• An axiomatization of full computation tree logic
• Automated certified proofs with CiME3
• Axioms for Branching Time
• Branching-time logic with quantification over branches: The point of view of modal logic
• Deciding full branching time logic
• Decision procedures and expressiveness in the temporal logic of branching time
• Handbook of modal logic
• scientific article; zbMATH DE number 1059246 (Why is no real title available?)
• scientific article; zbMATH DE number 2090074 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Logic and time
• On Non-local Propositional and Weak Monodic Quantified CTL*
• Propositional dynamic logic of regular programs
• Rewrite method for theorem proving in first order theory with equality
• Using branching time temporal logic to synthesize synchronization skeletons

Cited in

(6)

• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• From linear temporal logic properties to rewrite propositions
• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• CTL model checking in deduction modulo
• The Temporal Logic of Rewriting: A Gentle Introduction
• scientific article; zbMATH DE number 2090074 (Why is no real title available?)

Describes a project that uses

Uses Software

• AProVE
• CiME
• Waldmeister

This page was built for publication: Rewrite rules for \(\mathrm{CTL}^\ast\)

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