The fixed-parameter tractability of model checking concurrent systems

DOI10.4230/LIPICS.CSL.2013.332MaRDI QIDQ2958531zbMATH OpenFDO

Authors Stefan Göller

Publication date 2 February 2017

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2013.332

zbMATH Keywords

model checkingparameterized complexityconcurrent systems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Concurrency makes simple theories hard
• scientific article; zbMATH DE number 2196601
• Satisfiability and model checking for MSO-definable temporal logics are in PSPACE.
• Distributed Computing - IWDC 2004
• Parametric temporal logic for “model measuring”

Cited in

(9)

• Compact and efficiently verifiable models for concurrent systems
• On the complexity of verifying concurrent transition systems
• The complexity of model checking multi-stack systems
• Model checking concurrent programs with nondeterminism and randomization
• Concurrency makes simple theories hard
• On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
• scientific article; zbMATH DE number 967185 (Why is no real title available?)
• The Complexity of Model Checking Multi-stack Systems
• Model checking of concurrent software systems via heuristic-guided SAT solving

This page was built for publication: The fixed-parameter tractability of model checking concurrent systems

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