{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:14:19Z","timestamp":1760080459990,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030628215"},{"type":"electronic","value":"9783030628222"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-62822-2_6","type":"book-chapter","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T21:04:28Z","timestamp":1604869468000},"page":"89-107","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata"],"prefix":"10.1007","author":[{"given":"Xie","family":"Li","sequence":"first","affiliation":[]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Mingji","family":"Xia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,11,9]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0055627","volume-title":"CONCUR\u201998 Concurrency Theory","author":"PA Abdulla","year":"1998","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K.: Simulation is decidable for one-counter nets. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 253\u2013268. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055627"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/11817963_9","volume-title":"Computer Aided Verification","author":"S Bardin","year":"2006","unstructured":"Bardin, S., Leroux, J., Point, G.: FAST extended release. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 63\u201366. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_9"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Blondin, M., Finkel, A., G\u00f6ller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6\u201310 July 2015, pp. 32\u201343. IEEE Computer Society (2015)","DOI":"10.1109\/LICS.2015.14"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-15375-4_13","volume-title":"CONCUR 2010 - Concurrency Theory","author":"S B\u00f6hm","year":"2010","unstructured":"B\u00f6hm, S., G\u00f6ller, S., Jan\u010dar, P.: Bisimilarity of one-counter processes is PSPACE-complete. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 177\u2013191. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_13"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"B\u00f6hm, S., G\u00f6ller, S., Jancar, P.: Equivalence of deterministic one-counter automata is NL-complete. In: Boneh, D., Roughgarden, T., Feigenbaum, J. (eds.) Symposium on Theory of Computing Conference, STOC 2013, Palo Alto, CA, USA, 1\u20134 June 2013, pp. 131\u2013140. ACM (2013)","DOI":"10.1145\/2488608.2488626"},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1090\/S0002-9939-1976-0396605-3","volume":"55","author":"I Borosh","year":"1976","unstructured":"Borosh, I., Treybig, L.B.: Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc. 55(2), 299\u2013304 (1976)","journal-title":"Proc. Am. Math. Soc."},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517\u2013531. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_47"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Chitic, C., Rosu, D.: On validation of XML streams using finite state machines. In: Amer-Yahia, S., Gravano, L. (eds.)Proceedings of the 7th International Workshop on the Web and Databases, WebDB 2004, 17\u201318 June 2004, Maison de la Chimie, Paris, France, Colocated with ACM SIGMOD\/PODS 2004, pp. 85\u201390. ACM (2004)","DOI":"10.1145\/1017074.1017096"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-48320-9_18","volume-title":"CONCUR\u201999 Concurrency Theory","author":"H Comon","year":"1999","unstructured":"Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 242\u2013257. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_18"},{"issue":"1\u20133","key":"6_CR10","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. Theor. Comput. Sci. 302(1\u20133), 93\u2013121 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. In: 14th International Symposium on Temporal Representation and Reasoning, TIME 2007, Alicante, Spain, 28\u201330 June 2007, pp. 94\u2013104. IEEE Computer Society (2007)","DOI":"10.1109\/TIME.2007.63"},{"key":"6_CR12","unstructured":"Dima, C.: Computing reachability relations in timed automata. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science, LICS 2002, Copenhagen, Denmark, 22\u201325 July 2002, p. 177. IEEE Computer Society (2002)"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.ic.2014.12.004","volume":"243","author":"J Fearnley","year":"2015","unstructured":"Fearnley, J., Jurdzinski, M.: Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput. 243, 26\u201336 (2015)","journal-title":"Inf. Comput."},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"105871","DOI":"10.1016\/j.ipl.2019.105871","volume":"153","author":"M Fr\u00e4nzle","year":"2020","unstructured":"Fr\u00e4nzle, M., Quaas, K., Shirmohammadi, M., Worrell, J.: Effective definability of the reachability relation in timedautomata. Inf. Process. Lett. 153, 105871 (2020)","journal-title":"Inf. Process. Lett."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-642-14162-1_48","volume-title":"Automata, Languages and Programming","author":"S G\u00f6ller","year":"2010","unstructured":"G\u00f6ller, S., Haase, C., Ouaknine, J., Worrell, J.: Model checking succinct and parametric one-counter automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 575\u2013586. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_48"},{"issue":"3","key":"6_CR16","doi-asserted-by":"publisher","first-page":"884","DOI":"10.1137\/120876435","volume":"42","author":"S G\u00f6ller","year":"2013","unstructured":"G\u00f6ller, S., Lohrey, M.: Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput. 42(3), 884\u2013923 (2013)","journal-title":"SIAM J. Comput."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"G\u00f6ller, S., Mayr, R., To, A.W.: On the computational complexity of verifying one-counter processes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, Los Angeles, CA, USA, 11\u201314 August 2009, pp. 235\u2013244. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.37"},{"key":"6_CR18","unstructured":"Haase, C.: On the complexity of model checking counter automata. Ph.D. thesis (2012)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Haase, C.: Subclasses of Presburger arithmetic and the weak EXP hierarchy. In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, New York, NY, USA. Association for Computing Machinery (2014)","DOI":"10.1145\/2603088.2603092"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-04081-8_25","volume-title":"CONCUR 2009 - Concurrency Theory","author":"C Haase","year":"2009","unstructured":"Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in succinct and parametric one-counter automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 369\u2013383. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_25"},{"issue":"3\u20134","key":"6_CR21","doi-asserted-by":"publisher","first-page":"317","DOI":"10.3233\/FI-2016-1316","volume":"143","author":"C Haase","year":"2016","unstructured":"Haase, C., Ouaknine, J., Worrell, J.: Relating reachability problems in timed and counter automata. Fundam. Inform. 143(3\u20134), 317\u2013338 (2016)","journal-title":"Fundam. Inform."},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"743","DOI":"10.1007\/978-3-642-22110-1_60","volume-title":"Computer Aided Verification","author":"M Hague","year":"2011","unstructured":"Hague, M., Lin, A.W.: Model checking recursive programs with numeric data types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 743\u2013759. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_60"},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"OH Ibarra","year":"1978","unstructured":"Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. ACM 25(1), 116\u2013133 (1978)","journal-title":"J. ACM"},{"issue":"1","key":"6_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0890-5401(03)00171-8","volume":"188","author":"P Jancar","year":"2004","unstructured":"Jancar, P., Kucera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inf. Comput. 188(1), 1\u201319 (2004)","journal-title":"Inf. Comput."},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-45022-X_28","volume-title":"Automata, Languages and Programming","author":"A Ku\u010dera","year":"2000","unstructured":"Ku\u010dera, A.: Efficient verification algorithms for one-counter processes. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 317\u2013328. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45022-X_28"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-32033-3_23","volume-title":"Term Rewriting and Applications","author":"P Lafourcade","year":"2005","unstructured":"Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 308\u2013322. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_23"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere!. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 489\u2013503. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562948_36"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: ICALP, pp. 1136\u20131149 (2004)","DOI":"10.1007\/978-3-540-27836-8_94"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-77966-7_8","volume-title":"Hardware and Software: Verification and Testing","author":"A Smr\u010dka","year":"2008","unstructured":"Smr\u010dka, A., Vojnar, T.: Verifying parametrised hardware designs via counter automata. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 51\u201368. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-77966-7_8"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-319-63046-5_31","volume-title":"Automated Deduction \u2013 CADE 26","author":"Z Xu","year":"2017","unstructured":"Xu, Z., Chen, T., Wu, Z.: Satisfiability of compositional separation logic with tree predicates and data constraints. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 509\u2013527. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_31"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-62822-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,11]],"date-time":"2023-10-11T20:33:14Z","timestamp":1697056394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-62822-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030628215","9783030628222"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-62822-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"9 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/lcs.ios.ac.cn\/setta2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}