Exploiting interleaving semantics in symbolic state-space generation

DOI10.1007/S10703-006-0033-YMaRDI QIDQ2642670zbMATH OpenOpenAlexFDO

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

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

Decision diagramsInterleaving semanticsKronecker algebraSymbolic state-space exploration

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 1701768
• scientific article; zbMATH DE number 1956594
• Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams
• scientific article; zbMATH DE number 1324664
• scientific article; zbMATH DE number 1507203

Cites work

• A decomposition approach for stochastic reward net models
• An O(n log n) unidirectional distributed algorithm for extrema finding in a circle
• Compositional minimisation of finite state systems using interface specifications
• Efficient descriptor-vector multiplications in stochastic automata networks
• Efficient symbolic model checking of software using partial disjunctive partitioning
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 1696452 (Why is no real title available?)
• scientific article; zbMATH DE number 1701768 (Why is no real title available?)
• scientific article; zbMATH DE number 177237 (Why is no real title available?)
• scientific article; zbMATH DE number 1956594 (Why is no real title available?)
• scientific article; zbMATH DE number 1979555 (Why is no real title available?)
• scientific article; zbMATH DE number 1863167 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• scientific article; zbMATH DE number 1423226 (Why is no real title available?)
• Partial-order reduction in symbolic state-space exploration
• Structural symbolic CTL model checking of asynchronous systems.
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(8)

• scientific article; zbMATH DE number 1701768 (Why is no real title available?)
• Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams
• Hierarchical Set Decision Diagrams and Regular Models
• Symbolic CTL model checking of asynchronous systems using constrained saturation
• scientific article; zbMATH DE number 1956594 (Why is no real title available?)
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Partially-shared zero-suppressed multi-terminal BDDs: Concept, algorithms and applications
• Improving Saturation Efficiency with Implicit Relations

Describes a project that uses

Uses Software

• CUDD
• SPIN
• NuSMV
• SMART_

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

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