Long-run cost analysis by approximation of linear operators over dioids. (English) Zbl 1209.68124
Summary: 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.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q55 | Semantics in the theory of computing |
Keywords:
quantitative behaviour of programsReferences:
| [1] | DOI: 10.1109/SFCS.2005.19 · doi:10.1109/SFCS.2005.19 |
| [2] | Davey, Introduction to Lattices and Order (1990) · Zbl 0701.06001 |
| [3] | DOI: 10.1145/256303.256306 · Zbl 0890.68032 · doi:10.1145/256303.256306 |
| [4] | DOI: 10.1016/S0004-3702(02)00208-4 · doi:10.1016/S0004-3702(02)00208-4 |
| [5] | DOI: 10.1109/SEFM.2005.40 · doi:10.1109/SEFM.2005.40 |
| [6] | DOI: 10.1070/IM1992v038n01ABEH002188 · Zbl 0746.16034 · doi:10.1070/IM1992v038n01ABEH002188 |
| [7] | Gondran, Graphs, Dioids and semirings, New Models and Algorithms (2008) · Zbl 1201.16038 |
| [8] | Dudnikov, Advances in Soviet Mathematics pp 65– (1992) |
| [9] | Baccelli, Synchronization and Linearity (1992) |
| [10] | DOI: 10.1016/j.entcs.2006.01.020 · doi:10.1016/j.entcs.2006.01.020 |
| [11] | DOI: 10.1016/j.tcs.2005.03.002 · Zbl 1142.68444 · doi:10.1016/j.tcs.2005.03.002 |
| [12] | DOI: 10.1016/j.tcs.2007.09.003 · Zbl 1133.68010 · doi:10.1016/j.tcs.2007.09.003 |
| [13] | DOI: 10.1093/logcom/exi008 · Zbl 1070.03008 · doi:10.1093/logcom/exi008 |
| [14] | De Alfaro, Proceedings 13th Symposium on Logic in Computer Science (LICS’98) pp 174– (1998) |
| [15] | Santini, AAAI’08: Proceedings of the 23rd national conference on Artificial intelligence pp 1869– (2008) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
