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

Jensen, Jonas Finnemann ; Østergaard, Lars Kærlund

4. term

Computer Science, Master

2013

2013-06-07

72

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.

wctl ; model checking ; ctl ; on-the-fly ; local

Download
View record in AAU Student Projects