{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:07:56Z","timestamp":1746194876947},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,3,1]],"date-time":"2011-03-01T00:00:00Z","timestamp":1298937600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Tiwari proved that the termination of a class of linear programs is decidable in Tiwari (Proceedings of CAV\u201904. Lecture notes in computer science, vol 3114, pp 70\u201382, 2004). The decision procedure proposed therein depends on the computation of\n            <jats:italic>Jordan forms<\/jats:italic>\n            . Thus, people may draw a wrong conclusion from this procedure, if they simply apply floating-point computation to compute Jordan forms. In this paper, we first use an example to explain this problem, and then present a symbolic implementation of the decision procedure. Thus, the rounding error problem is therefore avoided. Moreover, we also show that the symbolic decision procedure is as efficient as the numerical one given in Tiwari (Proceedings of CAV\u201904. Lecture notes in computer science, vol 3114, pp 70\u201382, 2004). The complexity of former is max{\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>6<\/jats:sup>\n            ),\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>m<\/jats:italic>\n              +3\n            <\/jats:sup>\n            )}, while that of the latter is\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>m<\/jats:italic>\n              +3\n            <\/jats:sup>\n            ), where\n            <jats:italic>n<\/jats:italic>\n            is the number of variables of the program and\n            <jats:italic>m<\/jats:italic>\n            is the number of its Boolean conditions. In addition, for the case when the characteristic polynomial of the assignment matrix is irreducible, we design a more efficient symbolic algorithm whose complexity is max(\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>6<\/jats:sup>\n            ),\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>mn<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            )).\n          <\/jats:p>","DOI":"10.1007\/s00165-009-0144-5","type":"journal-article","created":{"date-parts":[[2009,12,16]],"date-time":"2009-12-16T16:11:32Z","timestamp":1260979892000},"page":"171-190","source":"Crossref","is-referenced-by-count":13,"title":["Symbolic decision procedure for termination of linear programs"],"prefix":"10.1145","volume":"23","author":[{"given":"Bican","family":"Xia","sequence":"first","affiliation":[{"name":"LMAM, School of Mathematical Sciences, Peking University, Beijing, China"}]},{"given":"Lu","family":"Yang","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[{"name":"Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"given":"Zhihai","family":"Zhang","sequence":"additional","affiliation":[{"name":"LMAM, School of Mathematical Sciences, Peking University, Beijing, China"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Chen C Lemaire F Li L Moreno Maza M Pan W Xie Y (2008) The Constructible Set Tools and Parametric Systems Tools modules of the Regular Chains library in Maple. In: Proceedings of the international conference on computational science and applications pp 342\u2013352. IEEE Computer Society Press New York","DOI":"10.1109\/ICCSA.2008.61"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80152-6"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-7091-3406-1_7","volume-title":"Computer algebra: symbolic and algebraic computation","author":"Collins GE","year":"1982"},{"issue":"2","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/261320.261324","article-title":"REDLOG: computer algebra meets computer logic","volume":"31","author":"Dolzman A","year":"1997","journal-title":"ACM SIGSAM Bull"},{"key":"e_1_2_1_2_5_2","unstructured":"Hoffman E Kunze R (1971) Linear algebra 2nd edn. Prentice-Hall"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-7091-9459-1_13","volume-title":"Quantifier elimination and cylinderical algebraic decomposition","author":"Johnson JR","year":"1998"},{"key":"e_1_2_1_2_7_2","unstructured":"Lions JL (1996) The ARIANE 5 Flight 501 failure report 19 July 1996. European Space Agency (ESA)"},{"key":"e_1_2_1_2_8_2","volume-title":"Ordinary differential equations","author":"Miller RK","year":"1982"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Mine A (2005) Relational abstract domains for the detection of floating-point run-time eorrors. In: Proceedings of ESOP\u201905. Lecture notes in computer science vol 2986 pp 3\u201317","DOI":"10.1007\/978-3-540-24725-8_2"},{"issue":"4","key":"e_1_2_1_2_10_2","first-page":"11","article-title":"Roundoff error and the Patriot missile","volume":"25","author":"Skeel R","year":"1992","journal-title":"SIAM News"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Tiwari A (2004) Termination of linear programs. In: Proceedings of CAV\u201904. Lecture notes in computer science vol 3114 pp 70\u201382","DOI":"10.1007\/978-3-540-27813-9_6"},{"issue":"2","key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1137\/0802011","article-title":"A low complexity interior-point algorithm for linear programming","volume":"2","author":"Todd M","year":"1992","journal-title":"SIAM J Optim"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0572"},{"issue":"3","key":"e_1_2_1_2_14_2","first-page":"102","article-title":"DISCOVERER: a tool for solving semi-algebraic systems. Software Demo at ISSAC 2007, Waterloo, July 30, 2007","volume":"41","author":"Xia B","year":"2007","journal-title":"ACM SIGSAM Bull"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1006\/jsco.1998.0274","article-title":"Recent advances on determining the number of real roots of parametric polynomials","volume":"28","author":"Yang L","year":"1999","journal-title":"J Symb Comput"},{"key":"e_1_2_1_2_16_2","first-page":"628","article-title":"A complete discrimination system for polynomials","volume":"39","author":"Yang L","year":"1996","journal-title":"Sci China (Ser E)"},{"key":"e_1_2_1_2_17_2","unstructured":"Yang L Xia B (2005) Real solution classifications of a class of parametric semi-algebraic systems. In: Proceedings of international conference on algorithmic algebra and logic pp 281\u2013289"},{"key":"e_1_2_1_2_18_2","unstructured":"Yang L Zhan N Xia B Zhou C (2005) Program verification by using DISCOVERER. In: Proceedings of VSTTE\u201905. Lecture notes in computer science vol 4174 pp 575\u2013586"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0144-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0144-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0144-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:59:37Z","timestamp":1641484777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0144-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["10.1007\/s00165-009-0144-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0144-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3]]}}}