A stubborn attack on state explosion
From MaRDI portal
Publication:685106
DOI10.1007/BF00709154zbMath0783.68083MaRDI QIDQ685106
Publication date: 30 September 1993
Published in: Formal Methods in System Design (Search for Journal in Brave)
temporal logicreduced state spaces\(LTL\)-preserving stubborn set methodautomatic verification of concurrent systems
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Star-Topology Decoupling in SPIN ⋮ Stubborn set reduction for timed reachability and safety games ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ Stutter-invariant temporal properties are expressible without the next-time operator ⋮ Combining static analysis and case-based search space partitioning for reducing peak memory in model checking ⋮ Stubborn versus structural reductions for Petri nets ⋮ Automata Theory and Model Checking ⋮ Automata-driven partial order reduction and guided search for LTL model checking ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Permutation rewriting and algorithmic verification ⋮ An application of temporal projection to interleaving concurrency ⋮ Unnamed Item ⋮ Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving ⋮ Partial-order reduction in the weak modal mu-calculus ⋮ On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ An algorithmic approach for checking closure properties of Ω-regular languages ⋮ Exponential automatic amortized resource analysis ⋮ The inconsistent labelling problem of stutter-preserving partial-order reduction ⋮ Transparent partial order reduction ⋮ Partial order reduction for reachability games ⋮ Star-topology decoupled state space search ⋮ AN EXPRESSIVE EXTENSION OF TLC ⋮ Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems ⋮ On commutativity based edge lean search ⋮ Difficult configurations -- on the complexity of LTrL ⋮ On stubborn sets in the verification of linear time temporal properties ⋮ An expressively complete linear time temporal logic for Mazurkiewicz traces ⋮ An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ Exploring the Scope for Partial Order Reduction ⋮ Specification Languages for Stutter-Invariant Regular Properties ⋮ Unnamed Item ⋮ More efficient on-the-fly LTL verification with Tarjan's algorithm ⋮ A valuation-based analysis of conflict-free Petri nets
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A partial approach to model checking
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- Interleaving set temporal logic
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- A Theory of Communicating Sequential Processes
