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

https://hal.inria.fr/hal-01062173
Contributor : Nicolas Markey <>
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

File

avgltl.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

120

Files downloads

844