Averaging in~LTL - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Averaging in~LTL

Résumé

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.
Fichier principal
Vignette du fichier
avgltl.pdf (642.42 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01062173 , version 1 (11-09-2014)

Identifiants

Citer

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⟩
53 Consultations
211 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More