Coalgebraic CTL: fixpoint characterization and polynomial-time model checking

DOI10.1007/978-3-031-66438-0_1MaRDI QIDQ6666771

Ryota Kojima, Corina Cîrstea, Koko Muroya, Ichiro Hasuo

Publication date: 20 January 2025

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maximal traces and path-based coalgebraic temporal logics
• Results on the propositional \(\mu\)-calculus
• Model checking computation tree logic over finite lattices
• Using branching time temporal logic to synthesize synchronization skeletons
• Constructive versions of Tarski's fixed point theorems
• Coalgebraic logic
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Semantics of weakening and contraction
• A logic for reasoning about time and reliability
• Categorical Büchi and parity conditions via alternating fixed points of functors
• Coalgebraic modal logic: soundness, completeness and decidability of local consequence
• Decision procedures and expressiveness in the temporal logic of branching time
• Automata and fixed point logic: a coalgebraic perspective
• A lattice-theoretical fixpoint theorem and its applications
• Lattice-theoretic progress measures and coalgebraic model checking
• PSPACE bounds for rank-1 modal logics
• Terminal Coalgebras for Measure-Polynomial Functors
• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• “Sometimes” and “not never” revisited
• Bilinearity and Cartesian Closed Monads.
• Affine Monads and Side-Effect-Freeness

This page was built for publication: Coalgebraic CTL: fixpoint characterization and polynomial-time model checking