Metoda ověřování modelu (MC) pro konečně stavové systémy a lineární temporální logiku. Princip překladu formulí LTL na automaty nad nekonečnými slovy. Základní symbolické a explicitní algoritmy pro MC a jejich teoretická složitost.

Upozornění: bez nároku na úplnost a korektnost. Podle hesla „lepší něco než nic“. Ale snaha byla o co nejlepší výsledek.

Model checking problem is the problem to decide whether a given model (or system) satisfies a given specification. Specification is a formal description of some property that should be satisfied by the system. Specification is typically given as a formula of some temporal logic.

φ ::= T | a | ¬φ | φ1 ∧ φ2 | Xφ | φ1 U φ2

Fφ := T U φ
Gφ := ¬F¬φ
φ R ψ := ¬(¬φ U ¬ψ) … release

The set of atomic propositions occurring in a formula φ is denoted by AP(φ).

We define the semantics of LTL in terms of languages over infinite words. An alphabet is a set Σ = 2AP , where AP ⊆ AP is a finite subset. A word over alphabet Σ is an infinite sequence w = w(0)w(1)w(2)… ∈ Σ^ω of letters from Σ. For every i ∈ N0, by wi we denote the suffix of w of the form w(i)w(i + 1)w(i + 2)…

Validity of an LTL formula φ for w ∈ Σ^ω, written w |= φ, is defined as follows:
w |= T
w |= a iff a ∈ w(0)
w |= ¬φ iff w |!= φ
w |= φ1 ∧ φ2 iff w |= φ1 ∧ w |= φ2
w |= Xφ iff w1 |= φ
w |= φ1 U φ2 iff ∃i ∈ N0 : wi |= φ2 ∧ ∀ 0 ≤ j < i : wj |= φ1

Given an alphabet Σ, an LTL formula φ defines the language L^Σ (φ) = {w ∈ Σ^ω | w |= φ}.

V action-based LTL: w |= a ⇔ a = w(0).

In general, it means that all behaviours of the system satisfy the specification. In state-based LTL setting, it means that a given model M and a given LTL formula φ satisfy L^AP(φ) (M) ⊆ L^2^AP(φ) (φ). (To druhé je jazyk všech běhů, které splňují φ.)
Similarly, in action-based LTL setting, it means that a given model M and a given LTL formula φ satisfy L(M) ⊆ L^Act (φ).

State-based LTL MC je rozhodnutelný pro menší třídu systémů – klade omezení na Petriho sítě i PDA (decidable where validity of atomic propositions depends only on control state and the topmost stack symbol).

Time and space complexity of this algorithm is O(|M| · 2^O(|φ|)), where |M| is the number of states and transitions in the Kripke structure M. The LTL model checking problem is PSPACE-complete.

Pro každou Kripkeho strukturu M = (S, T, I, s0) lze sestrojit Büchi automat A_sys takový, že L_sys = L(A_sys).

Konstrukce Asys: Nechť AP je množina atomických propozic. Pak A_sys = (S, 2^AP, s0, δ, S), kde q ∈ δ(p, a) právě když (p, q) ∈ T ∧ I(p) = a.

1. Formule φ se převede do normální formy.
2. Vypočítá se přechodový graf budoucího automatu.
3. Graf se doplní na zobecněný Büchi automat.
4. Zobecněný BA se převede na standardní Büchi automat.

Řekneme, že LTL formule je v normální formě, pokud neobsahuje operátory F a G a všechny operátory unární negace jsou aplikovány na podformule tvořené pouze atomickou propozicí.

= Syntax =
φ ::= p | ¬p | φ ∨ φ | φ ∧ φ | X φ | φ U φ | φ R φ

= Pravidla pro převod do normální formy =
¬(φ ∨ ψ) ≡ (¬φ) ∧ (¬ψ)
¬(φ ∧ ψ) ≡ (¬φ) ∨ (¬ψ)
¬X φ ≡ X (¬φ)
¬(φ U ψ) ≡ (¬φ R ¬ψ)
¬(φ R ψ) ≡ (¬φ U ¬ψ)

= Zobecněný BA =

• F ⊆ 2^S je systém množin koncových stavů. [F by mělo být takové to kaligrafické F]
• Běh ρ je akceptující, pokud ∀Fi ∈ F platí inf (ρ) ∩ Fi != ∅.
• Dezobecnění:
  • Nechť A = (Σ, S, s, δ, {F1, …, Fn}).
  • B = (Σ, S × {0, …, n}, (s, 0), δ', S × {n}), kde (q, y) ∈ δ'((p, x), a) pokud q ∈ δ(p, a) a pro x a y platí
    • jestliže q ∈ Fi a x = i − 1, tak y = i
    • jestliže x = n, tak y = 0
    • jinak x = y
  • → tzn. inkrementuje se, jak se postupně prochází původně akceptujícími stavy z jednotlivých množin

= Další BA =

• slabý BA (WBA) – každá silně souvislá komponenta obsahuje buď pouze akceptující nebo neakceptující stavy
• terminální BA – každý akceptující cyklus má podobu smyčky nad akceptujícím stavem

A × B = (SA × SB × {0, 1}, Σ, (sA, sB, 0), δ_{A×B}, FA × SB × {0})

(p', q', j) ∈ δ_{A×B} ((p, q, i), a) pro všechna:

• p' ∈ δA (p, a)
• q' ∈ δB (q, a)
• j = (i + 1) mod 2 pokud (i = 0 ∧ p ∈ FA) ∨ (i = 1 ∧ q ∈ FB)
  • → projití akceptujícího stavu z A mě hodí do 1, musím projít ještě akceptujícím stavem z B, abych se dostal zpět na 0, aby se mi průchod přes akceptující stav z A opět započítal
• j = i v ostatních případech

Redukce M |= φ na problém prázdnosti L(A_sys × A¬φ) – původně chceme L(A_sys) ⊆ L(A_φ), což je totéž jako prázdný průnik s komplementem L(φ).

state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, symbolic trajectory evaluation, symbolic execution

• množina stavů = množina binárních vektorů → lze popsat booleovskou fcí
• represents system as a boolean function
• state space search as operations on boolean functions
• Binary Decision Diagrams (BDD; acyklický) are efficient (= deduplikované) ways of representing boolean functions + operations on them

• namísto nad vstupními hodnotami se „počítá“ nad symboly

• Nested DFS – Vnější procedura detekuje akceptující stavy, vnitřní procedura testuje, zda akceptující stav je dosažitelný ze sebe sama (leží na cyklu).
• OWCTY – vrcholy na akceptujícím cyklu jsou dosažitelné z akceptujícího vrcholu & mají 1+ předchůdce
  • Obecně O(|V|^2 + |V||E|), na WBA O(|V| + |E|)
  • Střídají se procedury Reachability (z akceptujících vrcholů) a Elimination (vyhazují nedosažitelné vrcholy + vrcholy bez dosažitelných předchůdců).
• MAP
  • Obecně O(|V|^3 + |V||E|), na WBA O(|V| + |E|)
  • Propagují se maximální akceptující předchůdci (akceptující vrcholy jsou nějak uspořádané) – pokud se propaguje akceptující vrchol do sebe, je na cyklu.

• IA159 Formal Verification Methods
• IV113 Úvod do validace a verifikace