Nicolas Markey

Abstract

Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.

@inproceedings{atva2014-BGM,
  author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
                         Nicolas},
  title =               {Quantitative verification of weighted {K}ripke
                         structures},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {64-80},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_6},
  abstract =            {Extending formal verification techniques to handle
                         quantitative aspects, both for the models and for
                         the properties to be checked, has become a central
                         research topic over the last twenty years. Following
                         several recent works, we study model checking for
                         (one-dimensional) weighted Kripke structures with
                         positive and negative weights, and temporal logics
                         constraining the total and/or average weight. We
                         prove decidability when only accumulated weight is
                         constrained, while allowing average-weight
                         constraints alone already is undecidable.},
}