Skip to main content
SpringerLink
Log in

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems

  • Regular contribution
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Andersen HR (1994) Model checking and boolean graphs. Theor Comput Sci 126(1):3–30

    Article  MATH  MathSciNet  Google Scholar 

  2. Andersen HR, Vergauwen B (1995) Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In: Wolper P (ed) Proceedings of the 7th international conference on computer-aided verification CAV’95, Liege, Belgium, July 1995. Lecture notes in computer science, vol 939. Springer, Berlin Heidelberg New York, pp 142–154

  3. Arnold A, Crubillé P (1988) A linear algorithm to solve fixed-point equations on transition systems. Inf Process Lett 29(1):57–66

    Article  MATH  Google Scholar 

  4. Baeten JCM, van Glabbeek RJ (1987) Another look at abstraction in process algebra. In: Ottman T (ed) Proceedings of ICALP’87. Lecture notes in computer science, vol 267. Springer, Berlin Heidelberg New York, pp 84–94

  5. Bouajjani A, Fernandez J-C, Graf S, Rodríguez C, Sifakis J (1991) Safety for branching time semantics. In: Proceedings of the 18th international colloquium on automata, languages, and programming ICALP’91, Madrid, July 1991. Lecture notes in computer science, vol 510. Springer, Berlin Heidelberg New York

  6. Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677–691

    Google Scholar 

  7. Mateescu R (2005) Man page of the Caesar_Solve_1 library. INRIA Rhône-Alpes/VASY, January 2005

  8. Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Programm Lang Syst 8(2):244–263

    Article  MATH  Google Scholar 

  9. Clarke EM, Grumberg O, McMillan KL, Zhao X (1995) Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of the 32nd ACM/IEEE conference on design automation DAC’95, San Francisco, pp 427–432

  10. Cleaveland R, Parrow J, Steffen B (1993) The Concurrency Workbench: a semantics-based verification tool for finite state systems. ACM Trans Programm Lang Syst 15(1):36–72

    Article  Google Scholar 

  11. Cleaveland R, Steffen B (1991) Computing behavioural relations, logically. In: Albert JL, Monien B, Rodríguez-Artalejo M (eds) Proceedings of the 18th international colloquium on automata, languages, and programming ICALP’91, Madrid, July 1991. Lecture notes in computer science, vol 510. Springer, Berlin Heidelberg New York, pp 127–138

  12. Cleaveland R, Steffen B () A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In: Larsen KG, Skou A (eds) Proceedings of the 3rd international conference on computer-aided verification CAV’91, Aalborg, Denmark, July 1991. Lecture notes in computer science, vol 575. Springer, Berlin Heidelberg New York, pp 48–58

  13. Cleaveland R, Steffen B (1993) A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods Syst Des 2(2):121–147

    Article  MATH  Google Scholar 

  14. Dowling WF, Gallier JH (1984) Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J Logic Programm 3:267–284

    Article  MathSciNet  Google Scholar 

  15. Du X, Smolka SA, Cleaveland R (1999) Local model checking and protocol analysis. Int J Softw Tools Technol Transfer 2(3):219–241

    Article  MATH  Google Scholar 

  16. Emerson EA, Lei C-L (1986) Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of the 1st symposium on logic in computer science (LICS), pp 267–278

  17. Fantechi A, Gnesi S, Ristori G (1992) From ACTL to mu-calculus. In: Proceedings of the ERCIM workshop on theory and practice in verification, Pisa, Italy, December 1992. IEI–CNR, Pisa, pp 3–10

  18. Fernandez J-C, Jard C, Jéron T, Nedelka L, Viho C (1996) Using on-the-fly verification techniques for the generation of test suites. In: Alur R, Henzinger TA (eds) Proceedings of the 8th international conference on computer-aided verification CAV’96, New Brunswick, NJ, August 1996. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 348–359

  19. Fernandez J-C, Mounier L (1991) “On the fly” verification of behavioural equivalences and preorders. In: Larsen KG, Skou A (eds) Proceedings of the 3rd international workshop on computer-aided verification CAV’91, Aalborg, Denmark, July 1991. Lecture notes in computer science, vol 575. Springer, Berlin Heidelberg New York

  20. Fischer MJ, Ladner RE (1979) Propositional dynamic logic of regular programs. J Comput Syst Sci (18):194–211

    Article  MATH  Google Scholar 

  21. Garavel H (1998) OPEN/CAESAR: an open software architecture for verification, simulation, and testing. In: Steffen B (ed) Proceedings of the 1st international conference on tools and algorithms for the construction and analysis of systems (TACAS’98), Lisbon, Portugal, March 1998. Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 68–84. Full version available as INRIA Research Report RR-3352

  22. Garavel H, Lang F, Mateescu R (2002) An overview of CADP 2001. European Assoc Softw Sci Technol (EASST) Newslett 4:13–24. Also available as INRIA Technical Report RT-0254

    Google Scholar 

  23. Garavel H, Mateescu R (2004) SEQ.OPEN: a tool for efficient trace-based verification. In: Graf S, Mounier L (eds) Proceedings of the 11th international SPIN workshop on model checking of software SPIN’2004, Barcelona, April 2004. Lecture notes in computer science, vol 2989. Springer, Berlin Heidelberg New York, pp 150–155

  24. Groote JF, Keinänen M (2004) Solving disjunctive/conjunctive boolean equation systems with alternating fixed points. In: Jensen K, Podelski A (eds) Proceedings of the 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS’2004), Barcelona, March 2004. Lecture notes in computer science, vol 2988. Springer, Berlin Heidelberg New York, pp 436–450

  25. Groote JF, van de Pol J (2000) State space reduction using partial τ-confluence. In: Nielsen M, Rovan B (eds) Proceedings of the 25th international symposium on mathematical foundations of computer science MFCS’2000, Bratislava, Slovakia, August 2000. Lecture notes in computer science, vol 1893. Springer, Berlin Heidelberg New York, pp 383–393

  26. Hermanns H, Siegle M (1999) Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen J-P (ed) Proceedings of the 5th international AMAST workshop ARTS’99, Bamberg, Germany, May 1999. Lecture notes in computer science, vol 1601. Springer, Berlin Heidelberg New York, pp 244–265

  27. Hu AJ (1995) Techniques for efficient formal verification using binary decision diagrams. PhD thesis, Stanford University, Stanford, CA, December 1995

  28. Ingolfsdottir A, Steffen B (1994) Characteristic formulae for processes with divergence. Inf Comput 110(1):149–163

    Article  MATH  MathSciNet  Google Scholar 

  29. Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47(2):312–360

    Article  MathSciNet  Google Scholar 

  30. Larsen KG (1992) Efficient local correctness checking. In: v Bochmann G, Probst DK (eds) Proceedings of the 4th international conference on computer-aided verification CAV’92, Montréal, June–July 1992. Lecture notes in computer science, vol 663. Springer, Berlin Heidelberg New York, pp 30–43

  31. Liu X, Ramakrishnan CR, Smolka SA (1998) Fully local and efficient evaluation of alternating fixed points. In: Steffen B (ed) Proceedings of the 1st international conference on tools and algorithms for the construction and analysis of systems (TACAS’98), Lisbon, Portugal, March 1998. Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 5–19

  32. Liu X, Smolka SA (1998) Simple linear-time algorithms for minimal fixed points. In: Proceedings of the 25th international colloquium on automata, languages, and programming ICALP’98, Aalborg, Denmark. Lecture notes in computer science, vol 1443. Springer, Berlin Heidelberg New York, pp 53–66

  33. Mader A (1997) Verification of modal properties using Boolean equation systems. VERSAL 8, Bertz, Berlin

  34. Mateescu R (2000) Efficient diagnostic generation for boolean equation systems. In: Graf S, Schwartzbach M (eds) Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS’2000), Berlin, Germany, March 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 251–265. Full version available as INRIA Research Report RR-3861

  35. Mateescu R (2002) Local model-checking of modal mu-calculus on acyclic labeled transition systems. In: Katoen J-P, Stevens P (eds) Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS’2002), Grenoble, France, April 2002. Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 281–295. Full version available as INRIA Research Report RR-4430

  36. Mateescu R, Sighireanu M (2003) Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci Comput Programm 46(3):255–281

    Article  MATH  MathSciNet  Google Scholar 

  37. Milner R (1989) Communication and concurrency. Prentice-Hall, Englewood Cliffs, NJ

  38. De Nicola R, Vaandrager FW (1990) Action versus state based logics for transition systems. In: Semantics of concurrency. Lecture notes in computer science, vol 469. Springer, Berlin Heidelberg New York, pp 407–419

  39. De Nicola R, Montanari U, Vaandrager F (1990) Back and forth bisimulations. Computer Science Report CS R9021. Centrum voor Wiskunde en Informatica, Amsterdam, May 1990

  40. Pace G, Lang F, Mateescu R (2003) Calculating τ-confluence compositionally. In: Hunt WA Jr, Somenzi F (eds) Proceedings of the 15th international conference on computer-aided verification CAV’2003, Boulder, CO, July 2003. Lecture notes in computer science, vol 2725. Springer, Berlin Heidelberg New York, pp 446–459. Full version available as INRIA Research Report RR-4918

  41. Park D (1981) Concurrency and automata on infinite sequences. In: Deussen P (ed) Theoretical computer science. Lecture notes in computer science, vol 104. Springer, Berlin Heidelberg New York, pp 167–183

  42. Steffen B, Classen A, Klein M, Knoop J, Margaria T (1995) The fixpoint analysis machine. In: Lee J, Smolka SA (eds) Proceedings of the 6th international conference on concurrency theory CONCUR’95, Philadelphia, PA, August 1995. Lecture notes in computer science, vol 962. Springer, Berlin Heidelberg New York, pp 72–87

  43. Steffen B, Margaria T, Classen A, Braun V (1996) The METAFrame’95 environment. In: Alur R, Henzinger TA (eds) Proceedings of the 8th conference on computer-aided verification CAV’96, New Brunswick, NJ, August 1996. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 450–453

  44. Steffen B, Margaria T, Braun V (1997) The Electronic Tool Integration platform: concepts and design. Int J Softw Tools Technol Transfer 1–2(1):9–30

    Google Scholar 

  45. Stevens P, Stirling C (1998) Practical model-checking using games. In: Steffen B (ed) Proceedings of the 1st international conference on tools and algorithms for the construction and analysis of systems (TACAS’98), Lisbon, Portugal, March 1998. Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 85–101

  46. Tarjan RE (1972) Depth first search and linear graph algorithms. SIAM J Comput 1(2):146–160

    Article  MATH  MathSciNet  Google Scholar 

  47. Thorup M (2000) Near-optimal fully-dynamic graph connectivity. In: Proceedings of the 32nd ACM symposium on the theory of computing STOC’2000, Portland, OR

  48. van Glabbeek RJ, Weijland WP (1989) Branching-time and abstraction in bisimulation semantics (extended abstract). Computer Science Report CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam. Also in Proceedings of IFIP 11th World Computer Congress, San Francisco, 1989

  49. Vergauwen B, Lewi J (1992) A linear algorithm for solving fixed-point equations on transition systems. In: Proceedings of the 17th colloquium on trees in algebra and programming CAAP’92, Rennes, France, February 1992. Lecture notes in computer science, vol 581. Springer, Berlin Heidelberg New York, pp 322–341

  50. Vergauwen B, Lewi J (1994) Efficient local correctness checking for single and alternating boolean equation systems. In: Abiteboul S, Shamir E (eds) Proceedings of the 21st international colloquium on automata, logic, and programming ICALP’94, Vienna, July 1994. Lecture notes in computer science, vol 820. Springer, Berlin Heidelberg New York, pp 304–315

  51. Vergauwen B, Wauman J, Lewi J (1994) Efficient fixpoint computation. In: Proceedings of the 1st international symposium on static analysis (SAS’94), Namur, Belgium, September 1994. Lecture notes in computer science, vol 864. Springer, Berlin Heidelberg New York, pp 314–328

  52. Yang B, Bryant RE, O’Hallaron DR, Biere A, Coudert O, Janssen G, Ranjan RK, Somenzi F (1998) A performance study of BDD-based model-checking. In: Proceedings of FMCAD’98. Lecture notes in computer science, vol 1522. Springer, Berlin Heidelberg New York, pp 255–289

Download references

Author information

Authors and Affiliations

  1. INRIA Rhône-Alpes/VASY, 655, avenue de l’Europe, 38330, Montbonnot St Martin, France

    Radu Mateescu

Authors
  1. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Radu Mateescu.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Mateescu, R. CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems. Int J Softw Tools Technol Transfer 8, 37–56 (2006). https://doi.org/10.1007/s10009-005-0194-9

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-005-0194-9

Keywords

Search

Navigation