{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T16:01:34Z","timestamp":1756310494174,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319165769"},{"type":"electronic","value":"9783319165776"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-16577-6_3","type":"book-chapter","created":{"date-parts":[[2015,3,29]],"date-time":"2015-03-29T02:05:04Z","timestamp":1427594704000},"page":"55-78","source":"Crossref","is-referenced-by-count":10,"title":["A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Johanna","family":"Nellen","sequence":"first","affiliation":[]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[]},{"given":"Benedikt","family":"Wolters","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-36577-X_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Counter-example guided predicate abstraction of hybrid systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 208\u2013223. Springer, Heidelberg (2003)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E. Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 365\u2013770. Springer, Heidelberg (2002)"},{"key":"3_CR4","unstructured":"Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.L.: Ariadne: A framework for reachability analysis of hybrid automata. In: Proc. of MTNS 2006 (2006)"},{"key":"3_CR5","unstructured":"Baresi, L., Carmeli, S., Monti, A., Pezz\u00e8, M.: PLC programming languages: A formal approach. In: Proc. of Automation 1998. ANIPLA (1998)"},{"key":"3_CR6","unstructured":"Bauer, N.: Formale Analyse von Sequential Function Charts. Ph.D. thesis, Universit\u00e4t Dortmund (2004)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-540-27863-4_22","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"N. Bauer","year":"2004","unstructured":"Bauer, N., Huuck, R., Lukoschus, B., Engell, S.: A unifying semantics for sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 400\u2013418. Springer, Heidelberg (2004)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-39176-7_8","volume-title":"Model Checking Software","author":"S. Bogomolov","year":"2013","unstructured":"Bogomolov, S., Donz\u00e9, A., Frehse, G., Grosu, R., Johnson, T.T., Ladan, H., Podelski, A., Wehrle, M.: Abstraction-based guided search for hybrid systems. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol.\u00a07976, pp. 117\u2013134. Springer, Heidelberg (2013)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X. Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"issue":"04","key":"3_CR10","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Fehnker, A., Han, Z., Krogh, B.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. Journal of Foundations of Computer Science\u00a014(04), 583\u2013604 (2003)","journal-title":"Int. Journal of Foundations of Computer Science"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 192\u2013207. Springer, Heidelberg (2003)"},{"key":"3_CR12","doi-asserted-by":"crossref","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.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_15"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H. Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 114\u2013129. Springer, Heidelberg (2007)"},{"issue":"2","key":"3_CR14","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1142\/S021819400500204X","volume":"15","author":"S. Engell","year":"2005","unstructured":"Engell, S., Lohmann, S., Stursberg, O.: Verification of embedded supervisory controllers considering hybrid plant dynamics. Int. Journal of Software Engineering and Knowledge Engineering\u00a015(2), 307\u2013312 (2005)","journal-title":"Int. Journal of Software Engineering and Knowledge Engineering"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-540-31954-2_16","volume-title":"Hybrid Systems: Computation and Control","author":"A. Fehnker","year":"2005","unstructured":"Fehnker, A., Clarke, E., Jha, S., Krogh, B.: Refining abstractions of hybrid systems using counterexample fragments. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 242\u2013257. Springer, Heidelberg (2005)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G. Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. Int. Journal on Software Tools for Technology Transfer\u00a010, 263\u2013279 (2008)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Frey, G., Litz, L.: Formal methods in PLC programming. In: Proc. of SMC 2000, vol.\u00a04, pp. 2431\u20132436. IEEEXplore (2000)","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. TAC 2007\u00a052(5), 782\u2013798 (2007)","DOI":"10.1109\/TAC.2007.895849"},{"key":"3_CR20","unstructured":"Hassapis, G., Kotini, I., Doulgeri, Z.: Validation of a SFC software specification by using hybrid automata. In: Proc. of INCOM 1998, pp. 65\u201370. Pergamon (1998)"},{"issue":"1-2","key":"3_CR21","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P., Wong-Toi, H.: Hytech: A model checker for hybrid systems. Int. Journal on Software Tools for Technology Transfer\u00a01(1-2), 110\u2013122 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"3_CR22","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? Journal of Computer and System Sciences\u00a057(1), 94\u2013124 (1998)","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Herceg, M., Kvasnica, M., Jones, C.N., Morari, M.: Multi-Parametric Toolbox 3.0. In: Proc. of the ECC 2013, Z\u00fcrich, Switzerland, pp. 502\u2013510 (2013)","DOI":"10.23919\/ECC.2013.6669862"},{"key":"3_CR24","unstructured":"Int. Electrotechnical Commission: Programmable Controllers, Part 3: Programming Languages, 61131\u201361133 (2003)"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-71493-4_24","volume-title":"Hybrid Systems: Computation and Control","author":"S.K. Jha","year":"2007","unstructured":"Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 287\u2013300. Springer, Heidelberg (2007)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Kurzhanskiy, A., Varaiya, P.: Ellipsoidal toolbox. Tech. rep., EECS, UC Berkeley (2006)","DOI":"10.1109\/CDC.2006.377036"},{"key":"3_CR27","unstructured":"Lukoschus, B.: Compositional Verification of Industrial Control Systems - Methods and Case Studies. Ph.D. thesis, Christian-Albrechts-Universit\u00e4t zu Kiel (2005)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-10512-3_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Minopoli","year":"2014","unstructured":"Minopoli, S., Frehse, G.: Non-convex invariants and urgency conditions on linear hybrid automata. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol.\u00a08711, pp. 176\u2013190. Springer, Heidelberg (2014)"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-46430-1_27","volume-title":"Hybrid Systems: Computation and Control","author":"I. Mitchell","year":"2000","unstructured":"Mitchell, I., Tomlin, C.: Level set methods for computation in hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 310\u2013323. Springer, Heidelberg (2000)"},{"key":"3_CR30","unstructured":"Nellen, J., \u00c1brah\u00e1m, E.: Hybrid sequential function charts. In: Proc. of MBMV 2012, pp. 109\u2013120. Verlag Dr. Kovac (2012)"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Nellen, J., \u00c1brah\u00e1m, E.: A CEGAR approach for the reachability analysis of PLC-controlled chemical plants. In: Proc. of FMi 2014 (2014)","DOI":"10.1109\/IRI.2014.7051930"},{"key":"3_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-35873-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Prabhakar","year":"2013","unstructured":"Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 48\u201367. Springer, Heidelberg (2013)"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-73368-3_46","volume-title":"Computer Aided Verification","author":"M. Segelken","year":"2007","unstructured":"Segelken, M.: Abstraction and counterexample-guided construction of \u03c9-automata for model checking of step-discrete linear hybrid models. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 433\u2013448. Springer, Heidelberg (2007)"}],"container-title":["Advances in Intelligent Systems and Computing","Formalisms for Reuse and Systems Integration"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-16577-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T18:18:52Z","timestamp":1747851532000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-16577-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319165769","9783319165776"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-16577-6_3","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2015]]}}}