{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,3]],"date-time":"2025-10-03T17:50:58Z","timestamp":1759513858016,"version":"3.37.3"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,6,18]],"date-time":"2010-06-18T00:00:00Z","timestamp":1276819200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,8]]},"DOI":"10.1007\/s10009-010-0163-9","type":"journal-article","created":{"date-parts":[[2010,6,17]],"date-time":"2010-06-17T19:30:23Z","timestamp":1276803023000},"page":"307-317","source":"Crossref","is-referenced-by-count":12,"title":["Path-oriented bounded reachability analysis of composed linear hybrid systems"],"prefix":"10.1007","volume":"13","author":[{"given":"Lei","family":"Bu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,6,18]]},"reference":[{"key":"163_CR1","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"163_CR2","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S.: Integration graphs: a class of decidable hybrid systems. In: Hybrid System. LNCS, vol. 736, pp. 179\u2013208","DOI":"10.1007\/3-540-57318-6_29"},{"key":"163_CR3","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. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"163_CR4","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T. Henzinger","year":"1998","unstructured":"Henzinger T., Kopke P., Puri A., Varaiya P.: What\u2019s decidable about hybrid automata?. J. Comput. Syst. Sci. 57, 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"163_CR5","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Ho, P.-H., Wong-Toi, H.: HYTECH: a model checker for hybrid systems. In: Software Tools for Technology Transfer, vol. 1, pp. 110\u2013122 (1997)","DOI":"10.1007\/s100090050008"},{"key":"163_CR6","doi-asserted-by":"crossref","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceeding of Hybrid Systems: Computation and Control\u201905. LNCS, vol. 2289, pp. 258\u2013273 (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"163_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Advance in Computers, vol. 58. Academic Press, London (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"163_CR8","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satifiability solvers. In: Proceedings of CAV 2002. LNCS, vol. 2404, pp. 17\u201336. Springer, Berin (2002)","DOI":"10.1007\/3-540-45657-0_2"},{"key":"163_CR9","first-page":"209","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle M., Herde C., Ratschan S., Schubert T., Teige T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1, 209\u2013236 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"2","key":"163_CR10","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.entcs.2004.12.022","volume":"119","author":"G. Audemard","year":"2005","unstructured":"Audemard G., Bozzano M., Cimatti A., Sebastiani R.: Verifying industrial hybrid systems with MathSAT. Electron. Notes Theor. Comput. Sci. 119(2), 17\u201332 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"163_CR11","doi-asserted-by":"crossref","unstructured":"Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Conference on Formal Techniques for Networked and Distributed Systems. In: LNCS, vol. 2529, pp. 243\u2013259 (2002)","DOI":"10.1007\/3-540-36135-9_16"},{"key":"163_CR12","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Klaedtke, F., Steffen, M.: Optimizing bounded model checking for linear hybrid systems. In: Proceedings of VMCAI 2005. LNCS, vol. 3385, pp. 396\u2013412","DOI":"10.1007\/978-3-540-30579-8_26"},{"key":"163_CR13","doi-asserted-by":"crossref","unstructured":"Li, X., Jha, S., Bu, L.: Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming. In: ENTCS, vol. 174, issue 3, pp. 57\u201370 (2007)","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"163_CR14","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Li, X.: BACH: Bounded ReachAbility CHecker for linear hybrid automata. In: Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design, pp. 65\u201368. IEEE Computer Society Press, Portland, OR, USA (2008)","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"163_CR15","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: Proceedings of the 13th Design Automation and Test in Europe Conference, Dresden, Germany, pp. 1512\u20131517 (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"163_CR16","doi-asserted-by":"crossref","unstructured":"Alur, R.: Timed automata. In: Proceedings of the 11th International Conference on Computer-Aided Verification. In: LNCS, vol. 1633, pp. 8\u201322. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_3"},{"issue":"1","key":"163_CR17","doi-asserted-by":"crossref","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 Trans. Softw. Eng. 31(1), 38\u201351 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"163_CR18","unstructured":"OR-Objects of DRA Systems. http:\/\/OpsResearch.com\/OR-Objects\/index.html"},{"key":"163_CR19","doi-asserted-by":"crossref","unstructured":"Malinowski, J., Niebert, P.: SAT based bounded model checking with partial order semantics for timed automata. In: Proceedings of TACAS 2010, Paphos, Cyprus. LNCS, vol. 6015, pp. 405\u2013419 (2010)","DOI":"10.1007\/978-3-642-12002-2_34"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0163-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0163-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0163-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T01:55:59Z","timestamp":1740189359000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0163-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6,18]]},"references-count":19,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["163"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0163-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2010,6,18]]}}}