{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:26Z","timestamp":1725494306304},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755951"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75596-8_30","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T14:03:37Z","timestamp":1194098617000},"page":"425-440","source":"Crossref","is-referenced-by-count":16,"title":["Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Disch","sequence":"additional","affiliation":[]},{"given":"Hardi","family":"Hungar","sequence":"additional","affiliation":[]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Pigorsch","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]},{"given":"Boris","family":"Wirtz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"7th Workshop on Hybrid Systems: Computation and Control","author":"M. Agrawal","year":"2004","unstructured":"Agrawal, M., Thiagarajan, P.S.: Lazy rectangular hybrid automata. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-540-31954-2_4","volume-title":"8th Workshop on Hybrid Systems: Computation and Control","author":"M. Agrawal","year":"2005","unstructured":"Agrawal, M., Thiagarajan, P.S.: The discrete time behavior of lazy linear hybrid automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 55\u201369. Springer, Heidelberg (2005)"},{"issue":"1","key":"30_CR3","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(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"7","key":"30_CR4","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E. Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of non-linear systems. Acta Informatica\u00a043(7), 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"14th Conference on Computer Aided Verification","author":"E. Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of the hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 365\u2013370. Springer, Heidelberg (2002)"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/11817963_40","volume-title":"18th Conference on Computer Aided Verification","author":"B. Boigelot","year":"2006","unstructured":"Boigelot, B., Herbreteau, F.: The power of hybrid acceleration. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 438\u2013451. Springer, Heidelberg (2006)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/11901914_22","volume-title":"4th Symposium on Automated Technology for Verification and Analysis","author":"W. Damm","year":"2006","unstructured":"Damm, W., Disch, S., Hungar, H., Pang, J., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Automatic verification of hybrid systems with large discrete state space. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 276\u2013291. Springer, Heidelberg (2006)"},{"issue":"1","key":"30_CR8","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1142\/S0129054107004577","volume":"18","author":"W. Damm","year":"2007","unstructured":"Damm, W., Pinto, G., Ratschan, S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. Journal of Foundations of Computer Science\u00a018(1), 63\u201386 (2007)","journal-title":"Journal of Foundations of Computer Science"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Dolzmann, A.: Algorithmic Strategies for Applicable Real Qunantifier Elimination. PhD thesis, Universit\u00e4t Passau (2000)","DOI":"10.1007\/978-3-642-59932-3_11"},{"issue":"3","key":"30_CR10","doi-asserted-by":"publisher","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 in System Design\u00a030(3), 179\u2013198 (2007)","journal-title":"Formal Methods in System Design"},{"key":"30_CR11","unstructured":"Frehse, G.: Compositional Verification of Hybrid Systems using Simulation Relations. PhD thesis, Radboud Universiteit Nijmegen (2005)"},{"issue":"5","key":"30_CR12","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/TAC.2007.895849","volume":"52","author":"A. Girard","year":"2007","unstructured":"Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Transactions on Automatic Control\u00a052(5), 782\u2013798 (2007)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"30_CR13","unstructured":"H3 FOMC Team. The flap controller description, http:\/\/www.avacs.org\/Benchmarks\/flapcontroller.pdf"},{"key":"30_CR14","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1109\/LICS.1996.561342","volume-title":"11th IEEE Symposium on Logic in Computer Science","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: 11th IEEE Symposium on Logic in Computer Science, pp. 278\u2013292. IEEE Press, Los Alamitos (1996)"},{"issue":"1\u20132","key":"30_CR15","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.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer\u00a01(1\u20132), 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"30_CR16","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communication of the ACM\u00a012, 576\u2013583 (1969)","journal-title":"Communication of the ACM"},{"key":"30_CR17","unstructured":"Jha, S., Brady, B., Seshia, S.: Symbolic reachability analysis of lazy linear hybrid automata. Technical report, EECS Dept. UC Berkeley (2007)"},{"issue":"12","key":"30_CR18","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"5","key":"30_CR19","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. The Computer Journal\u00a036(5), 450\u2013462 (1993)","journal-title":"The Computer Journal"},{"key":"30_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"30_CR21","unstructured":"Mishchenko, A., Chatterjee, S., Jiang, R., Brayton, R.K.: FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS Dept. UC Berkeley (2005)"},{"key":"30_CR22","first-page":"459","volume-title":"18th IEEE Conference on Computer Design","author":"V. Paruthi","year":"2000","unstructured":"Paruthi, V., Kuehlmann, A.: Equivalence checking combining a structural SAT-solver, BDDs, and simulation. In: 18th IEEE Conference on Computer Design, pp. 459\u2013464. IEEE Press, Los Alamitos (2000)"},{"key":"30_CR23","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1109\/FMCAD.2006.4","volume-title":"6th Conference on Formal Methods in Computer Aided Design","author":"F. Pigorsch","year":"2006","unstructured":"Pigorsch, F., Scholl, C., Disch, S.: Advanced unbounded model checking by using AIGs, BDD sweeping and quantifier scheduling. In: 6th Conference on Formal Methods in Computer Aided Design, pp. 89\u201396. IEEE Press, Los Alamitos (2006)"},{"key":"30_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/978-3-540-71493-4_37","volume-title":"HSCC 2007","author":"A. Platzer","year":"2007","unstructured":"Platzer, A., Clarke, E.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. 10th Workshop on Hybrid Systems: Computation and Control. LNCS, vol.\u00a04416, pp. 473\u2013486. Springer, Heidelberg (2007)"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/978-3-540-73368-3_46","volume-title":"CAV 2007","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)"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using CheckMate. In: 4th Conference on Automation of Mixed Processes (2000)","DOI":"10.1109\/ACC.2000.879487"},{"key":"30_CR27","unstructured":"The VIS Group. VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"issue":"1","key":"30_CR28","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/TSE.2005.13","volume":"31","author":"F. Wang","year":"2005","unstructured":"Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. IEEE Transactions on Software Engineering\u00a031(1), 38\u201352 (2005)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:25:26Z","timestamp":1619519126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755951"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_30","relation":{},"subject":[]}}