Pages that link to "Item:Q1122572"

The following pages link to Tableau-based model checking in the propositional mu-calculus (Q1122572):

Displaying 37 items.

• Solving parity games by a reduction to SAT (Q414902) (← links)
• A game-theoretic framework for specification and verification of cryptographic protocols (Q607405) (← links)
• Modular abstractions for verifying real-time distributed systems (Q685095) (← links)
• Compositional checking of satisfaction (Q685107) (← links)
• The expressive power of implicit specifications (Q685409) (← links)
• Compositionality and locality for improving model checking in the selective mu-calculus (Q703588) (← links)
• Distributed symbolic model checking for \(\mu\)-calculus (Q816198) (← links)
• Reduced models for efficient CCS verification (Q816205) (← links)
• Model checking for hybrid logic (Q1047796) (← links)
• Local model checking in the modal mu-calculus (Q1177939) (← links)
• Local model checking for infinite state spaces (Q1190489) (← links)
• Reasoning about nondeterministic and concurrent actions: A process algebra approach (Q1277769) (← links)
• A compositional \(\mu\)-calculus proof system for statecharts processes (Q1285661) (← links)
• Model checking and boolean graphs (Q1325844) (← links)
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus (Q1325848) (← links)
• Proving properties of dynamic process networks (Q1383156) (← links)
• A graphical \(\mu\)-calculus and local model checking. (Q1433941) (← links)
• A local approach for temporal model checking of Java bytecode (Q1776379) (← links)
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus (Q1801498) (← links)
• A new logic for electronic commerce protocols (Q1853749) (← links)
• Selective mu-calculus and formula-based equivalence of transition systems (Q1970206) (← links)
• Program schemata technique for propositional program logics: a 30-year history (Q2216719) (← links)
• Bounded model checking of infinite state systems (Q2369883) (← links)
• The alternation hierarchy in fixpoint logic with chop is strict too (Q2509356) (← links)
• Probabilistic temporal logics via the modal mu-calculus (Q2566296) (← links)
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus (Q2643076) (← links)
• Minimal Proof Search for Modal Logic K Model Checking (Q2915084) (← links)
• (Q3023539) (← links)
• The mu-calculus and Model Checking (Q3176384) (← links)
• (Q4353562) (← links)
• Proving correctness of labeled transition systems by semantic tableaux (Q4610332) (← links)
• Tableau methods for PA-processes (Q4610333) (← links)
• Local model checking for context-free processes (Q4630295) (← links)
• Efficient local correctness checking for single and alternating boolean equation systems (Q4632435) (← links)
• An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability (Q4982121) (← links)
• Three notes on the complexity of model checking fixpoint logic with chop (Q5441546) (← links)
• On model checking for the \(\mu\)-calculus and its fragments (Q5941205) (← links)