arXiv subjects

David Cachera

Publications and source records attributed to David Cachera.

2 recordsLinked to original sources

arXiv2019

An $ω$-Algebra for Real-Time Energy Problems

We develop a $^*$-continuous Kleene $ω$-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on $^*$-continuous Kleene $ω$-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and Büchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.

cs.LO↗

arXiv2010

Injecting Abstract Interpretations into Linear Cost Models

We present a semantics based framework for analysing the quantitative behaviour of programs with regard to resource usage. We start from an operational semantics equipped with costs. The dioid structure of the set of costs allows for defining the quantitative semantics as a linear operator. We then present an abstraction technique inspired from abstract interpretation in order to effectively compute global cost information from the program. Abstraction has to take two distinct notions of order into account: the order on costs and the order on states. We show that our abstraction technique provides a correct approximation of the concrete cost computations.

cs.LO↗