A parametric analysis of the state-explosion problem in model checking

DOI10.1016/j.jcss.2005.11.003zbMath1094.68056OpenAlexW2024402979MaRDI QIDQ2495399

Yanyan Li

Publication date: 30 June 2006

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2005.11.003

zbMATH Keywords

model checkingparameterized complexitytemporal logicsbisimilaritystate-explosion problem

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Parameterized Complexity Results for 1-safe Petri Nets ⋮ Weak Kripke Structures and LTL

Cites Work

• Advice classes of parametrized tractability
• CCS expressions, finite state processes, and three problems of equivalence
• The complexity of combinatorial problems with succinct input representation
• Hierarchies of complete problems
• Complexity of some problems in Petri nets
• On the complexity of database queries
• Deciding true concurrency equivalences on safe, finite nets
• The parameterized complexity of sequence alignment and consensus
• Complexity of equivalence problems for concurrent systems of finite agents
• On the parameterized complexity of short computation and factorization
• Symbolic model checking for \(\mu\)-calculus requires exponential time
• On the complexity of verifying concurrent transition systems
• The complexity of propositional linear temporal logics in simple cases
• Preprocessing of intractable problems
• The Turing way to parameterized complexity
• Fixed-Parameter Tractability, Definability, and Model-Checking
• Algebraic laws for nondeterminism and concurrency
• The complexity of propositional linear temporal logics
• Nondeterministic Space is Closed under Complementation
• Classes of Pebble Games and Complete Problems
• Computation Models for Parameterized Complexity
• The emptiness problem for intersections of regular languages
• When is the evaluation of conjunctive queries tractable?
• Computer Science Logic
• An automata-theoretic approach to branching-time model checking
• CONCUR 2003 - Concurrency Theory
• CONCUR 2003 - Concurrency Theory
• Rudiments of \(\mu\)-calculus
• On model checking for the \(\mu\)-calculus and its fragments
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item