On-The-Fly Model Checking of Weighted Computation Tree Logic
Authors
Jensen, Jonas Finnemann ; Østergaard, Lars Kærlund
Term
4. term
Education
Publication year
2013
Submitted on
2013-06-07
Pages
72
Abstract
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.
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.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords
wctl ; model checking ; ctl ; on-the-fly ; local