Skip to main content

Mosel: A flexible toolset for monadic second-order logic

Part of the Lecture Notes in Computer Science book series (LNCS,volume 1217)

Abstract

Mosel is a new tool-set for the analysis and verification in Monadic Second-order Logic. In this paper we concentrate on the system's design: Mosel is a tool-set to include a flexible set of decision procedures for several theories of the logic complemented by a variety of support components for input format translations, visualization, and interfaces to other logics and tools. The main distinguishing features of Mosel are its layered approach to the logic, based on a formal semantics for a minimal subset, its modular design, and its integration in a heterogeneous analysis and verification environment.

Keywords

  • Boolean Function
  • Decision Procedure
  • Edge Label
  • Finite State Automaton
  • Sequential Circuit

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. S. Akers: “Binary Decision Diagrams,” IEEE Trans. on Comp. Vol.C-27, 1978, pp. 509–516.

    Google Scholar 

  2. D. Basin, N. Klarlund: “Hardware verification using monadic second-order logic,” Proc. CAV '95, Liège (B), July 1995, LNCS N. 939, Springer Verlag, pp. 31–41.

    Google Scholar 

  3. N. Bjørner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H. Sipma, T. Uribe: “STeP: Deductive-algorithmic verification of reactive and real-time systems,” Proc. CAV'96, New Brunswick, NJ (USA), Aug. 1996, LNCS N. 1102, Springer Verlag, pp. 415–418.

    Google Scholar 

  4. M. von der Beeck, V. Braun, A. Claßen, A. Dannecker, C. Friedrich, D. Koschützki, T. Margaria, F. Schreiber and B. Steffen: “Graphs in MetaFrame: The Unifying Power of Polymorphism,” Proc. TACAS'97, Enschede (NL), April 1997, in this same Volume of LNCS, Springer.

    Google Scholar 

  5. J. Burch, E. Clarke, K. McMillan, D. Dill, L. Hwang: “Symbolic model checking: 1020 states and beyond,” Proc. LICS'90, Philadelphia, 1990, pp. 428–439.

    Google Scholar 

  6. R.E. Bryant: “Graph-based algorithms for Boolean function manipulation,” IEEE Trans. Computing, vol. C-35(8), August 1986, pp. 677–691.

    Google Scholar 

  7. R. E. Bryant: “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Surveys Vol. 4, 1992, pp. 293–318.

    Google Scholar 

  8. J.R. Büchi: “Weak second-order arithmetic and finite automata,” Z. Math. Logik Grundl. Math., Vol. 6, 1960, pp. 66–92.

    Google Scholar 

  9. A. Church: “Logic, arithmetic and automata,” Proc. Int. Congr. Math., Almqvist and Wiksells, Uppsala 1963, pp. 23–35.

    Google Scholar 

  10. daVinci: the tool is available via ftp at site ftp://ftp.uni-bremen.de/pub/ graphics/daVinci

    Google Scholar 

  11. C. Friedrich: “The ffgraph library,” Techn. Rep. MIP-9520, Fakultät für Mathematik und Informatik, Universität Passau, December 1995.

    Google Scholar 

  12. J. Hopcroft: “An n log n algorithm for minimizing states in a finite automaton,” Proc. Int. Symp. on Theory of Machines and Computations, Technion, Haifa (IL), Aug. 1971, pp.189–196.

    Google Scholar 

  13. P. Kelb: “Abstraktionstechniken für automatische Verifikationsmethoden,” Ph.D. Diss., Univ. of Oldenburg (Germany), Dec. 1995, Shaker Verlag, Aachen (D).

    Google Scholar 

  14. J. Henriksen, J. Jensen, M. Jørgensen N. Klarlund, R. Paige, T. Rauhe, A. Sandholm: “Mona: Monadic second-order logic in practice,” Proc. TACAS'95, Århus (DK), May 1995, LNCS 1019, Springer V., pp. 89–110.

    Google Scholar 

  15. N. Klarlund, M. Nielsen, K. Sunesen: “A Case Study in Verification Based on Trace Abstractions,” in M. Broy, S. Merz, K. Spies (eds.), Formal Systems Verification — The RPC-Memory Specification Case Study, LNCS N. 1169, Springer V., Nov. 1996.

    Google Scholar 

  16. T. Margaria, M. Mendler: “Automatic Treatment of Sequential Circuits in Second-Order Monadic Logic”, 4th GI/ITG/GME Worksh. on Methoden des Entwurfs und der Verifikation digitaler Systeme, Kreischa (D), March 1996, Shaker Verlag.

    Google Scholar 

  17. T. Margaria, M. Mendler: “Model-based Automatic Synthesis and Analysis in Second-Order Monadic Logic,” Proc. AAS'97, ACM/SIGPLAN Int. Worksh. on Automated Analysis of Software, Paris (F), Jan. 1997, pp.99–112.

    Google Scholar 

  18. T. Margaria: “Fully Automatic Verification and Error Detection for Parametérized Iterative Sequential Circuits”, Proc. TACAS'96, Passau (D), March 1996, LNCS N.1055, Springer Verlag, pp. 258–277.

    Google Scholar 

  19. T. Margaria: “Verification of Systolic Arrays in M2L(Str),” Techn. Rep. MIP-9613, Fakultät für Mathematik und Informatik, Universität Passau, July 1996.

    Google Scholar 

  20. O. Matz, A. Miller, A. Potthoff, W. Thomas, E. Valkema: “Report on the Program AMoRE”, Techn. Rep. Nr. 9507, Inst. für Informatik und Praktische Mathematik, Universität Kiel (D), 1995.

    Google Scholar 

  21. J.K. Ousterhout: “Tcl and the Tk Toolkit,” Addison-Wesley, April 1994.

    Google Scholar 

  22. R. Paige, R. Tarjan: “Three partition refinement algorithms,” SIAM Journ. of Computation, Vol.16, N.6, Dec. 1987, pp.973–989.

    Google Scholar 

  23. K. S. Brace, R. L. Rudell, R. E. Bryant: “Efficient Implementation of a BDD Package,” Proc. DAC'90, Orlando, FL, June 1990, pp. 40–45.

    Google Scholar 

  24. B. Steffen, T. Margaria, A. Claßen, V. Braun: “Incremental Formalization: A Key to Industrial Success”, In “SOFTWARE: Concepts and Tools”, Vol. 17, No 2, pp. 78–91, Springer Verlag, July 1996.

    Google Scholar 

  25. B. Steffen, T. Margaria, A. Claßen, V. Braun: “The MetaFrame'95 Environment”, (Experience Report for the Industry Day), Proc. CAV'96, Juli–Aug. 1996, New Brunswick, NJ, USA, LNCS N.1102, Springer Verlag, pp.450–453.

    Google Scholar 

  26. B. Steffen, T. Margaria, A. Claßen: “Heterogeneous Analysis and Verification for Distributed Systems”, In “SOFTWARE: Concepts and Tools”, vol. 17, N.1, pp. 13–25, Springer Verlag, 1996.

    Google Scholar 

  27. W. Thomas: “Automata on infinite objects,” In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, p. 133–191. MIT Press/Elsevier, 1990.

    Google Scholar 

  28. W. Thomas: “Languages, automata, and objects,” to appear in the forthcoming new edition of the Handbook of Theoretical Computer Science, MIT Press/Elsevier.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and Permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kelb, P., Margaria, T., Mendler, M., Gsottberger, C. (1997). Mosel: A flexible toolset for monadic second-order logic. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035388

Download citation

  • DOI: https://doi.org/10.1007/BFb0035388

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62790-6

  • Online ISBN: 978-3-540-68519-7

  • eBook Packages: Springer Book Archive