Skip to Main content Skip to Navigation
Conference papers

Averaging in~LTL

Abstract : For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean--either a property is true, or it is false. We believe that this is too crude in a context where quantitative information and constraints are crucial: correctness should be quantified! In a recent line of works, several authors have proposed quantitative semantics for temporal logics, using e.g. discounting modalities (which give less importance to distant events). In the present paper, we define and study a quantitative semantics of LTL with averaging modalities, either on the long run or within an until modality. This, in a way, relaxes the classical Boolean semantics of LTL, and provides a measure of certain properties of a model. We prove that computing and even approximating the value of a formula in this logic is undecidable.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Nicolas Markey Connect in order to contact the contributor
Submitted on : Thursday, September 11, 2014 - 1:48:02 PM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM
Long-term archiving on: : Friday, December 12, 2014 - 10:15:19 AM


Files produced by the author(s)




Patricia Bouyer, Nicolas Markey, Raj~mohan Matteplackel. Averaging in~LTL. Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14), Sep 2014, Rome, Italy. pp.266-280, ⟨10.1007/978-3-662-44584-6_19⟩. ⟨hal-01062173⟩



Record views


Files downloads