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.
Type de document :
Communication dans un congrès
Baldan, Paolo and Gorla, Daniele. Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14), Sep 2014, Rome, Italy. Springer, 8704, pp.266-280, 2014, 〈10.1007/978-3-662-44584-6_19〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01062173
Contributeur : Nicolas Markey <>
Soumis le : jeudi 11 septembre 2014 - 13:48:02
Dernière modification le : vendredi 20 avril 2018 - 15:36:02
Document(s) archivé(s) le : vendredi 12 décembre 2014 - 10:15:19

Fichier

avgltl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

65

Téléchargements de fichiers

103