{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:17:18Z","timestamp":1749010638285,"version":"3.41.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319390857"},{"type":"electronic","value":"9783319390864"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-39086-4_9","type":"book-chapter","created":{"date-parts":[[2016,6,8]],"date-time":"2016-06-08T09:09:16Z","timestamp":1465376956000},"page":"123-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research"],"prefix":"10.1007","author":[{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D\u00e1niel","family":"Darvas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Attila","family":"Klenik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c1kos","family":"Hajdu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Attila","family":"J\u00e1mbor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tam\u00e1s","family":"Bartha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,9]]},"reference":[{"key":"9_CR1","unstructured":"Bartha, T., V\u00f6r\u00f6s, A., J\u00e1mbor, A., Darvas, D.: Verification of an industrial safety function using coloured Petri nets and model checking. In: Proceedings of the 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Enterprises, pp. 472\u2013485. Hungarian Academy of Sciences (2012)"},{"key":"9_CR2","unstructured":"Cayir, S., Ucer, M.: An algorithm to compute a basis of Petri net invariants. In: 4th ELECO International Conference on Electrical and Electronics Engineering. UCTEA, Bursa, Turkey (2005)"},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf. 8(1), 4\u201325 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11560548_13","volume-title":"Correct Hardware Design and Verification Methods","author":"G Ciardo","year":"2005","unstructured":"Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 146\u2013161. Springer, Heidelberg (2005)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-29072-5_3","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"G Ciardo","year":"2012","unstructured":"Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a Petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 51\u201395. Springer, Heidelberg (2012)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"9_CR7","unstructured":"Cseh, A., Tarnai, G., S\u00e1ghi, B.: Petri net modelling of signalling systems [in Hungarian, original title: Biztos\u00edt\u00f3berendez\u00e9sek modellez\u00e9se Petri-h\u00e1l\u00f3kkal]. Vezet\u00e9kek Vil\u00e1ga XIX(1), 14\u201317 (2014)"},{"key":"9_CR8","unstructured":"Darvas, D., Fern\u00e1ndez Adiego, B., Blanco Vi\u00f1uela, E.: Transforming PLC programs into formal models for verification purposes. Internal Note CERN-ACC-NOTE-2013-0040, CERN (2013)"},{"key":"9_CR9","unstructured":"Darvas, D., V\u00f6r\u00f6s, A.: Saturation-based test input generation using coloured Petri nets [in Hungarian, original title: Szatur\u00e1ci\u00f3alap\u00fa tesztbemenet-gener\u00e1l\u00e1s sz\u00ednezett Petri-h\u00e1l\u00f3kkal]. In: Mesterpr\u00f3ba 2013, pp. 48\u201351 (2013)"},{"key":"9_CR10","unstructured":"Darvas, D., V\u00f6r\u00f6s, A., Bartha, T.: Improving saturation-based bounded model checking. Acta Cybernetica (2014, accepted, in press). http:\/\/petridotnet.inf.mit.bme.hu\/publications\/AC2014_DarvasEtAl.pdf"},{"key":"9_CR11","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. 6996, pp. 336\u2013350. Springer, Heidelberg (2011)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-19488-2_16","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"\u00c1 Hajdu","year":"2015","unstructured":"Hajdu, \u00c1., V\u00f6r\u00f6s, A., Bartha, T.: New search strategies for the Petri net CEGAR approach. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 309\u2013328. Springer, Heidelberg (2015)"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"401","DOI":"10.14232\/actacyb.21.3.2014.8","volume":"21","author":"\u00c1 Hajdu","year":"2014","unstructured":"Hajdu, \u00c1., V\u00f6r\u00f6s, A., Bartha, T., M\u00e1rtonka, Z.: Extensions to the CEGAR approach on Petri nets. Acta Cybernetica 21(3), 401\u2013417 (2014)","journal-title":"Acta Cybernetica"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-38697-8_21","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"M Heiner","year":"2013","unstructured":"Heiner, M., Rohr, C., Schwarick, M.: MARCIE \u2013 model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389\u2013399. Springer, Heidelberg (2013)"},{"key":"9_CR15","unstructured":"ISO\/IEC 15909-2 Systems, software engineering - High-level Petri nets - Part 2: Transfer format (2011)"},{"key":"9_CR16","unstructured":"Klenik, A., Marussy, K.: Configurable stochastic analysis framework for asynchronous systems. Scientific students\u2019 associations report, Budapest University of Technology and Economics (2015). http:\/\/petridotnet.inf.mit.bme.hu\/publications\/TDK2015_KlenikMarussy.pdf"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-68353-4_47","volume-title":"Application and Theory of Petri Nets, Informatik-Fachberichte","author":"J Mart\u00ednez","year":"1982","unstructured":"Mart\u00ednez, J., Silva, M.: A simple and fast algorithm to obtain all invariants of a generalised Petri net. In: Girault, C., Reisig, W. (eds.) Application and Theory of Petri Nets, Informatik-Fachberichte, vol. 52, pp. 301\u2013310. Springer, Heidelberg (1982)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Mil\u00e1nkovich, A., Ill, G., Lendvai, K., Imre, S., Szab\u00f3, S.: Evaluation of energy efficiency of aggregation in WSNs using Petri nets. In: Proceedings of the 3rd International Conference on Sensor Networks, pp. 289\u2013297. Science and Technology Publications (2014)","DOI":"10.5220\/0004668402890297"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-662-46681-0_58","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Moln\u00e1r","year":"2015","unstructured":"Moln\u00e1r, V., Darvas, D., V\u00f6r\u00f6s, A., Bartha, T.: Saturation-based incremental LTL model checking with inductive proofs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 643\u2013657. Springer, Heidelberg (2015)"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Moln\u00e1r, V., V\u00f6r\u00f6s, A., Darvas, D., Bartha, T., Majzik, I.: Component-wise incremental LTL model checking. Formal Aspects of Computing (2016, in press). doi:10.1007\/s00165-015-0347-x","DOI":"10.1007\/s00165-015-0347-x"},{"issue":"4","key":"9_CR21","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"9_CR22","unstructured":"Szilv\u00e1si, B.: Development of an education tool for the Formal methods course [in Hungarian, original title: Oktat\u00e1si seg\u00e9deszk\u00f6z fejleszt\u00e9se Form\u00e1lis m\u00f3dszerek t\u00e1rgyhoz]. Master\u2019s thesis, Budapest University of Technology and Economics (2008)"},{"issue":"8","key":"9_CR23","first-page":"1209","volume":"9","author":"WJ Thong","year":"2014","unstructured":"Thong, W.J., Ameedeen, M.A.: A survey of Petri net tools. ARPN J. Eng. Appl. Sci. 9(8), 1209\u20131214 (2014)","journal-title":"ARPN J. Eng. Appl. Sci."},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3176\/proc.2013.1.07","volume":"62","author":"A V\u00f6r\u00f6s","year":"2013","unstructured":"V\u00f6r\u00f6s, A., Darvas, D., Bartha, T.: Bounded saturation-based CTL model checking. Proc. Est. Acad. Sci. 62(1), 59\u201370 (2013)","journal-title":"Proc. Est. Acad. Sci."},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.3311\/PPee.2080","volume":"58","author":"A V\u00f6r\u00f6s","year":"2014","unstructured":"V\u00f6r\u00f6s, A., Darvas, D., J\u00e1mbor, A., Bartha, T.: Advanced saturation-based model checking of well-formed coloured Petri nets. Periodica Polytechnica, Electr. Eng. Comput. Sci. 58(1), 3\u201313 (2014)","journal-title":"Periodica Polytechnica, Electr. Eng. Comput. Sci."},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-19835-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Wimmel","year":"2011","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 224\u2013238. Springer, Heidelberg (2011)"},{"issue":"2","key":"9_CR27","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10009-009-0099-0","volume":"11","author":"AJ Yu","year":"2009","unstructured":"Yu, A.J., Ciardo, G., L\u00fcttgen, G.: Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Int. J. Softw. Tools Technol. Transf. 11(2), 117\u2013131 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-04761-9_27","volume-title":"Automated Technology for Verification and Analysis","author":"Y Zhao","year":"2009","unstructured":"Zhao, Y., Ciardo, G.: Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 368\u2013381. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-39086-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:00:56Z","timestamp":1748984456000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-39086-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319390857","9783319390864"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-39086-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 June 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PETRI NETS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applications and Theory of Petri Nets and Concurrency","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Torun","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 June 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"apn2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}