Logic in Computer Science (LICS 1997)

Paper: Quantitative Analysis and Model Checking (at LICS 1997)

Authors: Michael Huth Marta Kwiatkowska

Abstract

Many notions of models in computer science provide quantitative information, or uncertainties, which necessitate a quantitative model checking paradigm. We present such a framework for reactive and generative systems based on a non-standard interpretation of the modal mu-calculus, where mu x.phi / nu x.phi are interpreted as least/greatest fixed points over the infinite lattice of maps from states to the unit interval. By letting formulas denote lower bounds of probabilistic evidence of properties, the values computed by our quantitative model checker can serve as satisfactory correctness guarantees in cases where conventional qualitative model checking fails. Since fixed point iteration in this infinite domain is computationally unfeasible, we establish that the computation of fixed points may be restated as a conventional, and on average efficient, optimization problem in linear programming; this holds for a fragment of the modal mu-calculus which subsumes CTL. Our semantics induces a state equivalence which is strictly in between probabilistic bisimulation and probabilistic ready bisimulation.

BibTeX

  @InProceedings{HuthKwiatkowska-QuantitativeAnalysi,
    author = 	 {Michael Huth and Marta Kwiatkowska},
    title = 	 {Quantitative Analysis and Model Checking},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {111--122},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }