{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:54:07Z","timestamp":1740099247468,"version":"3.37.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030050627"},{"type":"electronic","value":"9783030050634"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-05063-4_5","type":"book-chapter","created":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T19:23:45Z","timestamp":1544124225000},"page":"47-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verifying CTL with Unfoldings of Petri Nets"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2948-4822","authenticated-orcid":false,"given":"Lanlan","family":"Dong","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7523-4827","authenticated-orcid":false,"given":"Guanjun","family":"Liu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3757-9779","authenticated-orcid":false,"given":"Dongming","family":"Xiang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,12,7]]},"reference":[{"issue":"99","key":"5_CR1","first-page":"1","volume":"PP","author":"YY Dai","year":"2017","unstructured":"Dai, Y.Y., Brayton, R.K.: Verification and synthesis of clock-gated circuits. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. PP(99), 1 (2017)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"6","key":"5_CR2","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1109\/TCAD.2015.2481869","volume":"35","author":"A Griggio","year":"2016","unstructured":"Griggio, A., Roveri, M.: Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 35(6), 1026\u20131039 (2016)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Gnesi S, Margaria T.: Practical applications of probabilistic model checking to communication protocols, pp. 133\u2013150. Wiley-IEEE Press (2013)","DOI":"10.1002\/9781118459898.ch7"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Wang, H., Zhao, T., Ren, F., et al.: Integrated modular avionics system safety analysis based on model checking. In: Reliability and Maintainability Symposium, pp. 1\u20136. IEEE (2017)","DOI":"10.1109\/RAM.2017.7889773"},{"issue":"6","key":"5_CR5","first-page":"81","volume":"4","author":"MS Hegde","year":"2012","unstructured":"Hegde, M.S., Jnanamurthy, H.K., Singh, S.: Modelling and verification of extensible authentication protocol using spin model checker. Int. J. Netw. Secur. Its Appl. 4(6), 81\u201398 (2012)","journal-title":"Int. J. Netw. Secur. Its Appl."},{"key":"5_CR6","unstructured":"Petri, C.A.: Kommunikation mit Automaten. Ph.D. Thesis, Institut Fuer Instrumentelle Mathematik (1962)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"EM Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Hiraishi, H., et al.: Verification of the Futurebus+ cache coherence protocol. Form. Methods Syst. Des. 6, 217\u2013232 (1995)","journal-title":"Form. Methods Syst. Des."},{"issue":"8","key":"5_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E., Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"5_CR9","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., et al.: Symbolic model checking: 10 20, states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"5_CR10","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. Computer Science Department, pp. 49\u201358 (1991)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-662-55862-1_7","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XII","author":"A Valmari","year":"2017","unstructured":"Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Koutny, M., Kleijn, J., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XII. LNCS, vol. 10470, pp. 140\u2013165. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-55862-1_7"},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1047659.1040315","volume":"40","author":"C Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40(1), 110\u2013121 (2005)","journal-title":"ACM SIGPLAN Not."},{"issue":"2","key":"5_CR13","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/s11241-017-9297-0","volume":"54","author":"H Boucheneb","year":"2018","unstructured":"Boucheneb, H., Barkaoui, K.: Delay-dependent partial order reduction technique for real time systems. Real-Time Syst. 54(2), 278\u2013306 (2018)","journal-title":"Real-Time Syst."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-41202-8_13","volume-title":"Formal Methods and Software Engineering","author":"Y Si","year":"2013","unstructured":"Si, Y., Sun, J., Liu, Y., Wang, T.: Improving model checking stateful timed CSP with non-zenoness through clock-symmetry reduction. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 182\u2013198. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41202-8_13"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245\u2013259. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/978-3-540-69611-7_16"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-11164-3_28","volume-title":"Runtime Verification","author":"A Nouri","year":"2014","unstructured":"Nouri, A., Raman, B., Bozga, M., Legay, A., Bensalem, S.: Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 340\u2013355. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_28"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"4104","DOI":"10.1109\/ACCESS.2016.2597061","volume":"4","author":"Guanjun Liu","year":"2016","unstructured":"Liu, G., Reisig, W., Jiang, C., et al.: A branching-process-based method to check soundness of workflow systems. IEEE Access 4, 4104\u20134118 (2016)","journal-title":"IEEE Access"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-49583-5_7","volume-title":"Algorithms and Architectures for Parallel Processing","author":"Guanjun Liu","year":"2016","unstructured":"Liu, G., Zhang, K., Jiang, C.: Deciding the deadlock and livelock in a petri net with a target marking based on its basic unfolding. In: Carretero, J., Garcia-Blas, J., Ko, R.K.L., Mueller, P., Nakano, K. (eds.) ICA3PP 2016. LNCS, vol. 10048, pp. 98\u2013105. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49583-5_7"},{"issue":"6","key":"5_CR19","doi-asserted-by":"publisher","first-page":"2995","DOI":"10.1109\/TII.2017.2698640","volume":"13","author":"Dongming Xiang","year":"2017","unstructured":"Xiang, D., Liu, G., Yan, C., et al.: Detecting data inconsistency based on the unfolding technique of petri nets. IEEE Trans. Ind. Inform. 13, 2995\u20133005 (2017)","journal-title":"IEEE Transactions on Industrial Informatics"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-45139-0_4","volume-title":"Model Checking Software","author":"J Esparza","year":"2001","unstructured":"Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37\u201356. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45139-0_4"},{"key":"5_CR21","unstructured":"Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"3","key":"5_CR22","first-page":"285","volume":"1099","author":"J Esparza","year":"2002","unstructured":"Esparza, J., Vogler, W.: An improvement of McMillan\u2019s unfolding algorithm. LNCS 1099(3), 285\u2013310 (2002)","journal-title":"LNCS"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Himmel, A.S., Molter, H., Niedermeier, R., et al.: Adapting the BronCKerbosch algorithm for enumerating maximal cliques in temporal graphs. Soc. Netw. Anal. Min. 7(1), 35 (2017)","DOI":"10.1007\/s13278-017-0455-0"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/11767589_22","volume-title":"Petri Nets and Other Models of Concurrency - ICATPN 2006","author":"O Bonnet-Torr\u00e9s","year":"2006","unstructured":"Bonnet-Torr\u00e9s, O., Domenech, P., Lesire, C., Tessier, C.: Exhost-PIPE: PIPE extended for two classes of monitoring petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 391\u2013400. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11767589_22"},{"key":"5_CR25","unstructured":"Roch, S., Starke, P.H.: INA: Integrated Net Analyzer (2002). https:\/\/www2.informatik.hu-berlin.de\/~starke\/ina.html"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Architectures for Parallel Processing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-05063-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T18:17:20Z","timestamp":1573064240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-05063-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030050627","9783030050634"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-05063-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ICA3PP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Algorithms and Architectures for Parallel Processing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 November 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ica3pp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/nsclab.org\/ica3pp2018\/authors.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"407","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"141","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"50","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"2.3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"7.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}