Skip to Main content Skip to Navigation
Journal articles

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
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Document type :
Journal articles
Complete list of metadatas
Contributor : David Cachera <>
Submitted on : Monday, May 21, 2012 - 12:40:23 PM
Last modification on : Friday, July 10, 2020 - 4:25:17 PM

Links full text



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⟩



Record views