Generating BDDs for symbolic model checking in CCS

DOI10.1007/BF02242704zbMath0778.68063MaRDI QIDQ2365568

Thomas Filkorn, Reinhard Enders, Dirk Taubner

Publication date: 29 June 1993

Published in: Distributed Computing (Search for Journal in Brave)

zbMATH Keywords

process algebramodel checkingtransition systemsCCSbisimilarityBinary decision diagram

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)

Related Items

An exercise in the automatic verification of asynchronous designs, Combining static analysis and case-based search space partitioning for reducing peak memory in model checking, Symbolic model checking for probabilistic processes, On the use of MTBDDs for performability analysis and verification of stochastic systems., Deciding bisimilarity and similarity for probabilistic processes., Automatic verification of distributed systems: the process algebra approach., Two-layer symbolic representation for stochastic models with phase-type distributed events, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria

Cites Work

• Unnamed Item
• 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