Compositionality & Abstraction in verification of Probabilistic Transition
Authors
Anh, Tu Hoang ; Ahiable, Antoinette
Term
4. term
Education
Publication year
2003
Abstract
Dette speciale undersøger, hvordan man kan reducere antallet af tilstande, der skal udforskes ved verifikation af probabilistiske transitionssystemer (modeller med tilstande og sandsynlighedsvægtede overgange). Vores tilgang er kompositionel abstraktion: vi laver enkle abstraktioner af de enkelte komponenter i et samtidig system og bruger dem direkte i modeltjek (model checking), så egenskaber kan kontrolleres uden alle detaljer. For at sikre, at abstraktionerne er korrekte, bygger vi på probabilistisk simulations-præorden, en relation der bevarer adfærd på en sikker måde. Vi præsenterer også en minimeringsalgoritme for PTS, som slår tilstande sammen og danner en mindre struktur, der bevarer adfærd op til simulationsækvivalens. Dernæst introducerer vi en kvotienteringsteknik (Quotient) for vores PTS-model. Den oprindelige idé var at bruge minimeringsalgoritmen til at gøre de transformerede specifikationer mindre; men vi viser, at dette aldrig bliver relevant, fordi den transformerede specifikation allerede er minimal givet vores forudsætninger. Derfor anbefaler vi at anvende en forenklingsheuristik på komponenterne før kvotientering i stedet for efter. Vi implementerer kvotienteringsteknikken i vores værktøj, CAPS, og demonstrerer de foreslåede algoritmer.
This thesis explores how to reduce the number of states that must be explored when verifying probabilistic transition systems (models with states and probability-weighted transitions). Our approach is compositional abstraction: we build simple abstractions of individual components in a concurrent system and use them directly in model checking, so properties can be checked without all the details. To ensure that the abstractions are sound, we rely on a probabilistic simulation preorder, a relation that safely preserves behavior. We also present a minimization algorithm for probabilistic transition systems that merges states to produce a smaller structure while preserving behavior up to simulation equivalence. We then introduce a Quotient technique for our PTS model. The initial idea was to use the minimization algorithm to shrink the transformed specifications, but we show this case does not arise: under our constraints and assumptions, the transformed specification is already minimal. Based on this, we recommend applying a simplification heuristic to system components before quotienting rather than after. We implement the Quotient technique in our tool, CAPS, and demonstrate the proposed algorithms.
[This abstract was generated with the help of AI]
Documents