{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,16]],"date-time":"2025-02-16T14:10:11Z","timestamp":1739715011695,"version":"3.37.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_10","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"95-111","source":"Crossref","is-referenced-by-count":5,"title":["Complexity Bounds for the Verification of Real-Time Software"],"prefix":"10.1007","author":[{"given":"Rohit","family":"Chadha","sequence":"first","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]},{"given":"Pavithra","family":"Prabhakar","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1007\/11523468_88","volume-title":"Automata, Languages and Programming","author":"P.A. Abdulla","year":"2005","unstructured":"Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1089\u20131101. Springer, Heidelberg (2005)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-48340-3_12","volume-title":"Mathematical Foundations of Computer Science 1999","author":"L. Aceto","year":"1999","unstructured":"Aceto, L., Laroussinie, F.: Is your model checker on time? In: Kuty\u0142owski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol.\u00a01672, pp. 125\u2013136. Springer, Heidelberg (1999)"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly Pushdown Automata. In: ACM Symposium on Theory of Computation, pp. 202\u2013211 (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1145\/1007352.1007390","volume-title":"STOC","author":"R. Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC, pp. 202\u2013211. ACM, New York (2004)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Balc\u00e1zar, J.L., Lozano, A., Tor\u00e1n, J.: The complexity of algorithmic problems on succinct instances. Computer Science, 351\u2013377 (1992)","DOI":"10.1007\/978-1-4615-3422-8_30"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: International Conference on Hybrid Systems: Computation and Control, pp. 64\u201385 (1994)","DOI":"10.1007\/3-540-60472-3_4"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-56496-9_24","volume-title":"Computer Aided Verification","author":"K. Cerans","year":"1993","unstructured":"Cerans, K.: Decidability of bisimulation equivalence for parallel timer processes. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 302\u2013315. Springer, Heidelberg (1993)"},{"key":"10_CR9","unstructured":"Chadha, R., Legay, A., Prabhakar, P., Viswanathan, M.: Complexity bounds for the verification of real-time software. Technical report, University of Illinois at Urbana-Champaign (2009), http:\/\/hdl.handle.net\/2142\/14134"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-74407-8_10","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"R. Chadha","year":"2007","unstructured":"Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 136\u2013150. Springer, Heidelberg (2007)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","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)"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(02)00743-0","volume":"302","author":"Z. Dang","year":"2003","unstructured":"Dang, Z.: Pushdown timed automata: A binary reachability characterization and safety verification. Theoretical Computer Science\u00a0302, 93\u2013121 (2003)","journal-title":"Theoretical Computer Science"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Emmi, M., Majumdar, R.: Decision Problems for the Verification of Real-time Software. In: International Conference on Hybrid Systems: Computation and Control, pp. 200\u2013211 (2006)","DOI":"10.1007\/11730637_17"},{"key":"10_CR14","first-page":"183","volume":"56","author":"H. Galperin","year":"1983","unstructured":"Galperin, H., Wigderson, A.: Succinct representations of graphs. Information and Computation\u00a056, 183\u2013198 (1983)","journal-title":"Information and Computation"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-540-71389-0_16","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Hague","year":"2007","unstructured":"Hague, M., Ong, C.-H.L.: Symbolic backwards-reachability analysis for higher-order pushdown systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 213\u2013227. Springer, Heidelberg (2007)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Harel, D., Kupferman, O., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. In: International Conference on Concurrency Theory, pp. 258\u2013272 (1997)","DOI":"10.1007\/3-540-63141-0_18"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-44464-5_11","volume-title":"Advances in Computing Science - ASIAN 2000","author":"A. Kucera","year":"2000","unstructured":"Kucera, A.: On simulation-checking with sequential systems. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol.\u00a01961, pp. 133\u2013148. Springer, Heidelberg (2000)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-46432-8_13","volume-title":"Foundation of Software Science and Computation Structures","author":"F. Laroussinie","year":"2000","unstructured":"Laroussinie, F., Schnoebelen, P.: The State Explosion Problem from Trace to Bisimulation Equivalence. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol.\u00a01784, pp. 192\u2013207. Springer, Heidelberg (2000)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-44929-9_33","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"R. Mayr","year":"2000","unstructured":"Mayr, R.: On the complexity of bisimulation problems for pushdown automata. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 474\u2013488. Springer, Heidelberg (2000)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Luke Ong, C.-H.: On model checking trees generated by higher order recursion schemes. In: IEEE Symposium on Logic in Computer Science, pp. 81\u201390 (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: IEEE Symposium on Logic in Computer Science, pp. 54\u201363 (2004)","DOI":"10.1109\/LICS.2004.1319600"},{"key":"10_CR23","first-page":"181","volume":"71","author":"C. Papadimitriou","year":"1986","unstructured":"Papadimitriou, C., Yannakakis, M.: A note on succinct representation of graphs. Information and Computation\u00a071, 181\u2013185 (1986)","journal-title":"Information and Computation"},{"issue":"2","key":"10_CR24","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1006\/inco.1997.2661","volume":"139","author":"A. Rabinovich","year":"1997","unstructured":"Rabinovich, A.: Complexity of equivalence problems for concurrent finite agents. Information and Computation\u00a0139(2), 111\u2013129 (1997)","journal-title":"Information and Computation"},{"issue":"2","key":"10_CR25","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1016\/S0304-3975(00)00033-5","volume":"243","author":"A. Rabinovich","year":"2000","unstructured":"Rabinovich, A.: Symbolic model checking for \u03bc-calculus requires exponential time. Theoretical Computer Science\u00a0243(2), 467\u2013475 (2000)","journal-title":"Theoretical Computer Science"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45627-9_29","volume-title":"SOFSEM 2001: Theory and Practice of Informatics","author":"Z. Sawa","year":"2001","unstructured":"Sawa, Z., Jancar, P.: P-Hardness of Equivalence Testing on Finite-State Processes. In: Pacholski, L., Ru\u017ei\u010dka, P. (eds.) SOFSEM 2001. LNCS, vol.\u00a02234, pp. 326\u2013335. Springer, Heidelberg (2001)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Srba, J.: Visibly pushdown automata: From language equivalence to simulation and bisimulation. In: International Workshop on Computer Science Logic, pp. 89\u2013103 (2006)","DOI":"10.1007\/11874683_6"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Veith, H.: Succinct representation, leaf languages, and projection reductions. In: IEEE Conference on Computational Complexity, pp. 118\u2013126 (1996)","DOI":"10.1109\/CCC.1996.507675"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11319-2_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,16]],"date-time":"2025-02-16T13:43:27Z","timestamp":1739713407000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}