Complexity Bounds for Ordinal-Based Termination

Sylvain Schmitz 1, 2
1 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : ‘What more than its truth do we know if we have a proof of a theorem in a given formal system?’ We examine Kreisel’s question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program running times. Our main tool for this are length function theorems, which provide complexity bounds on the use of well quasi orders. We illustrate how to prove such theorems in the simple yet until now untreated case of ordinals. We show how to apply this new theorem to derive complexity bounds on programs when they are proven to terminate thanks to a ranking function into some ordinal.
Type de document :
Communication dans un congrès
Joël Ouaknine; Igor Potapov; James Worrell. 8th International Workshop on Reachability Problems, Sep 2014, Oxford, United Kingdom. Springer, 8762, pp.1--19, Lecture Notes in Computer Science. 〈10.1007/978-3-319-11439-2_1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01076701
Contributeur : Sylvain Schmitz <>
Soumis le : mercredi 22 octobre 2014 - 18:57:41
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Lien texte intégral

Identifiants

Collections

Citation

Sylvain Schmitz. Complexity Bounds for Ordinal-Based Termination. Joël Ouaknine; Igor Potapov; James Worrell. 8th International Workshop on Reachability Problems, Sep 2014, Oxford, United Kingdom. Springer, 8762, pp.1--19, Lecture Notes in Computer Science. 〈10.1007/978-3-319-11439-2_1〉. 〈hal-01076701〉

Partager

Métriques

Consultations de la notice

129