Nicolas Markey

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.

@inproceedings{concur2014-BMM,
  author =              {Bouyer, Patricia and Markey, Nicolas and
                         Matteplackel, Raj~Mohan},
  title =               {Averaging in~{LTL}},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8704},
  pages =               {266-280},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_19},
  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!\par In a
                         recent line of works, several authors have proposed
                         quantitative semantics for temporal logics, using
                         e.g. \emph{discounting} modalities (which give less
                         importance to distant events). In~the present paper,
                         we define and study a quantitative semantics of~LTL
                         with \emph{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.},
}