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

Vi præsenterer min-max-grafer – en teknik til at omsætte modeltjek-problemet for vægtet Computation Tree Logic (CTL) med ikke-negative begrænsninger på modaliteterne over vægtede Kripke-strukturer. Modeltjek er automatisk kontrol af, om en systemmodel opfylder en formel. Vægtet CTL er en grenlogik med numeriske vægte, og vægtede Kripke-strukturer er tilstands-overgangsgrafer, hvor tilstande eller overgange har vægte. Vi gennemgår tidligere tilgange baseret på afhængighedsgrafer og deres symbolske udvidelse. Med min-max-grafer viser vi, hvordan modeltjek kan udføres som en fikspunktberegning på en graf, der koder problemet. Vi bruger både globale algoritmer, der analyserer hele grafen, og lokale/on-the-fly algoritmer, der kun udforsker de nødvendige dele. Fikspunktberegning betyder, at man gentager beregninger, indtil resultaterne ikke længere ændrer sig. Vi har implementeret algoritmerne og evalueret deres ydeevne i eksperimenter. Resultaterne viser, at den lokale tilgang ofte er meget fordelagtig.

We present min-max graphs, a technique for encoding the model checking problem of weighted Computation Tree Logic (CTL) with nonnegative constraints on the modalities over weighted Kripke structures. Model checking automatically verifies whether a system model satisfies a specification. Weighted CTL is a branching-time logic with numerical weights, and weighted Kripke structures are state-transition graphs in which states or transitions carry weights. We review prior approaches based on dependency graphs and their symbolic extension. With min-max graphs, we show how to perform model checking as a fixed-point computation on a graph that encodes the problem. We use both global algorithms that analyze the whole graph and local/on-the-fly algorithms that explore only the parts needed. Fixed-point computation means iterating until the results stop changing. We implemented the algorithms and evaluated their performance experimentally. The results indicate that the local approach is often very advantageous.

[This abstract was generated with the help of AI]

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

Download
View record in AAU Student Projects