Rewrite rules for \(\mathrm{CTL}^\ast\)

DOI10.1016/j.jal.2016.12.003zbMath1436.03124OpenAlexW2565989685MaRDI QIDQ518745

John C. McCabe-Dansted, M. A. 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

verificationtableau\(\mathrm{CTL}\)bundled logicnon-local logicrewrite

Mathematics Subject Classification ID

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

Related Items (2)

Unnamed Item ⋮ Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)

Uses Software

• AProVE
• CiME
• Waldmeister

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A tableau-based decision procedure for CTL\(^*\)
• Using branching time temporal logic to synthesize synchronization skeletons
• Rewrite method for theorem proving in first order theory with equality
• A refutational approach to geometry theorem proving
• Propositional dynamic logic of regular programs
• Decision procedures and expressiveness in the temporal logic of branching time
• An axiomatization of full Computation Tree Logic
• A Rooted Tableau for BCTL*
• A Tableau for Bundled CTL
• Deciding full branching time logic
• Logic and time
• On Non-local Propositional and Weak Monodic Quantified CTL*
• Branching-time logic with quantification over branches: The point of view of modal logic
• A Decision Procedure for CTL* Based on Tableaux and Automata
• Axioms for Branching Time

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