Long-Run Cost Analysis by Approximation of Linear Operators over Dioids

David Cachera 1 Thomas Jensen 1 Arnaud Jobin 1 Pascal Sotin 1
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : In this paper we present a semantics-based framework for analysing the quantitative behaviour of programs with respect to resource usage. We start from an operational semantics in which costs are modelled using a dioid structure. The dioid structure of costs allows the definition of the quantitative semantics as a linear operator. We then develop a theory of approximation of such a semantics, which is akin to what is offered by the theory of abstract interpretation for analysing qualitative properties, in order to compute effectively global cost information from the program. We focus on the notion of long-run cost, which models the asymptotic average cost of a program. The abstraction of the semantics has to take two distinct notions of order into account: the order on costs and the order on states. We prove that our abstraction technique provides a correct approximation of the concrete long-run cost of a program.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2010, 20 (4), pp.589-624. 〈10.1017/S0960129510000113〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00699608
Contributeur : David Cachera <>
Soumis le : lundi 21 mai 2012 - 12:40:23
Dernière modification le : vendredi 16 novembre 2018 - 01:39:10

Lien texte intégral

Identifiants

Citation

David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2010, 20 (4), pp.589-624. 〈10.1017/S0960129510000113〉. 〈hal-00699608〉

Partager

Métriques

Consultations de la notice

298