Osaline otsinguruumi vähendamine

Sissejuhatus

Mudelikontrolli puhul osutub probleemiks Kripke struktuuri ehk sildistatud olekumasina "lahti voltimine" mis viib olekuruumi eksponentisaalse kasvuni. Konservatiivse lähenemise puhul kasutatakse Kripke struktuuri kirjeldamiseks kohandatud andmestruktuure, pakitakse informatsiooni ning kasutatakse symbolic model checking milles kasutakse OBDD lähenemist.

Agressiivsema lähenemise puhul eemaldatakse üleliigseid olekuid selleks, et vähendada olekuruumi. Osaline ... vähendamine (partial order reduction) tähendab kommutatiivsete paralleelsete üleminekute (transition) leidmist mis viivad sama olekuni. Paralleelsetes süsteemides üleminekud võivad toimuda suvalises järjestuses, mistõttu toimub järjekordne kombinatoorne olekuruumi järsk kasv.

Täielik olekute hulk (ample set) peab arvestama piisavalt käitumist, nii et vähendatud mudelikontroll siiski õige tulemi annaks. Vähendatud olekute graaf peaks olema märgatavalt väiksem kui kogu olekute graaf (enabled set). Selleks et tuletada kogu olekute graafist vähendatud täielike olekute graaf, peab kuluma mõistlik hulk arvutusvõimsust.

Semantika

Üleminek α on lubatud (enabled) olekus s kui eksisteerib olek s' nii et üleminek α(s, s') mis viib olekust s olekusse s'. Iga oleku kohta on seega defineeritud lubatud üleminekud kui:

\begin{equation*} enabled(s) \subseteq T \end{equation*}

Vastasel korral ei ole see üleminek lubatud (disabled) vastavas olekus:

\begin{equation*} disabled(s) \subseteq T \setminus enabled(s) \end{equation*}

Eeldame et kõik üleminekud on deterministlikud, see tähendab et iga oleku s kohta on kõige enam üks olek s' ülemineku α(s, s') kohta ning üleminekuid märgime üles:

\begin{equation*} s^\prime = \alpha \equiv \alpha(s, s^\prime) \end{equation*}

Tee (path) π on lõplik või lõputu üleminekute järjestus:

\begin{equation*} \pi = s_0 \xrightarrow{a_1} s_1 \xrightarrow{a_2} ... \end{equation*}

Kaks üleminekut α, β on sõltumatud (independent) kui iga oleku s kohta järgnev kehtib:

\begin{equation*} \alpha, \beta \in enabled(s) \implies \alpha \in enabled(\beta(s)) \end{equation*}

Ning mõlemad üleminekud viivad samasse olekusse:

\begin{equation*} \alpha, \beta \in enabled(s) \implies \alpha(\beta(s)) = \beta(\alpha(s)) \end{equation*}

Sõltuvussuhet (dependence relation) märgitakse üles järgnevalt, kus T on üleminek:

\begin{equation*} D \subseteq T \times T \end{equation*}

Analoogselt võime sõltumatussuhte (independence relation) kirja panna kui:

\begin{equation*} I \subseteq T \times T \setminus D \end{equation*}

Üleminek α on nähtamatu (invisible) kui väidete hulk (set of atomic propositions) ei muutu selle ülemineku käigus. Üleminek α on nähtav (visible), kui mõni väide (atomic propositional) muutub selle ülemineku toimudes.

Kokutav ekvivalent

Kokutavaks ekvivalendiks (stuttering equivalent) nimetatakse kahte LTL teed, kus osad olekud on korduvad ehk nende vahel on nähtamatud üleminekud. LTL valem ilma X operaatorita on invariant kokutamise puhul.

Mudelid M ja M' on kokutavad ekvivalendid kui iga tee π kohta mudelis M mis algab esialgses olekus vastab tee π' mudelis M' mis algab samast olekust ning teed π ja π' on kokutavad ekvivalendid.

Võime öelda et kui M ja M' on kokutavad ekvivalendid siis iga X operaatorita LTL valemi kohta järgnev väide kehtib:

\begin{equation*} M,s_0 \models A \varphi \iff M^\prime,s_ \models A \varphi \end{equation*}

Mudelikontrollis piisab ühe mudeli kasutamisest sellisel juhul.

Taandamisreeglid

Nähtamatud üleminekud saab taandada ning sõltumatud üleminekud saab ettepoole nihutada (prepone).

C0: Kui olekust ei ole väljuvaid üleminekuid siis ka piisav üleminekute hulk on tühihulk. Seda võib ka interpreteerida et olekust ei saa teha deadlocki kui seda seal eelnevalt pole ning ei saa lisada üleminekuid mida eelnevalt pole:

\begin{equation*} ample(s) = \varnothing \iff enabled(s) = \varnothing \end{equation*}

C1: Kõik üleminekud mis on lubatud üleminekute hulgas enabled(s) kuid mitte piisavas üleminekute hulgas ample(s) peavad olema sõltumatud ǘleminekutest hulgas ample(s). Sõltumatud üleminekud võib ettepoole tõsta (prepone).

C2: Kui ample(s) ≠ enabled(s) siis iga üleminek hulgas ample(s) peab olema nähtamatu. Nähtamatuid üleminekuid võib ettepoole tõsta.

C3: Olekutest ei saa moodustada tsükkleid.

C4*: Kas enabled(s) = ample(s) või ample(s) sisaldab vaid ühte üleminekut.

Otsingualgoritm

SEEN = []

def expand_state(state):
    transitions =
    # Iterate over ample transitions set for this state
    for transition in ample(s):
        new_state = transition(s)
        if new_state not in SEEN:
            SEEN.append(new_state)
            expand_state(state)

Sügavuti

Viited

Partial Order Reduction - Wikipedia, the free encyclopedia

QAoES TU Berlin