On-The-Fly Model Checking of Weighted Computation Tree Logic

Student thesis: Master thesis (including HD thesis)

  • Jonas Finnemann Jensen
  • Lars Kærlund Østergaard
4. term, Computer Science, Master (Master Programme)
We present min-max graphs; a technique to encode the model checking problem of weighted
Computation Tree Logic (CTL), with nonnegative constraints on the modalities, against
weighted Kripke structures.
We outline previous efforts to encode this problem using dependency graphs and their symbolic extension.
We demonstrate how to model check weighted CTL through fixed-point computation on a graph that encodes
the problem, using global and local/on-the-fly fixed-point algorithms.
Moreover, we have implemented the algorithms and evaluated their performance through experiments.
In turn, we conclude that the local approach is often very advantageous.
Publication date7 Jun 2013
Number of pages72
ID: 77336060