{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T13:52:31Z","timestamp":1710251551859},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Efficient symbolic and explicit-state model checking approaches have been developed for the verification of linear time temporal logic (LTL) properties. Several attempts have been made to combine the advantages of the various algorithms. Model checking LTL properties usually poses two challenges: one must compute the synchronous product of the state space and the automaton model of the desired property, then look for counterexamples that is reduced to finding strongly connected components (SCCs) in the state space of the product. In case of concurrent systems, where the phenomenon of state space explosion often prevents the successful verification, the so-called saturation algorithm has proved its efficiency in state space exploration. This paper proposes a new approach that leverages the saturation algorithm both as an iteration strategy constructing the product directly, as well as in a new fixed-point computation algorithm to find strongly connected components on-the-fly by incrementally processing the components of the model. Complementing the search for SCCs, explicit techniques and component-wise abstractions are used to prove the absence of counterexamples. The resulting on-the-fly, incremental LTL model checking algorithm proved to scale well with the size of models, as the evaluation on models of the Model Checking Contest suggests.<\/jats:p>","DOI":"10.1007\/s00165-015-0347-x","type":"journal-article","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T11:52:33Z","timestamp":1451908353000},"page":"345-379","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Component-wise incremental LTL model checking"],"prefix":"10.1145","volume":"28","author":[{"given":"Vince","family":"Moln\u00e1r","sequence":"first","affiliation":[{"name":"Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tud\u00f3sok k\u00f6r\u00fatja 2., 1117, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[{"name":"Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tud\u00f3sok k\u00f6r\u00fatja 2., 1117, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D\u00e1niel","family":"Darvas","sequence":"additional","affiliation":[{"name":"Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tud\u00f3sok k\u00f6r\u00fatja 2., 1117, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tam\u00e1s","family":"Bartha","sequence":"additional","affiliation":[{"name":"Institute for Computer Science and Control, Hungarian Academy of Sciences, Kende utca 13\u201317., 1111, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[{"name":"Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tud\u00f3sok k\u00f6r\u00fatja 2., 1117, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"163","volume-title":"Correct system design, Lecture notes in computer science, vol 1710.","author":"Biere A","year":"1999"},{"key":"e_1_2_1_2_2_2","first-page":"193","volume-title":"Tools and algorithms for the construction and analysis of systems, Lecture notes in computer science, vol 1579.","author":"Biere A","year":"1999"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_2_4_2","unstructured":"Bradley AR Somenzi F Hassan Z Zhang Y (2011) An incremental approach to model checking progress properties. In: Bjesse P Slobodov\u00e1 A (eds) Proceedings of the international conference on formal methods in computer-aided design. FMCAD Inc pp 144\u2013153"},{"key":"e_1_2_1_2_5_2","first-page":"1","volume-title":"Proceedings of the 1960 international congress on logic, methodology and philosophy of science.","author":"B\u00fcchi JR","year":"1962"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cavada R Cimatti A Dorigatti M Mariotti A Micheli A Mover S Griggio A Roveri M Tonetta S (2014) The nuXmv symbolic model checker. Technical report Fondazione Bruno Kessler","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_2_1_2_8_2","first-page":"359","volume-title":"Computer aided verification, Lecture notes in computer science, vol 2404.","author":"Cimatti A","year":"2002"},{"key":"e_1_2_1_2_9_2","first-page":"328","volume-title":"Tools and algorithms for the construction and analysis of systems, vol 2031 of Lecture notes in computer science.","author":"Ciardo G","year":"2001"},{"key":"e_1_2_1_2_10_2","first-page":"379","volume-title":"Tools and algorithms for the construction and analysis of systems, Lecture notes in computer science, vol 2619.","author":"Ciardo G","year":"2003"},{"key":"e_1_2_1_2_11_2","first-page":"83","volume-title":"Petri nets and other models of concurrency \u2013 ICATPN 2007, Lecture Notes in Computer Science, vol 4546.","author":"Ciardo G","year":"2007"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/3220917.3221217"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008615614281"},{"key":"e_1_2_1_2_14_2","volume-title":"Model checking","author":"Clarke EM","year":"1999"},{"key":"e_1_2_1_2_15_2","first-page":"419","volume-title":"Computer aided verification, Lecture notes in computer science, vol 1102.","author":"Clarke EM","year":"1996"},{"key":"e_1_2_1_2_16_2","first-page":"154","volume-title":"Computer aided verification, Lecture notes in computer science, vol 1855.","author":"Clarke E","year":"2000"},{"key":"e_1_2_1_2_17_2","first-page":"233","volume-title":"Computer-aided verification, Lecture notes in computer science, vol 531.","author":"Courcoubetis CA","year":"1991"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A Poitrenaud D (2004) SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In: Proceedings of the IEEE international symposium on modeling analysis and simulation of computer and telecommunications systems pp 76\u201383","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"e_1_2_1_2_19_2","unstructured":"Duret-Lutz A Klai K Poitrenaud D Thierry-Mieg Y (2011) Combining explicit and symbolic approaches for better on-the-fly LTL model checking. CoRR abs\/1106.5700. http:\/\/arxiv.org\/abs\/1106.5700"},{"key":"e_1_2_1_2_20_2","first-page":"336","volume-title":"Automated technology for verification and analysis, Lecture notes in computer science, vol 6996.","author":"Duret-Lutz A","year":"2011"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, languages and programming, Lecture notes in computer science, vol 85.","author":"Emerson EA","year":"1980"},{"key":"e_1_2_1_2_22_2","first-page":"53","volume-title":"Computer aided verification, Lecture notes in computer science, vol 2102.","author":"Gastin P","year":"2001"},{"key":"e_1_2_1_2_23_2","first-page":"3","volume-title":"Proceedings of the international symposium on protocol specification, testing and verification.","author":"Gerth R","year":"1995"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_2_1_2_25_2","first-page":"196","volume-title":"Automated technology for verification and analysis, Lecture notes in computer science, vol 3299.","author":"Haddad S","year":"2004"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA Jhala R Majumdar R Sutre G (2002) Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM New York pp 58\u201370","DOI":"10.1145\/565816.503279"},{"key":"e_1_2_1_2_27_2","unstructured":"Hillah LM Kindler E Kordon F Petrucci L Treves N et\u00a0al (2009) A primer on the Petri Net Markup Language and ISO\/IEC 15909-2. Petri Net Newsl 76:9\u201328"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Holzmann GJ Peled D Yannakakis M (1997) On nested depth first search. In: Holzmann GJ Gr\u00e9goire J-C Peled D-A (eds) The spin verification system DIMACS series in discretemathematics and theoretical computer science vol 32. AMS pp 81\u201389","DOI":"10.1090\/dimacs\/032\/03"},{"key":"e_1_2_1_2_29_2","first-page":"288","volume-title":"Applications and theory of Petri nets, Lecture notes in computer science, vol 5062.","author":"Klai K","year":"2008"},{"key":"e_1_2_1_2_30_2","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke SA","year":"1963","journal-title":"Acta Philos Fenn"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_2_32_2","unstructured":"McMillan KL (1992) Symbolic model checking: an approach to the state explosion problem. PhD thesis Carnegie Mellon University UMI Order No. GAX92-24209"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr Somenzi F (eds) Lecture notes in computer science vol 2725 pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_2_34_2","unstructured":"Miller DM Drechsler R (1998) Implementing a multiple-valued decision diagram package. In: Proceedings of the 28th IEEE international symposium on multiple-valued logic pp 52\u201357"},{"key":"e_1_2_1_2_35_2","first-page":"643","volume-title":"Tools and algorithms for the construction and analysis of systems, Lecture notes in computer science, vol 9035.","author":"Moln\u00e1r V","year":"2015"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_2_37_2","first-page":"17","volume-title":"Computer aided verification, Lecture notes in computer science, vol 1427.","author":"Peled D","year":"1998"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annual symposium on foundations of computer science. IEEE Computer Society pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_39_2","first-page":"350","volume-title":"Computer aided verification, Lecture notes in computer science, vol 3576.","author":"Sebastiani R","year":"2005"},{"key":"e_1_2_1_2_40_2","first-page":"108","volume-title":"Formal methods in computer-aided design, Lecture notes in computer science, vol 1954.","author":"Sheeran M","year":"2000"},{"key":"e_1_2_1_2_41_2","first-page":"90","volume-title":"Tools and algorithms for the construction and analysis of systems, Lecture notes in computer science, vol 3920.","author":"Siminiceanu RI","year":"2006"},{"key":"e_1_2_1_2_42_2","first-page":"88","volume-title":"Formal methods in computer-aided design, Lecture notes in computer science, vol 2517.","author":"Somenzi v","year":"2002"},{"key":"e_1_2_1_2_43_2","unstructured":"Szpyrka M Biernacka A Jerzy B (2014) Methods of translation of Petri nets to NuSMV language. In: Popova-Zeugmann L (ed) Concurrency specification and programming CEUR workshop proceedings vol 1269 pp 245\u2013256"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_2_45_2","first-page":"276","volume-title":"Formal techniques for networked and distributed systems \u2013 FORTE 2004, Lecture notes in computer science, vol 3235.","author":"Thierry-Mieg Y","year":"2004"},{"key":"e_1_2_1_2_46_2","first-page":"238","volume-title":"Logics for concurrency, Lecture notes in computer science, vol 1043.","author":"Vardi MY","year":"1996"},{"key":"e_1_2_1_2_47_2","unstructured":"Vardi MY Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of the symposium on logic in computer science. IEEE Computer Society pp 332\u2013344"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-4617-3"},{"key":"e_1_2_1_2_49_2","first-page":"368","volume-title":"Automated technology for verification and analysis, Lecture notes in computer science, vol 5799.","author":"Zhao Y","year":"2009"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0146-3"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0347-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0347-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0347-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:12:07Z","timestamp":1641485527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0347-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["10.1007\/s00165-015-0347-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0347-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5]]}}}