Generating BDDs for symbolic model checking in CCS

DOI10.1007/BF02242704MaRDI QIDQ2365568zbMATH OpenFDO

Authors Reinhard Enders, Thomas Filkorn, Dirk Taubner

Publication date 29 June 1993

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF02242704

zbMATH Keywords

Binary decision diagrambisimilarityCCSmodel checkingprocess algebratransition systems

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• BDD-based symbolic model checking
• scientific article; zbMATH DE number 2086590
• Improving BDD based symbolic model checking with isomorphism exploiting transition relations
• scientific article; zbMATH DE number 1487864
• Bisimulation minimization and symbolic model checking
• Symbolic bounded conformance checking of model programs

Cites work

• An implementation of an efficient algorithm for bisimulation equivalence
• Finite representations of CCS and TCSP programs by automata and Petri nets
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 177845 (Why is no real title available?)

Cited in

(9)

• An exercise in the automatic verification of asynchronous designs
• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
• Deciding bisimilarity and similarity for probabilistic processes.
• Two-layer symbolic representation for stochastic models with phase-type distributed events
• scientific article; zbMATH DE number 1786639 (Why is no real title available?)
• Symbolic model checking for probabilistic processes
• A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
• Automatic verification of distributed systems: the process algebra approach.

This page was built for publication: Generating BDDs for symbolic model checking in CCS

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