{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:08:42Z","timestamp":1774987722277,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,7,14]],"date-time":"2007-07-14T00:00:00Z","timestamp":1184371200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2007,7,14]]},"DOI":"10.1145\/1273920.1273943","type":"proceedings-article","created":{"date-parts":[[2012,10,10]],"date-time":"2012-10-10T14:45:29Z","timestamp":1349880329000},"page":"167-178","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Induction for positive almost sure termination"],"prefix":"10.1145","author":[{"given":"Isabelle","family":"Gnaedig","sequence":"first","affiliation":[{"name":"LORIA-INRIA"}]}],"member":"320","published-online":{"date-parts":[[2007,7,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"USA","author":"Nipkow F. Baaderand T.","year":"1998","unstructured":"F. Baaderand T. Nipkow . Term rewriting and all that Cambridge University Press, New York, NY , USA , 1998 . F. Baaderand T. Nipkow. Term rewriting and all that Cambridge University Press, New York, NY, USA, 1998."},{"key":"e_1_3_2_1_2_1","series-title":"Lecture Notes in Computer Science pages 84--155","volume-title":"Introduction to stochastic Petri nets","author":"Balbo G.","year":"2001","unstructured":"G. Balbo . Introduction to stochastic Petri nets . volume 2090 of Lecture Notes in Computer Science pages 84--155 . Springer-Verlag , 2001 . G. Balbo. Introduction to stochastic Petri nets. volume 2090 of Lecture Notes in Computer Science pages 84--155. Springer-Verlag, 2001."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications Electronic Notes in Theoretical Computer Science, Pont-\u00e0-Mousson (France)","author":"Borovansk\u00fd P.","year":"1998","unstructured":"P. Borovansk\u00fd , C. Kirchner , H. Kirchner , P.-E. Moreau , and C. Ringeissen . An Overview of ELAN In C. Kirchner and H.Kirchner, editors , Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications Electronic Notes in Theoretical Computer Science, Pont-\u00e0-Mousson (France) , Sept. 1998 . Elsevier Science Publishers B. V. (North-Holland). P. Borovansk\u00fd, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An Overview of ELAN In C. Kirchner and H.Kirchner, editors, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications Electronic Notes in Theoretical Computer Science, Pont-\u00e0-Mousson (France), Sept. 1998. Elsevier Science Publishers B. V. (North-Holland)."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_27"},{"key":"e_1_3_2_1_6_1","volume-title":"Strat\u00e9gies de r\u00e9\u00e9criture probabilistes dans ELAN 4.HAL-INRIA Open Archive Number inria-00104091","author":"Bournez O.","year":"2004","unstructured":"O. Bournez , F. Garnier , and C. Kirchner . Strat\u00e9gies de r\u00e9\u00e9criture probabilistes dans ELAN 4.HAL-INRIA Open Archive Number inria-00104091 , 2004 . O. Bournez, F. Garnier, and C. Kirchner. Strat\u00e9gies de r\u00e9\u00e9criture probabilistes dans ELAN 4.HAL-INRIA Open Archive Number inria-00104091, 2004."},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science pages 252--266","volume-title":"Proceedings of the 13th International Conference on Rewriting Techniques and Applications","author":"Bournez O.","year":"2002","unstructured":"O. Bournez and C. Kirchner . Probabilistic rewrite strategies: Applications to ELAN . In S. Tison, editor, Proceedings of the 13th International Conference on Rewriting Techniques and Applications volume 2378 of Lecture Notes in Computer Science pages 252--266 . Springer , 2002 . O. Bournez and C. Kirchner. Probabilistic rewrite strategies: Applications to ELAN. In S. Tison, editor, Proceedings of the 13th International Conference on Rewriting Techniques and Applications volume 2378 of Lecture Notes in Computer Science pages 252--266. Springer, 2002."},{"key":"e_1_3_2_1_8_1","first-page":"365","volume-title":"Compiler Construction (CC '01)volume 2027 of Lecture Notes in Computer Science","author":"Brand M.","year":"2001","unstructured":"M. Brand , A. Deursen , J. Heering , H. Jong , M. Jonge , T. Kuipers , P. Klint , L. Moonen , P. Olivier , J. Scheerder , J. Vinju , E. Visser , and J. Visser . The ASF+SDF Meta-Environment: a Component-Based Language Development Environment . In R. Wilhelm, editor, Compiler Construction (CC '01)volume 2027 of Lecture Notes in Computer Science pages 365 -- 370 . Springer , 2001 . M. Brand, A. Deursen, J. Heering, H. Jong, M. Jonge, T. Kuipers, P. Klint, L. Moonen, P. Olivier, J. Scheerder, J. Vinju, E. Visser, and J. Visser. The ASF+SDF Meta-Environment: a Component-Based Language Development Environment. In R. Wilhelm, editor, Compiler Construction (CC '01)volume 2027 of Lecture Notes in Computer Science pages 365--370. Springer, 2001."},{"key":"e_1_3_2_1_9_1","series-title":"Lecture Notes in Computer Science pages 76--87","volume-title":"Proceedings of the 14th International Conference on Rewriting Techniques and Applications","author":"Clavel M.","year":"2003","unstructured":"M. Clavel , F. Dur\u00e1n , S. Eker , P. Lincoln , N. Mart\u00ed-Oliet , J. Meseguer , and C. Talcott . The Maude 2.0 system . In R. Nieuwenhuis, editor, Proceedings of the 14th International Conference on Rewriting Techniques and Applications volume 2706 of Lecture Notes in Computer Science pages 76--87 . Springer , June 2003 . M. Clavel, F. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and C. Talcott. The Maude 2.0 system. In R. Nieuwenhuis, editor, Proceedings of the 14th International Conference on Rewriting Techniques and Applications volume 2706 of Lecture Notes in Computer Science pages 76--87. Springer, June 2003."},{"key":"e_1_3_2_1_10_1","unstructured":"Ieee csma\/ca 802.11 working group home page. http:\/\/www.ieee802.org\/11\/.  Ieee csma\/ca 802.11 working group home page. http:\/\/www.ieee802.org\/11\/."},{"key":"e_1_3_2_1_11_1","volume-title":"Stanford University","author":"de Alfaro L.","year":"1998","unstructured":"L. de Alfaro . Formal Verification of Probabilistic Systems PhD thesis , Stanford University , 1998 . L. de Alfaro. Formal Verification of Probabilistic Systems PhD thesis, Stanford University, 1998."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1016\/B978-044450813-3\/50011-4","volume-title":"Handbook of Automated Reasoning","author":"Dershowitz N.","year":"2001","unstructured":"N. Dershowitz and D. Plaisted . Rewriting . In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning volume I , chapter 9, pages 535 -- 610 . Elsevier Science , 2001 . N. Dershowitz and D. Plaisted. Rewriting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning volume I, chapter 9, pages 535--610. Elsevier Science, 2001."},{"key":"e_1_3_2_1_13_1","series-title":"Electronic Notes in Theoretical Computer Science Elsevier Science Publishers B","volume-title":"Selected papers of the 4th International Workshop on Strategies in Automated Deduction","author":"Fissore O.","year":"2001","unstructured":"O. Fissore , I. Gnaedig , and H. Kirchner . Termination of rewriting with local strategies . In M. P. Bonacina and B. Gramlich, editors, Selected papers of the 4th International Workshop on Strategies in Automated Deduction volume 58 of Electronic Notes in Theoretical Computer Science Elsevier Science Publishers B . V. (North-Holland) , 2001 . O. Fissore, I. Gnaedig, and H. Kirchner. Termination of rewriting with local strategies. In M. P. Bonacina and B. Gramlich, editors, Selected papers of the 4th International Workshop on Strategies in Automated Deduction volume58 of Electronic Notes in Theoretical Computer Science Elsevier Science Publishers B. V. (North-Holland), 2001."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571164"},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications","volume":"71","author":"Fissore O.","year":"2002","unstructured":"O. Fissore , I. Gnaedig , and H. Kirchner . Outermost ground termination . In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications volume 71 of Electronic Notes in Theoretical Computer Science Pisa, Italy , 2002 . Elsevier Science Publishers B. V. (North-Holland). O. Fissore, I. Gnaedig, and H. Kirchner. Outermost ground termination. In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications volume 71 of Electronic Notes in Theoretical Computer Science Pisa, Italy, 2002. Elsevier Science Publishers B. V. (North-Holland)."},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the third Workshop on Rule-Based Constraint Reasoning and Programming (RCoRP'01)","author":"Fr\u00fdhwirth T.","year":"2001","unstructured":"T. Fr\u00fdhwirth , A. Di Pierro , and H. Wiklicky . Toward probabilistic constraint handling rules. In S. Abdennadher and T. Fr\u00fdhwirth, editors , Proceedings of the third Workshop on Rule-Based Constraint Reasoning and Programming (RCoRP'01) Paphos, Cyprus , 2001 . T. Fr\u00fdhwirth, A. Di Pierro, and H. Wiklicky. Toward probabilistic constraint handling rules. In S. Abdennadher and T. Fr\u00fdhwirth, editors, Proceedings of the third Workshop on Rule-Based Constraint Reasoning and Programming (RCoRP'01)Paphos, Cyprus, 2001."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/523981.852154"},{"key":"e_1_3_2_1_18_1","volume-title":"Institut National Polytechnique de Lorraine","author":"Garnier F.","year":"2007","unstructured":"F. Garnier . Terminaison en temps moyen fini de syst\u00e8mes de r\u00e8gles probabilistes PhD thesis , Institut National Polytechnique de Lorraine , Nancy, France , 2007 . To be defended. F. Garnier. Terminaison en temps moyen fini de syst\u00e8mes de r\u00e8gles probabilistes PhD thesis, Institut National Polytechnique de Lorraine, Nancy, France, 2007. To be defended."},{"key":"e_1_3_2_1_19_1","volume-title":"Induction for positive almost sure termination. Extended version. HAL-INRIA Open Archive Number inria-00147450","author":"Gnaedig I.","year":"2007","unstructured":"I. Gnaedig . Induction for positive almost sure termination. Extended version. HAL-INRIA Open Archive Number inria-00147450 , 2007 . I. Gnaedig. Induction for positive almost sure termination. Extended version. HAL-INRIA Open Archive Number inria-00147450, 2007."},{"key":"e_1_3_2_1_20_1","volume-title":"Termination of rewriting under strategies: a generic approach","author":"Gnaedig I.","year":"2006","unstructured":"I. Gnaedig and H. Kirchner . Termination of rewriting under strategies: a generic approach . 2006 . Submitted. Also as HAL-INRIA Open Archive Number inria-00113156. I. Gnaedig and H. Kirchner. Termination of rewriting under strategies: a generic approach. 2006. Submitted. Also as HAL-INRIA Open Archive Number inria-00113156."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2428096.2428097"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647195.720842"},{"key":"e_1_3_2_1_23_1","unstructured":"G. Grimmett. Probability Theory Cambridge University Press 1993.  G. Grimmett. Probability Theory Cambridge University Press 1993."},{"key":"e_1_3_2_1_24_1","volume-title":"Time and Probability in Formal Design of Distributed Systems Series in Real-Time Safety Critical Systems","author":"Hansson H.","year":"1994","unstructured":"H. Hansson . Time and Probability in Formal Design of Distributed Systems Series in Real-Time Safety Critical Systems . Elsevier , 1994 . H. Hansson. Time and Probability in Formal Design of Distributed Systems Series in Real-Time Safety Critical Systems. Elsevier, 1994."},{"key":"e_1_3_2_1_25_1","series-title":"Lecture Notes in Computer Science pages 73--84","volume-title":"Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation","author":"T.","year":"2004","unstructured":"T. H&233;rault, R. Lassaigne , F. Magniette , and S. Peyronnet . Approximate probabilistic model checking . In B. Steffen and G. Levi, editors, Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation volume 2937 of Lecture Notes in Computer Science pages 73--84 . Springer , 2004 . T. H&233;rault, R. Lassaigne, F. Magniette, and S. Peyronnet. Approximate probabilistic model checking. In B. Steffen and G. Levi, editors, Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation volume 2937 of Lecture Notes in Computer Science pages 73--84. Springer, 2004."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00215-7"},{"key":"e_1_3_2_1_27_1","first-page":"210","article-title":"Well-quasi ordering, the tree theorem and Vazsonyi's conjecture","volume":"95","author":"Kruskal J. B.","year":"1960","unstructured":"J. B. Kruskal . Well-quasi ordering, the tree theorem and Vazsonyi's conjecture . Trans. Amer. Math. Soc . 95 : 210 -- 225 , 1960 . J. B. Kruskal. Well-quasi ordering, the tree theorem and Vazsonyi's conjecture. Trans. Amer. Math. Soc.95:210--225, 1960.","journal-title":"Trans. Amer. Math. Soc"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39958-2_3"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789069"},{"key":"e_1_3_2_1_30_1","series-title":"Lecture Notes in Computer Science pages 200--204","volume-title":"Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools","author":"Kwiatkowska M. Z.","year":"2002","unstructured":"M. Z. Kwiatkowska , G. Norman , and D. Parker . PRISM: Probabilistic symbolic model checker . In T. Field, P. G. Harrison, J. T. Bradley, and U. Harder, editors, Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools volume 2324 of Lecture Notes in Computer Science pages 200--204 . Springer , 2002 . M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In T. Field, P. G. Harrison, J. T. Bradley, and U. Harder, editors, Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools volume 2324 of Lecture Notes in Computer Science pages 200--204. Springer, 2002."},{"issue":"3","key":"e_1_3_2_1_31_1","first-page":"213","article-title":"Completeness results for basic narrowing. Applicable Algebra in Engineering","volume":"5","author":"Middeldorp A.","year":"1994","unstructured":"A. Middeldorp and E. Hamoen . Completeness results for basic narrowing. Applicable Algebra in Engineering , Communication and Computation 5 ( 3&4 ): 213 -- 253 , 1994 . A. Middeldorp and E. Hamoen. Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computation 5(3&4):213--253, 1994.","journal-title":"Communication and Computation"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765931.1765938"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms Cambridge University Press","author":"Motwani R.","year":"1995","unstructured":"R. Motwani and P. Raghavan . Randomized Algorithms Cambridge University Press , 1995 . R. Motwani and P. Raghavan. Randomized Algorithms Cambridge University Press, 1995."},{"key":"e_1_3_2_1_34_1","first-page":"15","volume-title":"Proceedings of the 1998 Joint Conference on Declarative Programming","author":"Pierro A. D.","year":"1998","unstructured":"A. D. Pierro and H. Wiklicky . A Markov model for probabilistic concurrent constraint programming. In J. L. Freire-Nistal, M. Falaschi, and M. V. Ferro, editors , Proceedings of the 1998 Joint Conference on Declarative Programming pages 15 -- 28 , 1998 . A. D. Pierro and H. Wiklicky. A Markov model for probabilistic concurrent constraint programming. In J. L. Freire-Nistal, M. Falaschi, and M. V. Ferro, editors, Proceedings of the 1998 Joint Conference on Declarative Programming pages 15--28, 1998."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/857172.857259"},{"key":"e_1_3_2_1_36_1","series-title":"Lecture Notes in Computer Science pages 446--455","volume-title":"Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science","author":"Pierro A. D.","year":"1998","unstructured":"A. D. Pierro and H. Wiklicky . Probabilistic concurrent constraint programming: Towards a fully abstract model . In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science volume 1450 of Lecture Notes in Computer Science pages 446--455 . Springer , 1998 . A. D. Pierro and H. Wiklicky. Probabilistic concurrent constraint programming: Towards a fully abstract model. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science volume 1450 of Lecture Notes in Computer Science pages 446--455. Springer, 1998."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351284"},{"key":"e_1_3_2_1_38_1","first-page":"315","volume-title":"Stochastic activity networks: formal definitions and concepts","author":"Sanders W. H.","year":"2002","unstructured":"W. H. Sanders and J. F. Meyer . Stochastic activity networks: formal definitions and concepts . pages 315 -- 343 , 2002 . W. H. Sanders and J. F. Meyer. Stochastic activity networks: formal definitions and concepts. pages 315--343, 2002."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1137\/0214070"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_3_2_1_41_1","volume-title":"Term Rewriting Systems Number55inCambridge Tracts in Theoretical Computer Science","year":"2003","unstructured":"Terese. Term Rewriting Systems Number55inCambridge Tracts in Theoretical Computer Science . Cambridge University Press , 2003 . Terese. Term Rewriting Systems Number55inCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_3_2_1_43_1","series-title":"Lecture Notes in Computer Science pages 357--361","volume-title":"Proceedings of the 12th International Conference on Rewriting Techniques and Applications","author":"Visser E.","year":"2001","unstructured":"E. Visser . Stratego : A Language for Program Transformation based on Rewriting Strategies. System Description for Stratego 0.5 . In A. Middeldorp, editor, Proceedings of the 12th International Conference on Rewriting Techniques and Applications volume 2051 of Lecture Notes in Computer Science pages 357--361 . Springer , 2001 . E. Visser. Stratego: A Language for Program Transformation based on Rewriting Strategies. System Description for Stratego 0.5. In A. Middeldorp, editor, Proceedings of the 12th International Conference on Rewriting Techniques and Applications volume 2051 of Lecture Notes in Computer Science pages 357--361. Springer, 2001."}],"event":{"name":"PPDP07: Principles and Practice of Declarative Programming","location":"Wroclaw Poland","acronym":"PPDP07","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1273920.1273943","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1273920.1273943","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:58:09Z","timestamp":1750258689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1273920.1273943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,14]]},"references-count":43,"alternative-id":["10.1145\/1273920.1273943","10.1145\/1273920"],"URL":"https:\/\/doi.org\/10.1145\/1273920.1273943","relation":{},"subject":[],"published":{"date-parts":[[2007,7,14]]},"assertion":[{"value":"2007-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}