Three notes on the complexity of model checking fixpoint logic with chop

DOI10.1051/ITA:2007011MaRDI QIDQ5441546zbMATH OpenOpenAlexFDO

Authors Martin Lange

Publication date 15 February 2008

Published in RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL http://www.numdam.org/item?id=ITA_2007__41_2_177_0, https://eudml.org/doc/92838, https://semanticscholar.org/paper/d8f1a21768da4fc8e88311a74de7ad876a6e443e

zbMATH Keywords

complexityfixpoint calculus with Chopmodel checkingmu-calculus

Mathematics Subject Classification ID

Temporal logic (03B44) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2087435
• scientific article; zbMATH DE number 1927566
• scientific article; zbMATH DE number 1304336
• Parallel and symbolic model checking for fixpoint logic with chop
• The Complexity of Model Checking Higher-Order Fixpoint Logic

Cites work

• Alternating context-free languages and linear time -calculus with sequential composition
• An improved algorithm for the evaluation of fixpoint expressions
• Automata, logics, and infinite games. A guide to current research
• CONCUR 2004 - Concurrency Theory
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Fast and simple nested fixpoints
• scientific article; zbMATH DE number 1304336 (Why is no real title available?)
• scientific article; zbMATH DE number 1927566 (Why is no real title available?)
• scientific article; zbMATH DE number 1500523 (Why is no real title available?)
• scientific article; zbMATH DE number 2087435 (Why is no real title available?)
• scientific article; zbMATH DE number 1841826 (Why is no real title available?)
• Mathematical Foundations of Computer Science 2005
• On model checking for the -calculus and its fragments
• Programming languages and their definition. Selected papers ed. by C. B. Jones
• Pushdown processes: Games and model-checking
• Results on the propositional \(\mu\)-calculus
• Tableau-based model checking in the propositional mu-calculus

Cited in

(11)

• Temporal logic with recursion
• The alternation hierarchy in fixpoint logic with chop is strict too
• Parallel and symbolic model checking for fixpoint logic with chop
• The complexity of independence-friendly fixpoint logic
• scientific article; zbMATH DE number 1304336 (Why is no real title available?)
• scientific article; zbMATH DE number 1927566 (Why is no real title available?)
• scientific article; zbMATH DE number 2087435 (Why is no real title available?)
• Theoretical Aspects of Computing – ICTAC 2005
• Temporal Logic with Recursion.
• Separating the expressive power of propositional dynamic and modal fixpoint logics
• Propositional dynamic logic of context-free programs and fixpoint logic with chop

This page was built for publication: Three notes on the complexity of model checking fixpoint logic with chop

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