{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:31:20Z","timestamp":1725492680528},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404316"},{"type":"electronic","value":"9783540450054"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45005-x_29","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T04:27:47Z","timestamp":1192768067000},"page":"326-338","source":"Crossref","is-referenced-by-count":2,"title":["Safety Verification for Two-Way Finite Automata with Monotonic Counters"],"prefix":"10.1007","author":[{"given":"Oscar H.","family":"Ibarra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhe","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhi-Wei","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013235, April 1994.","journal-title":"Theoretical Computer Science"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, pages 592\u2013601, San Diego, California, 16-18 May 1993.","DOI":"10.1145\/167088.167242"},{"key":"29_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Hybrid Systems II","author":"A. Bouajjani","year":"1995","unstructured":"A. Bouajjani, R. Echahed, and R. Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, volume 999 of Lecture Notes in Computer Science. Springer-Verlag, 1995."},{"key":"29_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Concurrency (CONCUR 1997)","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: application to model-checking. In Concurrency (CONCUR 1997), volume 1243 of Lecture Notes in Computer Science, pages 135\u2013150. Springer-Verlag, 1997."},{"key":"29_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop of Logic of Programs, volume 131 of Lecture Notes in Computer Science. Springer, 1981."},{"issue":"2","key":"29_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finit estate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR7","unstructured":"Z. Dang. Phd. dissertation. Department of Computer Science, University of California at Santa Barbara, 2000."},{"key":"29_CR8","unstructured":"Z. Dang, O. Ibarra, and Z. Sun. On the emptiness problems for two-way nondeterministic finite automata with one reversal-bounded counter. Submitted, 2002."},{"key":"29_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/10722167_9","volume-title":"Binary reachability analysis of discrete pushdown timed automata","author":"Z. Dang","year":"2000","unstructured":"Zhe Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. In Proceedings of the International Conference on Computer Aided Verification (CAV\u201900), volume 1855 of Lecture Notes in Computer Science, pages 69\u201384. Springer, 2000."},{"key":"29_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/3-540-44679-6_59","volume-title":"Decidable Approximations on Generalized and Parameterized Discrete Timed Automata","author":"Z. Dang","year":"2001","unstructured":"Zhe Dang, O. H. Ibarra, and R. A. Kemmerer. Decidable Approximations on Generalized and Parameterized Discrete Timed Automata. In Proceedings of the 7th Annual International Computing and Combinatorics Conference (COCOON\u201901), volume 2108 of Lecture Notes in Computer Science, pages 529\u2013539. Springer, 2001."},{"key":"29_CR11","unstructured":"Zhe Dang and R. A. Kemmerer. A symbolic model-checker for testing ASTRAL real-time specifications. In Proceedings of the Sixth International Conference on Real-time Computing Systems and Applications, pages 131\u2013142. IEEE Computer Society Press, 1999."},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Zhe Dang and R. A. Kemmerer. Using the ASTRAL Model Checker to Analyze Mobile IP. In Proceedings of the 1999 International Conference on Software Engineering (ICSE\u201999), pages 132\u2013141. IEEE Computer Society Press \/ ACM Press, 1999.","DOI":"10.1145\/302405.302459"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Zhe Dang and R. A. Kemmerer. Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems. In Proceedings of the 2000 International Conference on Software Engineering (ICSE\u201900), pages 345\u2013354. IEEE Computer Society Press, 2000.","DOI":"10.1145\/337180.337220"},{"key":"29_CR14","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"S. Ginsburg and E. Spanier. Semigroups, presburger formulas, and languages. Pacific J. of Mathematics, 16:285\u2013296, 1966.","journal-title":"Pacific J. of Mathematics"},{"key":"29_CR15","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/0022-0000(81)90028-3","volume":"22","author":"E. M. Gurari","year":"1981","unstructured":"E. M. Gurari and O. H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. Journal of Computer and System Sciences, 22:220\u2013229, 1981.","journal-title":"Journal of Computer and System Sciences"},{"issue":"5","key":"29_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997. Special Issue: Formal Methods in Software Practice.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"29_CR17","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. H. Ibarra","year":"1978","unstructured":"O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25(1):116\u2013133, January 1978.","journal-title":"Journal of the ACM"},{"key":"29_CR18","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1137\/S0097539792240625","volume":"24","author":"O. H. Ibarra","year":"1995","unstructured":"O. H. Ibarra, T. Jiang, N. Tran, and H. Wang. New decidability results concerning two-way counter machines. SIAM J. Comput., 24:123\u2013137, 1995.","journal-title":"SIAM J. Comput."},{"key":"29_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-44612-5_38","volume-title":"Counter machines: decidable properties and applications to verification problems","author":"O. H. Ibarra","year":"2000","unstructured":"O. H. Ibarra, J. Su, Zhe Dang, T. Bultan, and R. A. Kemmerer. Counter machines: decidable properties and applications to verification problems. In Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS 2000), volume 1893 of Lecture Notes in Computer Science, pages 426\u2013435. Springer-Verlag, 2000."},{"key":"29_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":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"29_CR21","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M. Minsky","year":"1961","unstructured":"M. Minsky. Recursive unsolvability of Post\u2019s problem of Tag and other topics in the theory of Turing machines. Ann. of Math., 74:437\u2013455, 1961.","journal-title":"Ann. of Math."},{"issue":"3","key":"29_CR22","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1983","unstructured":"A. P. Sistla and E. M. Clarke. Complexity of propositional temporal logics. Journal of ACM, 32(3):733\u2013749, 1983.","journal-title":"Journal of ACM"},{"key":"29_CR23","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, LICS\u201986, Cambridge, MA, USA, 16-18 June 1986, pages 332\u2013344, Washington, DC, 1986. IEEE Computer Society Press."}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45005-X_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T05:00:54Z","timestamp":1550984454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45005-X_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404316","9783540450054"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45005-x_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}