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

Studenteropgave: Speciale (inkl. HD afgangsprojekt)

  • Jonas Finnemann Jensen
  • Lars Kærlund Østergaard
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
Udgivelsesdato7 jun. 2013
Antal sider72
ID: 77336060