The Quotient Technique for Probabilistic Systems
Author
Vestergaard, Jacob
Term
4. term
Education
Publication year
2001
Abstract
At verificere systemer, der både rummer tilfældighed og valg, er svært på grund af tilstandseksplosion, hvor antallet af mulige kombinationer af tilstande vokser eksplosivt. I afhandlingen præsenterer vi en kompositionel kvotientteknik, der afhjælper dette ved trin for trin at fjerne komponenter fra systemet og samtidig omskrive specifikationen, så den stadig beskriver den resterende del korrekt. Vi bygger på teorien om probabilistiske alternerende transitionssystemer: modeller der kombinerer ikke-deterministisk og probabilistisk adfærd, og som kan beskrive både synkron og asynkron interaktion mellem komponenter. Vi introducerer en probabilistisk modal logik (kaldet \logic), et sprog til at beskrive systemegenskaber, for hvilken vi definerer kvotientoperationen. Det fører til en udvidelse af logikken med en generel modalitet, som vi analyserer for at kunne anvende forenklingsheuristikker på de formler, kvotienteringen skaber. Vi giver et formelt bevis for, at kvotientteknikken er korrekt, og vi undersøger i særlig grad, hvordan de kvotienterede formler kan forenkles i praksis. Vi implementerer teknikken i Moscow ML og beskriver centrale elementer i implementeringen. Til sidst afprøver vi implementeringen for at vurdere, hvor effektiv kvotientteknikken er.
Verifying systems that involve both randomness and choice is challenging because of the state explosion problem, where the number of possible state combinations grows rapidly. This thesis presents a compositional quotient technique that addresses this by removing components step by step while rewriting the specification so it still accurately describes the remaining system. We build on the theory of probabilistic alternating transition systems: models that combine non-deterministic and probabilistic behavior and can capture both synchronous and asynchronous interaction between components. We introduce a probabilistic modal logic (called \logic in the thesis), a language for specifying system properties, for which we define the quotient operation. This leads to extending the logic with a general modality, which we study in detail to enable simplification heuristics for the formulas produced by quotienting. We provide a formal proof of correctness for the technique and pay special attention to simplifying quotiented formulas in practice. We implement the technique in Moscow ML and describe key parts of the implementation. Finally, we run tests on the implementation to evaluate the effectiveness of the quotient technique.
[This abstract was generated with the help of AI]
Documents