Model Checking CTL is Almost Always Inherently Sequential

DOI10.2168/LMCS-7(2:12)2011MaRDI QIDQ3003330zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 26 May 2011

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-7(2:12)2011

zbMATH Keywords

complexitycomputation tree logicmodel checkingtemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model Checking Timed Recursive CTL.
• scientific article; zbMATH DE number 2102723
• scientific article; zbMATH DE number 2102715
• scientific article; zbMATH DE number 2080197
• Model checking CTL over restricted classes of automatic structures
• Model checking for graded CTL
• CTL model checking in deduction modulo
• Efficient CTL model-checking for pushdown systems

Cited in

(17)

• A two-level approach based on model checking to support architecture conformance checking
• The model checking fingerprints of CTL operators
• CTL model checking on a shared-memory architecture
• An axiomatization of PCTL*
• scientific article; zbMATH DE number 1705163 (Why is no real title available?)
• Complexity of model checking for modal dependence logic
• Model checking EGF on basic parallel processes
• scientific article; zbMATH DE number 177249 (Why is no real title available?)
• scientific article; zbMATH DE number 177502 (Why is no real title available?)
• On the applicability of Post's lattice
• Quirky quantifiers: optimal models and complexity of computation tree logic
• An experiment on parallel model checking of a CTL fragment
• Parametrised complexity of satisfiability in temporal logic
• Distributed Computing - IWDC 2004
• CTL may be ambiguous when model checking Moore machines
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs
• Taking Some Burden Off an Explicit CTL Model Checker

This page was built for publication: Model Checking CTL is Almost Always Inherently Sequential

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