{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T01:05:32Z","timestamp":1784768732194,"version":"3.55.0"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2014,8,21]],"date-time":"2014-08-21T00:00:00Z","timestamp":1408579200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We address the problem of conditional termination, which is that of defining\nthe set of initial configurations from which a given program always terminates.\nFirst we define the dual set, of initial configurations from which a\nnon-terminating execution exists, as the greatest fixpoint of the function that\nmaps a set of states into its pre-image with respect to the transition\nrelation. This definition allows to compute the weakest non-termination\nprecondition if at least one of the following holds: (i) the transition\nrelation is deterministic, (ii) the descending Kleene sequence\noverapproximating the greatest fixpoint converges in finitely many steps, or\n(iii) the transition relation is well founded. We show that this is the case\nfor two classes of relations, namely octagonal and finite monoid affine\nrelations. Moreover, since the closed forms of these relations can be defined\nin Presburger arithmetic, we obtain the decidability of the termination problem\nfor such loops.<\/jats:p>","DOI":"10.2168\/lmcs-10(3:8)2014","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T09:40:57Z","timestamp":1415958057000},"source":"Crossref","is-referenced-by-count":10,"title":["Deciding Conditional Termination"],"prefix":"10.46298","volume":"Volume 10, Issue 3","author":[{"given":"Radu","family":"Iosif","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Filip","family":"Konecny","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2014,8,21]]},"reference":[{"key":"788:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/737\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/737\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:49Z","timestamp":1681242889000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,21]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-10(3:8)2014","relation":{"is-same-as":[{"id-type":"arxiv","id":"1302.2762","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1302.2762","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1145\/3121136","asserted-by":"subject"},{"id-type":"doi","id":"10.17863\/cam.41431","asserted-by":"subject"},{"id-type":"handle","id":"1983\/bfcd960b-b1f8-4484-94d9-826cdf6635ba","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,21]]},"article-number":"737"}}