{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:31:53Z","timestamp":1778297513640,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540627906","type":"print"},{"value":"9783540685197","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0035388","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:28:40Z","timestamp":1138202920000},"page":"183-202","source":"Crossref","is-referenced-by-count":22,"title":["Mosel: A flexible toolset for monadic second-order logic"],"prefix":"10.1007","author":[{"given":"Peter","family":"Kelb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiziana","family":"Margaria","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudia","family":"Gsottberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,26]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S. Akers","year":"1978","unstructured":"S. Akers: \u201cBinary Decision Diagrams,\u201d IEEE Trans. on Comp. Vol.C-27, 1978, pp. 509\u2013516.","journal-title":"IEEE Trans. on Comp."},{"key":"13_CR2","series-title":"LNCS","first-page":"31","volume-title":"Proc. CAV '95","author":"D. Basin","year":"1995","unstructured":"D. Basin, N. Klarlund: \u201cHardware verification using monadic second-order logic,\u201d Proc. CAV '95, Li\u00e8ge (B), July 1995, LNCS N. 939, Springer Verlag, pp. 31\u201341."},{"key":"13_CR3","series-title":"LNCS","first-page":"415","volume-title":"Proc. CAV'96","author":"N. Bj\u00f8rner","year":"1996","unstructured":"N. Bj\u00f8rner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H. Sipma, T. Uribe: \u201cSTeP: Deductive-algorithmic verification of reactive and real-time systems,\u201d Proc. CAV'96, New Brunswick, NJ (USA), Aug. 1996, LNCS N. 1102, Springer Verlag, pp. 415\u2013418."},{"key":"13_CR4","series-title":"LNCS","volume-title":"Proc. TACAS'97","author":"M. Beeck von der","year":"1997","unstructured":"M. von der Beeck, V. Braun, A. Cla\u00dfen, A. Dannecker, C. Friedrich, D. Kosch\u00fctzki, T. Margaria, F. Schreiber and B. Steffen: \u201cGraphs in MetaFrame: The Unifying Power of Polymorphism,\u201d Proc. TACAS'97, Enschede (NL), April 1997, in this same Volume of LNCS, Springer."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, L. Hwang: \u201cSymbolic model checking: 1020 states and beyond,\u201d Proc. LICS'90, Philadelphia, 1990, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"issue":"8","key":"13_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant: \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Trans. Computing, vol. C-35(8), August 1986, pp. 677\u2013691.","journal-title":"IEEE Trans. Computing"},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"4","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant: \u201cSymbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,\u201d ACM Computing Surveys Vol. 4, 1992, pp. 293\u2013318.","journal-title":"ACM Computing Surveys"},{"key":"13_CR8","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J.R. B\u00fcchi","year":"1960","unstructured":"J.R. B\u00fcchi: \u201cWeak second-order arithmetic and finite automata,\u201d Z. Math. Logik Grundl. Math., Vol. 6, 1960, pp. 66\u201392.","journal-title":"Z. Math. Logik Grundl. Math."},{"key":"13_CR9","first-page":"23","volume-title":"Proc. Int. Congr. Math.","author":"A. Church","year":"1963","unstructured":"A. Church: \u201cLogic, arithmetic and automata,\u201d Proc. Int. Congr. Math., Almqvist and Wiksells, Uppsala 1963, pp. 23\u201335."},{"key":"13_CR10","unstructured":"daVinci: the tool is available via ftp at site ftp:\/\/ftp.uni-bremen.de\/pub\/ graphics\/daVinci"},{"key":"13_CR11","unstructured":"C. Friedrich: \u201cThe ffgraph library,\u201d Techn. Rep. MIP-9520, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau, December 1995."},{"key":"13_CR12","first-page":"189","volume-title":"An n log n algorithm for minimizing states in a finite automaton","author":"J. Hopcroft","year":"1971","unstructured":"J. Hopcroft: \u201cAn n log n algorithm for minimizing states in a finite automaton,\u201d Proc. Int. Symp. on Theory of Machines and Computations, Technion, Haifa (IL), Aug. 1971, pp.189\u2013196."},{"key":"13_CR13","volume-title":"Ph.D. Diss.","author":"P. Kelb","year":"1995","unstructured":"P. Kelb: \u201cAbstraktionstechniken f\u00fcr automatische Verifikationsmethoden,\u201d Ph.D. Diss., Univ. of Oldenburg (Germany), Dec. 1995, Shaker Verlag, Aachen (D)."},{"key":"13_CR14","series-title":"LNCS 1019","first-page":"89","volume-title":"Proc. TACAS'95","author":"J. Henriksen","year":"1995","unstructured":"J. Henriksen, J. Jensen, M. J\u00f8rgensen N. Klarlund, R. Paige, T. Rauhe, A. Sandholm: \u201cMona: Monadic second-order logic in practice,\u201d Proc. TACAS'95, \u00c5rhus (DK), May 1995, LNCS 1019, Springer V., pp. 89\u2013110."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"N. Klarlund, M. Nielsen, K. Sunesen: \u201cA Case Study in Verification Based on Trace Abstractions,\u201d in M. Broy, S. Merz, K. Spies (eds.), Formal Systems Verification \u2014 The RPC-Memory Specification Case Study, LNCS N. 1169, Springer V., Nov. 1996.","DOI":"10.1007\/BFb0024435"},{"key":"13_CR16","volume-title":"Automatic Treatment of Sequential Circuits in Second-Order Monadic Logic","author":"T. Margaria","year":"1996","unstructured":"T. Margaria, M. Mendler: \u201cAutomatic Treatment of Sequential Circuits in Second-Order Monadic Logic\u201d, 4th GI\/ITG\/GME Worksh. on Methoden des Entwurfs und der Verifikation digitaler Systeme, Kreischa (D), March 1996, Shaker Verlag."},{"key":"13_CR17","unstructured":"T. Margaria, M. Mendler: \u201cModel-based Automatic Synthesis and Analysis in Second-Order Monadic Logic,\u201d Proc. AAS'97, ACM\/SIGPLAN Int. Worksh. on Automated Analysis of Software, Paris (F), Jan. 1997, pp.99\u2013112."},{"key":"13_CR18","series-title":"LNCS","first-page":"258","volume-title":"Proc. TACAS'96","author":"T. Margaria","year":"1996","unstructured":"T. Margaria: \u201cFully Automatic Verification and Error Detection for Paramet\u00e9rized Iterative Sequential Circuits\u201d, Proc. TACAS'96, Passau (D), March 1996, LNCS N.1055, Springer Verlag, pp. 258\u2013277."},{"key":"13_CR19","unstructured":"T. Margaria: \u201cVerification of Systolic Arrays in M2L(Str),\u201d Techn. Rep. MIP-9613, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau, July 1996."},{"key":"13_CR20","unstructured":"O. Matz, A. Miller, A. Potthoff, W. Thomas, E. Valkema: \u201cReport on the Program AMoRE\u201d, Techn. Rep. Nr. 9507, Inst. f\u00fcr Informatik und Praktische Mathematik, Universit\u00e4t Kiel (D), 1995."},{"key":"13_CR21","unstructured":"J.K. Ousterhout: \u201cTcl and the Tk Toolkit,\u201d Addison-Wesley, April 1994."},{"issue":"N.6","key":"13_CR22","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"R. Paige, R. Tarjan: \u201cThree partition refinement algorithms,\u201d SIAM Journ. of Computation, Vol.16, N.6, Dec. 1987, pp.973\u2013989.","journal-title":"SIAM Journ. of Computation"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, R. E. Bryant: \u201cEfficient Implementation of a BDD Package,\u201d Proc. DAC'90, Orlando, FL, June 1990, pp. 40\u201345.","DOI":"10.1145\/123186.123222"},{"key":"13_CR24","unstructured":"B. Steffen, T. Margaria, A. Cla\u00dfen, V. Braun: \u201cIncremental Formalization: A Key to Industrial Success\u201d, In \u201cSOFTWARE: Concepts and Tools\u201d, Vol. 17, No 2, pp. 78\u201391, Springer Verlag, July 1996."},{"key":"13_CR25","series-title":"LNCS","first-page":"450","volume-title":"Proc. CAV'96","author":"B. Steffen","year":"1996","unstructured":"B. Steffen, T. Margaria, A. Cla\u00dfen, V. Braun: \u201cThe MetaFrame'95 Environment\u201d, (Experience Report for the Industry Day), Proc. CAV'96, Juli\u2013Aug. 1996, New Brunswick, NJ, USA, LNCS N.1102, Springer Verlag, pp.450\u2013453."},{"key":"13_CR26","unstructured":"B. Steffen, T. Margaria, A. Cla\u00dfen: \u201cHeterogeneous Analysis and Verification for Distributed Systems\u201d, In \u201cSOFTWARE: Concepts and Tools\u201d, vol. 17, N.1, pp. 13\u201325, Springer Verlag, 1996."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"W. Thomas: \u201cAutomata on infinite objects,\u201d In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, p. 133\u2013191. MIT Press\/Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"13_CR28","unstructured":"W. Thomas: \u201cLanguages, automata, and objects,\u201d to appear in the forthcoming new edition of the Handbook of Theoretical Computer Science, MIT Press\/Elsevier."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035388","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T11:56:22Z","timestamp":1736250982000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035388"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627906","9783540685197"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/bfb0035388","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}