{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:13:39Z","timestamp":1771701219776,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_20","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:56:36Z","timestamp":1427756196000},"page":"231-237","source":"Crossref","is-referenced-by-count":51,"title":["Symbolic Model-Checking Using ITS-Tools"],"prefix":"10.1007","author":[{"given":"Yann","family":"Thierry-Mieg","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Eclipse Modeling Framework, http:\/\/www.eclipse.org\/modeling\/emf\/"},{"key":"20_CR2","unstructured":"Model checking contest @ petri nets home page, http:\/\/mcc.lip6.fr\/"},{"key":"20_CR3","unstructured":"Spin model checker home page, http:\/\/spinroot.com\/"},{"key":"20_CR4","unstructured":"Uppaal home page, http:\/\/www.uppaal.org"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2013","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Len\u010do, M., Ro\u010dkai, P., \u0160till, V., Weiser, J.: DiVinE 3.0 \u2013 An Explicit-State Model Checker for Multithreaded C & C++ Programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"20_CR6","first-page":"24","volume":"VIII","author":"Y. Ben Ma\u00efssa","year":"2013","unstructured":"Ben Ma\u00efssa, Y., Kordon, F., Mouline, S., Thierry-Mieg, Y.: Modeling and Analyzing Wireless Sensor Networks with VeriSensor: an Integrated Workflow. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)\u00a0VIII, 24\u201347 (2013)","journal-title":"Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-54862-8_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.E. Ben Salem","year":"2014","unstructured":"Ben Salem, A.E., Duret-Lutz, A., Kordon, F., Thierry-Mieg, Y.: Symbolic model checking of stutter-invariant properties using generalized\u00a0testing\u00a0automata. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 440\u2013454. Springer, Heidelberg (2014)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45251-6_18","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"D. Beyer","year":"2001","unstructured":"Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 318. Springer, Heidelberg (2001)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 122\u2013125. Springer, Heidelberg (2003)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: lTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 354\u2013359. Springer, Heidelberg (2010)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., et al.: VIS: A System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-13675-7_10","volume-title":"Applications and Theory of Petri Nets","author":"C. Choppy","year":"2010","unstructured":"Choppy, C., Dedova, A., Evangelista, S., Hong, S., Klai, K., Petrucci, L.: The NEO protocol for large-scale distributed database systems: Modelling and initial verification. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol.\u00a06128, pp. 145\u2013164. Springer, Heidelberg (2010)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"830","DOI":"10.1007\/978-3-642-39799-8_58","volume-title":"Computer Aided Verification","author":"M. Colange","year":"2013","unstructured":"Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Towards distributed software model-checking using decision diagrams. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 830\u2013845. Springer, Heidelberg (2013)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Colange, M., Kordon, F., Thierry-Mieg, Y., Baarir, S.: State Space Analysis using Symmetries on Decision Diagrams. In: Application of Concurrency to System Design (ACSD), pp. 164\u2013172. IEEE Computer Society (2012)","DOI":"10.1109\/ACSD.2012.28"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Couvreur, J.M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.A.: Data decision diagrams for Petri net analysis. In: Application and Theory of Petri Nets (ICATPN), pp. 129\u2013158 (2002)","DOI":"10.1007\/3-540-48068-4_8"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Couvreur, J.M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Formal Techniques for Networked and Distributed Systems (FORTE), pp. 443\u2013457 (2005)","DOI":"10.1007\/11562436_32"},{"issue":"1\/2","key":"20_CR17","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1504\/IJCCBS.2014.059594","volume":"5","author":"A. Duret-Lutz","year":"2014","unstructured":"Duret-Lutz, A.: LTL translation improvements in Spot 1.0. International Journal on Critical Computer-Based Systems\u00a05(1\/2), 31\u201354 (2014)","journal-title":"International Journal on Critical Computer-Based Systems"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-642-24372-1_24","volume-title":"Automated Technology for Verification and Analysis","author":"A. Duret-Lutz","year":"2011","unstructured":"Duret-Lutz, A., Klai, K., Poitrenaud, D., Thierry-Mieg, Y.: Self-loop aggregation product \u2014 A new hybrid approach to on-the-fly LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 336\u2013350. Springer, Heidelberg (2011)"},{"issue":"3","key":"20_CR19","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.L.: Modalities for model checking: Branching time logic strikes back. Science of Computer Programming\u00a08(3), 275\u2013306 (1987)","journal-title":"Science of Computer Programming"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-68746-7_16","volume-title":"Applications and Theory of Petri Nets","author":"A. Hamez","year":"2008","unstructured":"Hamez, A., Thierry-Mieg, Y., Kordon, F.: Hierarchical Set Decision Diagrams and Automatic Saturation. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol.\u00a05062, pp. 211\u2013230. Springer, Heidelberg (2008)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 545\u2013558. Springer, Heidelberg (1992)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Iwashita, H., Nakata, T., Hirose, F.: Ctl model checking based on forward state traversal. In: Computer-Aided Design (ICCAD). pp. 82\u201387. IEEE\/ACM (1996)","DOI":"10.1109\/ICCAD.1996.569084"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-68746-7_20","volume-title":"Applications and Theory of Petri Nets","author":"K. Klai","year":"2008","unstructured":"Klai, K., Poitrenaud, D.: MC-SOG: An LTL model checker based on symbolic observation graphs. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol.\u00a05062, pp. 288\u2013306. Springer, Heidelberg (2008)"},{"key":"20_CR24","unstructured":"Spot, L.R.D.E.: a library for LTL model-checking, http:\/\/spot.lip6.fr\/"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Pinchinat, S., Acher, M., Vojtisek, D.: Towards synthesis of attack trees for supporting computer-aided risk analysis. In: Workshop on Formal Methods in the Development of Software (co-located with SEFM) (2014)","DOI":"10.1007\/978-3-319-15201-1_24"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/3-540-36126-X_6","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Somenzi","year":"2002","unstructured":"Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic SCC hull algorithms. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 88\u2013105. Springer, Heidelberg (2002)"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00768-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Thierry-Mieg","year":"2009","unstructured":"Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 1\u201315. Springer, Heidelberg (2009)"},{"key":"20_CR28","unstructured":"Voelter, M., Benz, S., Dietrich, C., Engelmann, B., Helander, M., Kats, L.C.L., Visser, E., Wachsmuth, G.: DSL Engineering - Designing, Implementing and Using Domain-Specific Languages. dslbook.org (2013)"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, Y., B\u00e9rard, B., Kordon, F., Thierry-Mieg, Y.: Automated Controllability and Synthesis with Hierarchical Set Decision Diagrams. In: Workshop on Discrete Event Systems (WODES). pp. 291\u2013296. IFAC\/Elsevier, Berlin, Germany (September 2010)","DOI":"10.3182\/20100830-3-DE-4013.00047"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:25:07Z","timestamp":1747855507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}