{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:25:27Z","timestamp":1750843527043,"version":"3.41.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319657646"},{"type":"electronic","value":"9783319657653"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-65765-3_8","type":"book-chapter","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T09:08:38Z","timestamp":1501664918000},"page":"133-150","source":"Crossref","is-referenced-by-count":6,"title":["Time-Triggered Conversion of Guards for Reachability Analysis of Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[]},{"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[]},{"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,3]]},"reference":[{"key":"8_CR1","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proceeding of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Hybrid Systems: Computation and Control, HSCC 2012, Beijing, China, 17\u201319 April 2012, pp. 45\u201354 (2012)","DOI":"10.1145\/2185632.2185643"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Althoff, M., Le Guernic, C., Krogh, B.H.: Reachable set computation for uncertain time-varying linear systems. In: Hybrid Systems: Computation and Control, pp. 93\u2013102 (2011)","DOI":"10.1145\/1967701.1967717"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Althoff, M., Rajhans, A., Krogh, B.H., Yaldiz, S., Li, X., Pileggi, L.: Formal verification of phase-locked loops using reachability analysis and continuization. In: Proceeding of the International Conference on Computer Aided Design, pp. 659\u2013666 (2011)","DOI":"10.1109\/ICCAD.2011.6105400"},{"issue":"2","key":"8_CR5","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/j.nahs.2009.03.009","volume":"4","author":"M Althoff","year":"2010","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Anal. Hybrid Syst. 4(2), 233\u2013249 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"issue":"1","key":"8_CR6","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bak, S.: Reducing the wrapping effect in flowpipe construction using pseudo-invariants. In: 4th ACM SIGBED International Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems (CyPhy 2014), pp. 40\u201343 (2014)","DOI":"10.1145\/2593458.2593471"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 155\u2013164. ACM, New York (2016)","DOI":"10.1145\/2883817.2883837"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), pp. 128\u2013133. ACM (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"8_CR10","unstructured":"Bak, S., Duggirala, P.S.: Direct verification of linear systems with over 10000 dimensions. In: 4th International Workshop on Applied Verification for Continuous and Hybrid Systems (2017)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 173\u2013178. ACM (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Bak, S., Johnson, T.T.: Periodically-scheduled controller analysis using hybrid systems reachability and continuization. In: 36th IEEE Real-Time Systems Symposium (RTSS), San Antonio, Texas. IEEE Computer Society, December 2015","DOI":"10.1109\/RTSS.2015.26"},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1002\/rnc.2914","volume":"24","author":"L Benvenuti","year":"2014","unstructured":"Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume-guarantee verification of nonlinear hybrid systems with ARIADNE. Int. J. Robust Nonlinear Control 24, 699\u2013724 (2014)","journal-title":"Int. J. Robust Nonlinear Control"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-13338-6_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Bogomolov","year":"2014","unstructured":"Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116\u2013131. Springer, Cham (2014). doi: 10.1007\/978-3-319-13338-6_10"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-642-31424-7_35","volume-title":"Computer Aided Verification","author":"S Bogomolov","year":"2012","unstructured":"Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 479\u2013494. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_35"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Mitrohin, C., Podelski, A.: Composing reachability analyses of hybrid systems for safety and stability. In: Proceeding of the 8th International Symposium on Automated Technology for Verification and Analysis, pp. 67\u201381 (2010)","DOI":"10.1007\/978-3-642-15643-4_7"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-46430-1_10","volume-title":"Hybrid Systems: Computation and Control","author":"O Botchkarev","year":"2000","unstructured":"Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73\u201388. Springer, Heidelberg (2000). doi: 10.1007\/3-540-46430-1_10"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-02444-8_6","volume-title":"Automated Technology for Verification and Analysis","author":"T Brihaye","year":"2013","unstructured":"Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: complexity and fixed points. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 55\u201370. Springer, Cham (2013). doi: 10.1007\/978-3-319-02444-8_6"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: Bach 2: bounded reachability checker for compositional linear hybrid systems. In: Proceeding of Design, Automation & Test in Europe, pp. 1512\u20131517 (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"8_CR20","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. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_18"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S., \u00c1brah\u00e1m, E.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceeding of the 33rd IEEE Real-Time Systems Symposium (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-319-17524-9_29","volume-title":"NASA Formal Methods","author":"X Chen","year":"2015","unstructured":"Chen, X., Schupp, S., Makhlouf, I.B., \u00c1brah\u00e1m, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 408\u2013414. Springer, Cham (2015). doi: 10.1007\/978-3-319-17524-9_29"},{"key":"8_CR23","unstructured":"Dang, T.: V\u00e9rification et synth\u00e8se des syst\u00e8mes hybrides. PhD thesis, Institut National Polytechnique de Grenoble (2000)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-71493-4_16","volume-title":"Hybrid Systems: Computation and Control","author":"A Donz\u00e9","year":"2007","unstructured":"Donz\u00e9, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174\u2013189. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71493-4_16"},{"issue":"3","key":"8_CR25","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Methods Syst. Des. 30(3), 179\u2013198 (2007)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31954-2_17"},{"key":"8_CR27","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., 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. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_30"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-78929-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2008","unstructured":"Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187\u2013200. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78929-1_14"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 203\u2013212. ACM (2013)","DOI":"10.1145\/2461328.2461361"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Frehse, G., Ray, R.: Flowpipe-guard intersection for reachability computations with support functions. In: Proceeding of Analysis and Design of Hybrid Systems, pp. 94\u2013101 (2012)","DOI":"10.3182\/20120606-3-NL-3011.00053"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Proceeding of the 27th International Conference on Computer Aided Verification, pp. 212\u2013226 (2010)","DOI":"10.1007\/978-3-642-14295-6_22"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Girard, A., Le Guernic, C.: Efficient reachability analysis for linear systems using support functions. In: Proceeding of the 17th IFAC World Congress, pp. 8966\u20138971 (2008)","DOI":"10.3182\/20080706-5-KR-1001.01514"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-78929-1_16","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2008","unstructured":"Girard, A., Guernic, C.: Zonotope\/Hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215\u2013228. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78929-1_16"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: the next generation. In: Proceeding. of the 16th IEEE Real-Time Systems Symposium, pp. 56\u201365 (1995)","DOI":"10.1109\/REAL.1995.495196"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Immler, F.: A verified algorithm for geometric zonotope\/hyperplane intersection. In: Proceeding of the Conference on Certified Programs and Proofs, pp. 129\u2013136 (2015)","DOI":"10.1145\/2676724.2693164"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$ -reachability analysis for hybrid systems. In: Proceeding of Tools and Algorithms for the Construction and Analysis of Systems, pp. 200\u2013205 (2015)","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"8_CR37","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/10984413_12","volume-title":"New Directions and Applications in Control Theory","author":"A Kurzhanski","year":"2005","unstructured":"Kurzhanski, A., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Dayawansa, W.P., Lindquist, A., Zhou, Y. (eds.) New Directions and Applications in Control Theory, vol. 321, pp. 193\u2013205. Springer, Heidelberg (2005). doi: 10.1007\/10984413_12"},{"key":"8_CR38","unstructured":"Lagerberg, A.: A benchmark on hybrid control of an automotive powertrain with backlash. Technical report R005\/2007, Signals and Systems, Chalmers University of Technology (2007)"},{"issue":"2","key":"8_CR39","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C Guernic Le","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250\u2013262 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"8_CR40","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/s11786-014-0204-y","volume":"8","author":"M Ma\u00efga","year":"2014","unstructured":"Ma\u00efga, M., Ramdani, N., Trav\u00e9-Massuy\u00e8s, L., Combastel, C.: A CSP versus a zonotope-based method for solving guard set intersection in nonlinear hybrid reachability. Math. Comput. Sci. 8, 407\u2013423 (2014)","journal-title":"Math. Comput. Sci."},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1007\/978-3-540-78929-1_51","volume-title":"Hybrid Systems: Computation and Control","author":"IM Mitchell","year":"2008","unstructured":"Mitchell, I.M., Susuki, Y.: Level set methods for computing reachable sets of hybrid systems with differential algebraic equation dynamics. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 630\u2013633. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78929-1_51"},{"key":"8_CR42","doi-asserted-by":"crossref","first-page":"1633","DOI":"10.1016\/S0005-1098(02)00047-X","volume":"38","author":"M Nordin","year":"2002","unstructured":"Nordin, M., Gutman, P.-O.: Controlling mechanical systems with backlash - a survey. Automatica 38, 1633\u20131649 (2002)","journal-title":"Automatica"},{"key":"8_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14509-4"},{"issue":"2","key":"8_CR44","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.nahs.2010.05.010","volume":"5","author":"N Ramdani","year":"2010","unstructured":"Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5(2), 149\u2013162 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Schupp, S., \u00c1brah\u00e1m, E., Chen, X., Ben Makhlouf, I., Frehse, G., Sankaranarayanan, S., Kowalewski, S.: Current challenges in the verification of hybrid systems. In: Proceeding of the Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, pp. 8\u201324 (2015)","DOI":"10.1007\/978-3-319-25141-7_2"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Smirnov, G.V.: Introduction to the Theory of Differential Inclusions. American Mathematical Society (2002)","DOI":"10.1090\/gsm\/041"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-65765-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T19:57:54Z","timestamp":1750795074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-65765-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319657646","9783319657653"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-65765-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}