{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:13:40Z","timestamp":1771701220638,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757747","type":"print"},{"value":"9783031757754","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75775-4_15","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:26:39Z","timestamp":1731396399000},"page":"338-359","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking of\u00a0PLC Code Specifications: Impact of\u00a0GRAFCET Features to\u00a0State Space Size"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1007-5597","authenticated-orcid":false,"given":"Robin","family":"Mro\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7348-0146","authenticated-orcid":false,"given":"Marcus","family":"V\u00f6lker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9397-2009","authenticated-orcid":false,"given":"Stefan","family":"Kowalewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3507-2851","authenticated-orcid":false,"given":"Aron","family":"Schnakenbeck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1922-654X","authenticated-orcid":false,"given":"Alexander","family":"Fay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-25423-4_15","volume-title":"Formal Methods and Software Engineering","author":"B Beckert","year":"2015","unstructured":"Beckert, B., Ulbrich, M., Vogel-Heuser, B., Weigl, A.: Regression verification for programmable logic controller software. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 234\u2013251. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_15"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Biallas, S., Bohlender, D., Kowalewski, S.: Boolean and modular abstraction for programmable logic controllers. In: Dependable Control of Discrete Systems (DCDS), pp. 97\u2013102. IEEE (2013)","DOI":"10.3182\/20130904-3-UK-4041.00011"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-24690-6_6","volume-title":"Software Engineering and Formal Methods","author":"JO Blech","year":"2011","unstructured":"Blech, J.O., Ould Biha, S.: Verification of PLC properties based on formal semantics in coq. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 58\u201373. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_6"},{"key":"15_CR4","unstructured":"Bornot, S., Huuck, R., Lakhnech, Y., Lukoschus, B.: Verification of sequential function charts using SMV. In: International Conference on Parallel and Distributed Processing Techniques and Applications, Monte Carlo Resort, Las Vegas, Nevada, USA, 26\u201329 June 2000, vol. V, pp. 2987\u20132993. CSREA Press (2000). ISBN 1-892512-51-3"},{"key":"15_CR5","unstructured":"Bornot, S., Huuck, R., Lakhnech, Y., Lukoschus, B.: Utilizing static analysis for programmable logic controllers. In: 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM), Dortmund, Germany, 18\u201319 September 2000, Aachen, Germany, pp. 183\u2013187. Shaker Verlag (2000). ISSN 0945-4659. ISBN 3-8265-7836-8"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, vol. 8, no. 2, pp. 244\u2013263 (1986). https:\/\/doi.org\/10.1145\/5397.5399","DOI":"10.1145\/5397.5399"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, Paris, France, Dunod, pp. 106\u2013130 (1976)","DOI":"10.1145\/390019.808314"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-662-43613-4_18","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D Darvas","year":"2014","unstructured":"Darvas, D., Fern\u00e1ndez Adiego, B., V\u00f6r\u00f6s, A., Bartha, T., Blanco Vi\u00f1uela, E., Gonz\u00e1lez Su\u00e1rez, V.M.: Formal verification of complex properties on PLC programs. In: \u00c1brah\u00e1m, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 284\u2013299. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43613-4_18"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Gourcuff, V., De Smet, O., Faure, J.-M.: Efficient representation for formal verification of PLC programs. In: 8th International Workshop on Discrete Event Systems, Ann Arbor, MI, USA, pp. 182\u2013187 (2006). https:\/\/doi.org\/10.1109\/WODES.2006.1678428","DOI":"10.1109\/WODES.2006.1678428"},{"key":"15_CR10","unstructured":"GRAFCET Specification Language for Sequential Function Charts, Standard IEC 60848 (2013)"},{"key":"15_CR11","unstructured":"Programmable controllers - Part 3: Programming languages, Standard IEC 61131-3 (2013)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Julius, R., Trenner, T., Fay, A., Neidig, J., Hoang, X.L.: A meta-model based environment for GRAFCET specifications. In: Proceedings of IEEE International Systems Conference (SysCon), Piscataway, NJ, USA, pp. 1\u20137 (2019)","DOI":"10.1109\/SYSCON.2019.8836959"},{"issue":"4","key":"15_CR13","doi-asserted-by":"publisher","first-page":"5","DOI":"10.18255\/1818-1015-2013-4-5-22","volume":"20","author":"EV Kuzmin","year":"2013","unstructured":"Kuzmin, E.V., Sokolov, V.A., Ryabukhin, D.A.: Construction and Verification of PLC-programs by LTL-specification. Model. Anal. Inform. Sist. 20(4), 5\u201322 (2013)","journal-title":"Model. Anal. Inform. Sist."},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-319-03077-7_4","volume-title":"Hardware and Software: Verification and Testing","author":"T Lange","year":"2013","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 44\u201360. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_4"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Mertke, T., Frey, G.: Formal verification of PLC programs generated from signal interpreted Petri nets. In: 2001 IEEE International Conference on Systems, Man and Cybernetics, Tucson, AZ, USA, vol. 4, pp. 2700\u20132705 (2001). https:\/\/doi.org\/10.1109\/ICSMC.2001.972974","DOI":"10.1109\/ICSMC.2001.972974"},{"key":"15_CR16","first-page":"67","volume":"38","author":"I Moon","year":"1992","unstructured":"Moon, I., Powers, G.J., Burch, J.R., Clarke, E.M.: Automatic verification of sequential control systems using temporal logic, in A.I.Ch.E. Journal 38, 67\u201375 (1992)","journal-title":"Journal"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Moon, I.: Modeling programmable logic controllers for logic verification. In: IEEE Control Systems Magazine, vol. 14, no. 2, pp. 53\u201359 (1994). https:\/\/doi.org\/10.1109\/37.272781","DOI":"10.1109\/37.272781"},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"125652","DOI":"10.1109\/ACCESS.2022.3225736","volume":"10","author":"R Mross","year":"2022","unstructured":"Mross, R., Schnakenbeck, A., V\u00f6lker, M., Fay, A., Kowalewski, S.: Transformation of GRAFCET into GAL for verification purposes based on a detailed meta-model. IEEE Access 10, 125652\u2013125665 (2022). https:\/\/doi.org\/10.1109\/ACCESS.2022.3225736","journal-title":"IEEE Access"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Mro\u00df, R., Schnakenbeck, A., V\u00f6lker, M., Fay, A., Kowalewski, S.: Unambiguous interpretation of IEC 60848 GRAFCET based on a literature review. In: 28th International Conference on Emerging Technologies and Factory Automation (ETFA) (2023)","DOI":"10.1109\/ETFA54631.2023.10275504"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Mro\u00df, R., Schnakenbeck, A., V\u00f6lker, M., Fay, A., Kowalewski, S.: GRAFCET reduction techniques for model checking. In: 21st International Conference on Industrial Informatics (INDIN) (2023)","DOI":"10.1109\/INDIN51400.2023.10218247"},{"key":"15_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"2010","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-662-03811-6. ISBN 3642084745"},{"key":"15_CR22","unstructured":"Pavlovic, O., Pinger, R., Kollmann, M.: Automation of formal verification of PLC programs written in IL. In: 4th International Verification Workshop (VERIFY), Bremen, Germany, CEUR Workshop Proceedings, vol. 259, pp. 152\u2013163 (2007)"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Pavlovic, O., Ehrich, H.-D.: Model checking PLC software written in function block diagram. In: 3rd International Conference on Software Testing, Verification and Validation, Paris, France, pp. 439\u2013448 (2010). https:\/\/doi.org\/10.1109\/ICST.2010.10","DOI":"10.1109\/ICST.2010.10"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Schlich, B., Brauer, J., Wernerus, J., Kowalewski, S.: Direct model checking of PLC programs in IL. In: Dependable Control of Discrete Systems (DCDS), IFAC Proceedings, vol. 42, no 5, pp. 28\u201333 (2009). https:\/\/doi.org\/10.3182\/20090610-3-IT-4004.00010","DOI":"10.3182\/20090610-3-IT-4004.00010"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Schnakenbeck, A., Mro\u00df, R., V\u00f6lker, M., Kowalewski, S., Fay, A.: Ans\u00e4tze f\u00fcr die Modellierung von Streckeninformationen zur Verifikation im Steuerungsentwurf. Tagung \u201cEntwurf komplexer Automatisierungssysteme\u201d (EKA), 14.-15.05.2024, Magdeburg, Germany (2024). https:\/\/doi.org\/10.25673\/116044","DOI":"10.25673\/116044"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Schnakenbeck, A., Mro\u00df, R., V\u00f6lker, M., Kowalewski, S., Fay, A.: A control flow based static analysis of grafcet using abstract interpretation. In: 21st International Conference on Industrial Informatics (INDIN) (2023)","DOI":"10.1109\/INDIN51400.2023.10218176"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Schnakenbeck, A., Mro\u00df, R., V\u00f6lker, M., Kowalewski, S., Fay, A.: Structural analysis of GRAFCET control specifications. In: 28th International Conference on Emerging Technologies and Factory Automation (ETFA) (2023)","DOI":"10.1109\/ETFA54631.2023.10275713"},{"key":"15_CR28","unstructured":"Thierry-Mieg, Y.: From Symbolic Verification To Domain Specific Languages. Habilitation \u00e0 diriger desrecherches, Sorbonne Universit\u00e9, UPMC; Laboratoired\u2019informatique de Paris 6 [LIP6] (2016)"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Treseler, H., Bauer, N., Kowalewski, S.: Verification of IL programs with an explicit model of their PLC execution. In: Proceedings of 5th Workshop on Discrete Event Systems (WODES 2000), Ghent, Belgium, 21\u201323 August 2000, pp. 283\u2013289. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4615-4493-7_29"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. SE-10(4), 352\u2013357 (1984). https:\/\/doi.org\/10.1109\/TSE.1984.5010248","DOI":"10.1109\/TSE.1984.5010248"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Zaytoon, J.: A contribution to the validation of grafcet controlled systems. Eur. J. Control 6(6), 488\u2013506 (2000). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0947358000711113","DOI":"10.1016\/S0947-3580(00)71111-3"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75775-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:03:35Z","timestamp":1731398615000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75775-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757747","9783031757754"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75775-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}