{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:20:14Z","timestamp":1725852014210},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496299"},{"type":"electronic","value":"9783662496305"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_27","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T05:04:32Z","timestamp":1458536672000},"page":"462-478","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Shortest Paths in One-Counter Systems"],"prefix":"10.1007","author":[{"given":"Dmitry","family":"Chistikov","sequence":"first","affiliation":[]},{"given":"Wojciech","family":"Czerwi\u0144ski","sequence":"additional","affiliation":[]},{"given":"Piotr","family":"Hofman","sequence":"additional","affiliation":[]},{"given":"Micha\u0142","family":"Pilipczuk","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Wehar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., \u010cern\u00fd, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 599\u2013610 (2011)","DOI":"10.1145\/1926385.1926454"},{"key":"27_CR2","unstructured":"Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: On bounded reachability analysis of shared memory systems. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, 15\u201317 December 2014, New Delhi, India, pp. 611\u2013623 (2014)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-40885-4_9","volume-title":"Frontiers of Combining Systems","author":"C Barrett","year":"2013","unstructured":"Barrett, C., Demri, S., Deters, M.: Witness runs for counter machines. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 120\u2013150. Springer, Heidelberg (2013)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR \u201997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"27_CR5","unstructured":"Chistikov, D.: Notes on counting with finite machines. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, 15\u201317 December 2014, New Delhi, India, pp. 339\u2013350 (2014)"},{"key":"27_CR6","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms 2nd (edn.) The MIT Press and McGraw-Hill Book Company. ISBN 0-262-03293-7 (2001)"},{"issue":"6","key":"27_CR7","doi-asserted-by":"publisher","first-page":"1541","DOI":"10.1093\/logcom\/exp037","volume":"19","author":"S Demri","year":"2009","unstructured":"Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. J. Log. Comput. 19(6), 1541\u20131575 (2009)","journal-title":"J. Log. Comput."},{"issue":"9","key":"27_CR8","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1016\/j.peva.2009.12.009","volume":"67","author":"K Etessami","year":"2010","unstructured":"Etessami, K., Wojtczak, D., Yannakakis, M.: Quasi-birth-death processes, tree-like QBDs, probabilistic 1-counter automata, and pushdown systems. Perform. Eval. 67(9), 837\u2013857 (2010)","journal-title":"Perform. Eval."},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Hofman, P., Mayr, R., Totzke, P.: Decidability of weak simulation on one-counter nets. In: 28th Annual ACM\/IEEE Symposium on Logic in Computer Science. LICS 2013, New Orleans, LA, USA, 25\u201328 June 2013, pp. 203\u2013212 (2013)","DOI":"10.1109\/LICS.2013.26"},{"key":"27_CR10","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4400-4","volume-title":"Design and Analysis of Algorithms","author":"DC Kozen","year":"1992","unstructured":"Kozen, D.C.: Design and Analysis of Algorithms. Texts and Monographs in Computer Science. Springer, New York (1992). ISBN: 978-3-540-97687-5"},{"key":"27_CR11","unstructured":"Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. Research report LSV-04-16, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France, p. 69, November 2004. \n                      http:\/\/www.lsv.ens-cachan.fr\/Publis\/RAPPORTS_LSV\/PS\/rr-lsv-2004-16.rr.ps"},{"key":"27_CR12","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)"},{"issue":"1","key":"27_CR13","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/0022-0000(83)90018-1","volume":"26","author":"M Latteux","year":"1983","unstructured":"Latteux, M.: Langages \u00e0 un compteur. J. Comput. Syst. Sci. 26(1), 14\u201333 (1983)","journal-title":"J. Comput. Syst. Sci."},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science. LICS 2015, 6\u201310 July 2015, Kyoto, Japan, pp. 56\u201367 (2015)","DOI":"10.1109\/LICS.2015.16"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-38592-6_15","volume-title":"Formal Techniques for Distributed Systems","author":"J Thakkar","year":"2013","unstructured":"Thakkar, J., Kanade, A., Alur, R.: Transducer-based algorithmic verification of retransmission protocols over noisy channels. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 209\u2013224. Springer, Heidelberg (2013)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-03351-3_2","volume-title":"Computer Science - Theory and Applications","author":"W Thomas","year":"2009","unstructured":"Thomas, W.: The reachability problem over infinite graphs. In: Frid, A., Morozov, A., Rybalchenko, A., Wagner, K.W. (eds.) CSR 2009. LNCS, vol. 5675, pp. 12\u201318. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49630-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T21:08:15Z","timestamp":1584997695000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}