Exploiting interleaving semantics in symbolic state-space generation

DOI10.1007/S10703-006-0033-YzbMath1118.68533OpenAlexW2039212262MaRDI QIDQ2642670

Gianfranco Ciardo, Andrew S. Miner, Gerald Lüttgen

Publication date: 17 August 2007

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-006-0033-y

zbMATH Keywords

Kronecker algebraDecision diagramsInterleaving semanticsSymbolic state-space exploration

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items (4)

Partially-shared zero-suppressed multi-terminal BDDs: Concept, algorithms and applications ⋮ Improving Saturation Efficiency with Implicit Relations ⋮ Hierarchical Set Decision Diagrams and Regular Models ⋮ Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation

Uses Software

• SPIN
• SMART_
• NuSMV
• CUDD

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• Compositional minimisation of finite state systems using interface specifications
• Efficient descriptor-vector multiplications in stochastic automata networks
• Graph-Based Algorithms for Boolean Function Manipulation
• An O(n log n) unidirectional distributed algorithm for extrema finding in a circle
• A decomposition approach for stochastic reward net models
• Correct Hardware Design and Verification Methods
• Computer Aided Verification
• Partial-order reduction in symbolic state-space exploration
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Exploiting interleaving semantics in symbolic state-space generation