Formalismy pro modelování nekonečně stavových systémů (Petriho sítě, procesové přepisovací systémy, automaty, procesové kalkuly) a algebry procesů, porovnání jejich vyjadřovací síly vzhledem k bisimulaci. Vybrané rozhodnutelné problémy z oblasti verifikace těchto systémů.
Upozornění: bez nároku na úplnost a korektnost. Podle hesla „lepší něco než nic“. Ale snaha byla o co nejlepší výsledek.
Petriho síť je matematická reprezentace struktury distribuovaného systému. Formálně je to trojice N = (P, T, F), kde P ≠ ∅ je konečná množina míst (places), T ≠ ∅ je konečná množina přechodů (transitions) a F je přechodová funkce (float): F: (P × T) ∪ (T × P) → N0
•t = {p ∈ P | F(p, t) > 0} … množina míst, odkud t bere
t• = {p ∈ P | F(t, p) > 0} … množina míst, kam t dává
•p, p• – mn. přechodů, odkud bere/kam dává
Marking (označkování) je fce M: P → N0.
t je připraven (uschopněn) v M, pokud M(p) ≥ F(p, t) pro ∀p ∈ •t. (nebo prostě P) – pokud jich tam je víc, 1 se nedet. vybere, odpálí a přejde se do následnického markingu.
M→M' ⇔ ∃t ∈ T: t je uschopněn v M a M'(p) = M(p) + F(t, p) – F(p, t) pro každé p ∈ P (lze psát M →^t M').
Procesový term nad množinou akcí (a, b, c, …) a procesových konstant (ε, X, Y, …) je definován:
t ::= ε | X | t1 · t2 | t1 || t2
ε je prázdný term.
Procesový přepisovací systém nad konstantami a akcemi je Δ, konečná množina výstupů tvaru t1 →^a t2, kde t1, t2 jsou procesové termy, t1 !≡ ε, a je akce. Je to přechodový systém s návěštími (S, L, R) – stavy, návěští, přechodová relace R ⊂ S × L × S.
1 – termy skládající se z jedné procesové konstanty (např. X)
S – termy skládající se z jedné konstanty nebo sekvenční kompozice konstant (např. X · Y · Z)
P – termy skládající se z jedné konstanty nebo paralelní kompozice konstant (např. X || Y || Z)
G – obecné procesové termy skládající se libovolně ze sekvenčních a paralelních kompozic
→ (α, β)-PRS je systém s třídou α na levé straně a β na pravé, kde β ≥ α. Vzniklé třídy jsou striktní vůči bisimulaci.
(1, 1)-PRS jsou konečné automaty.
(1, S)-PRS jsou BPA (Basic Process Algebra).
(1, P)-PRS jsou BPP (Basic Parallel Proceses).
(1, G)-PRS jsou procesové algebry.
(S, S)-PRS jsou PDA.
(P, P)-PRS jsou Petriho sítě.
All interesting analysis problems for Petri nets are know to be EXPSPACE-hard.
The model-checking problem for BPPs and LTL is EXPSPACE-hard.
Petriho sítě – „Je označkování M' dosažitelné z M v N?“
→ Nechť N = (P, T, F) je S-systém se silně souvislým grafem a nechť pro dvě označkování M, M' platí: Σ[přes p∈P] M(p) = Σ[přes p∈P] M'(p). Potom existuje σ ∈ T* takové, že M →^σ M'.
Petriho sítě – „Je síť N živá pro M0? (Je živý každý její přechod pro M0?)“
→ S-systém N = (P, T, F) s počátečním označkováním M0 je živý právě tehdy, když graf N je silně souvislý a existuje p ∈ P: M0(p) > 0.
Petriho sítě – „Existuje pro (N, M0) dosažitelné označkování M takové, že (N, M) je mrtvá, tj. není připraven žádný přechod?“