Advertisement

Generating BDD models for process algebra terms

  • Ashvin Dsouza
  • Bard Bloom
Session 2: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

The Simple systems form a class of process algebras whose operational semantics can be specified using finite state labelled transition systems. In this work, we describe how to efficiently derive the ordered Binary Decision Diagrams (BDDs) corresponding to the operational semantics of the terms of an arbitrary Simple system. Model checking using such BDDs can often significantly speedup the testing of properties such as bisimilarity over direct algorithms. We also introduce a useful extension of Simple providing explicit recursion. For the CCS operators, we show that the corresponding BDD operators we generate automatically are comparable to those coded by hand.

Keywords

Model Check Boolean Function Transition System Simple System Transition Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [ABV94]
    Luca Aceto, Bard Bloom, and Frits Vaandrager. Turning SOS rules into equations. Information and Computation, 111(1):1–52, May 1994. (Special Issue for LICS '92).Google Scholar
  2. [Ace93]
    Luca Aceto. GSOS and finite labelled transition systems. Technical Report 6/93, University of Sussex at Brighton, March 1993.Google Scholar
  3. [BCL91]
    J. Burch, E. Clarke, and D. Long. Symbolic model checking with partitioned transition relations. In VLSI 91, Edinburgh, Scotland, 1991.Google Scholar
  4. [BCM+90]
    J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In Logic in Computer Science, 1990.Google Scholar
  5. [BdS92]
    A. Bouali and R. de Simone. Symbolic bisimulation minimization. In Computer Aided Verification, volume 663 of LNCS, 1992.Google Scholar
  6. [Blo90]
    Bard Bloom. Ready Simulation, Bisimulation and the semantics of CCS-like languages. PhD thesis, MIT, Cambridge, Massachusetts, October 1990.Google Scholar
  7. [Bry86]
    R. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, 8 1986.Google Scholar
  8. [CWB92]
    The Edinburgh Concurrency Workbench, version 6.1, 1992. Available by ftp from ftp.dcs.ed.ac.uk, directory export/cwb/CWB6.1.Google Scholar
  9. [Dam93]
    Mads Dam. Model checking mobile processes. CONCUR 93, 1993.Google Scholar
  10. [DB95]
    A. Dsouza and B. Bloom. Applying symbolic model checking to process algebras, 1995. http: //www.cs.cornell.edu/Info/People/dsouza/pa2bdd.ps.Google Scholar
  11. [dS85]
    R. de Simone. Higher-level synchronizing devices in MEIJE-SCCS. Theoretical Computer Science, 37(3):245–267, 1985.CrossRefGoogle Scholar
  12. [dSV89]
    R. de Simone and D. Vergamini. Aboard Auto. Technical Report Rapports Techniques 111, INRIA, Sophia Antipolis, 1989.Google Scholar
  13. [EFT93]
    R. Enders, T. Filkhorn, and D. Taubner. Generating BDDs for symbolic model checking in CCS. Distributed Computing, 6:155–164, 1993.Google Scholar
  14. [Fer89]
    J-C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13:219–236, 1989.Google Scholar
  15. [FKM93]
    J-C. Fernandez, A. Kerbrat, and L. Mounier. Symbolic equivalence checking. In Computer Aided Verification, 1993.Google Scholar
  16. [GV90]
    J.F. Groote and F. Vandraager. An efficient algorithm for branching bisimulation and stuttering equivalence. In ICALP '90, Lecture Notes in Computer Science. Springer Verlag, 1990.Google Scholar
  17. [Lon93]
    David Long, bdd: A Binary Decision Diagram (BDD) package, 1993. Available by FTP from emc.cs.cmu.edu (pub/bdd/bddlib.tar.Z).Google Scholar
  18. [LOT]
    LOTOSphere is available by FTP from ftp.cs.utwente.nl.Google Scholar
  19. [Mil89]
    Robin Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, New York, 1989.Google Scholar
  20. [MM93]
    G. Milne and G. McCaskill. Sequential circuit analysis with a BDD based process algebra system. Technical Report HDV-25-93, University of Strathclyde, 1993.Google Scholar
  21. [Par81]
    D. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Theoretical Computer Science, Lect. Notes in Computer Sci., page 261. Springer-Verlag, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ashvin Dsouza
    • 1
  • Bard Bloom
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations