===== Zadání =====
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.

===== Vypracování =====
**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.

==== LTL ====
φ ::= 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).

=== Model checking pro LTL ===
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.

==== Princip překladu LTL na automaty nad nekonečnými slovy ====

=== Překlad Kripkeho struktury ===
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.

=== Převod LTL na BA ===
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.

== Normální forma LTL ==
Ř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

== Konstrukce A × B ==
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(φ).

==== Algoritmy ====
<del>state space enumeration, symbolic state space enumeration,</del> abstract interpretation, <del>symbolic simulation, symbolic trajectory evaluation,</del> symbolic execution

=== Symbolic MC ===
  * 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

== Symbolická exekuce ==
  * namísto nad vstupními hodnotami se „počítá“ nad symboly

=== Explicitní algoritmy ===
  * 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.


===== Předměty =====
  * [[https://is.muni.cz/auth/predmet/fi/IA159|IA159 Formal Verification Methods]]
  * [[https://is.muni.cz/auth/predmet/fi/IV113|IV113 Úvod do validace a verifikace]]

===== Související otázky =====


~~DISCUSSION~~