Modální μ-kalkulus

V teoretické informatice modální μ-kalkulus (Lμ, L _μ, někdy jen μ-kalkulus) označuje rozšíření výrokové modální logiky (s více modalitami). Toho je dosaženo přidáním operátoru s nejmenším pevným bodem μ a operátoru s největším pevným bodem ν. Jde tedy o logiku pevného bodu.

μ-kalkul vytvořili Dany Scotta a Jaca de Bakkera a dále jej rozvinul Dexter Kozen^[1] do dnes nejpoužívanější formy. Využívá se k popisu vlastností značených přechodových systémů a k verifikaci těchto vlastností. V μ-kalkulu lze zapsat mnoho jiných temporálních logik, včetně CTL* a dalších jeho používaných fragmentů — lineární temporální logiky (LTL) a výpočetní stromové logiky (CTL).^[2]

Algebraický pohled říká, že se jedná o algebru monotónních funkcí nad úplným svazem, s operátory sestávajících ze skládání funkcí a nejmenšími a největšími fixními bodovýmy operátory; z tohoto hlediska je modální μ-kalkulus nad svazem potenčně množinové algebry.^[3] Herní sémantika μ-kalkulu souvisí s hrami dvou hráčů s úplnou informací, zejména s nekonečnými paritovými hrami.^[4]

Syntax

Nechť P (množina výroků) a A (množina akcí) jsou dvě konečné množiny symbolů a nechť Var je spočetně nekonečná množina proměnných. Množina formulí (výrokového, modálního) μ-kalkulu je definován následovně:

• každý výrok a každá proměnná je formule;
• jsou-li ${\displaystyle \phi }$ a ${\displaystyle \psi }$ formule, potom ${\displaystyle \phi \wedge \psi }$ je formule;
• je-li ${\displaystyle \phi }$ formule, potom ${\displaystyle \neg \phi }$ je formule;
• je-li ${\displaystyle \phi }$ je formule a ${\displaystyle a}$ je akce, potom ${\displaystyle [a]\phi }$ je formule; (vyslovuje se buď: ${\displaystyle a}$ box ${\displaystyle \phi }$ nebo po ${\displaystyle a}$ nutně ${\displaystyle \phi }$)
• je-li ${\displaystyle \phi }$ formule a ${\displaystyle Z}$ proměnná ${\displaystyle \nu Z.\phi }$ je formule, za předpokladu, že každý volný výskyt ${\displaystyle Z}$ ve ${\displaystyle \phi }$ se vyskytuje pozitivně, tj. v rámci sudého počtu negací.

(Pojmy volné a vázané proměnné jsou míněny standardně, kde ${\displaystyle \nu }$ je jediným vázacím operátorem.)

Vzhledem k výše uvedeným definicím můžeme syntaxi obohatit o:

• ${\displaystyle \phi \lor \psi }$ znamenající ${\displaystyle \neg (\neg \phi \land \neg \psi )}$
• ${\displaystyle \langle a\rangle \phi }$ (vyslovuje se buď ${\displaystyle a}$ diamant ${\displaystyle \phi }$, nebo po ${\displaystyle a}$ možná ${\displaystyle \phi }$) znamenající ${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$ znamenající ${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}$, kde ${\displaystyle \phi [Z:=\neg Z]}$ značí substituci ${\displaystyle \neg Z}$ za ${\displaystyle Z}$ ve všech volných výskytech ${\displaystyle Z}$ ve ${\displaystyle \phi }$ .

První dvě formule jsou známé z klasického výrokového počtu, respektive minimální multimodální logiky K.

Notace ${\displaystyle \mu Z.\phi }$ (a opak tohoto) jsou inspirovány lambda kalkulem. Záměrem je označit nejmenší (a respektive největší) pevný bod formule ${\displaystyle \phi }$ kde "minimalizace" či "maximalizace" jsou v proměnné ${\displaystyle Z}$, podobně jako v lambda kalkulu ${\displaystyle \lambda Z.\phi }$ je funkce se vzorcem ${\displaystyle \phi }$ ve vázané proměnné ${\displaystyle Z}$.^[5] Podrobnosti viz denotační sémantika níže.

Denotační sémantika

Modely modálního μ-kalkulu jsou dány jako označované přechodové systémy ${\displaystyle (S,R,V)}$ kde:

• ${\displaystyle S}$ je množina stavů;
• ${\displaystyle R}$ mapuje ke každému štítku ${\displaystyle a}$ binární relaci na ${\displaystyle S}$ ;
• ${\displaystyle V:P\to 2^{S}}$, mapuje každý výrok ${\displaystyle p\in P}$ k množině stavů, kde je tvrzení pravdivé.

Vzhledem k označenému přechodovému systému ${\displaystyle (S,R,V)}$ a interpretaci ${\displaystyle i}$ proměnných ${\displaystyle Z}$ ${\displaystyle \mu }$-kalkulu, ${\displaystyle [\![\cdot ]\!]_{i}:\phi \to 2^{S}}$, je funkce definovaná následujícími pravidly:

• ${\displaystyle [\![p]\!]_{i}=V(p)}$ ;
• ${\displaystyle [\![Z]\!]_{i}=i(Z)}$ ;
• ${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}}$ ;
• ${\displaystyle [\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}}$ ;
• ${\displaystyle [\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}}$ ;
• ${\displaystyle [\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}}$, kde ${\displaystyle i[Z:=T]}$ mapuje ${\displaystyle Z}$ na ${\displaystyle T}$ při zachování mapování ${\displaystyle i}$ všude jinde.

Z důvodu duality, interpretace ostatních základních formulí je dána:

• ${\displaystyle [\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}}$ ;
• ${\displaystyle [\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}}$ ;
• ${\displaystyle [\![\mu Z.\phi ]\!]_{i}=\bigcap \{T\subseteq S\mid [\![\phi ]\!]_{i[Z:=T]}\subseteq T\}}$

Méně formálně, toto znamená, že pro daný systém přechodů ${\displaystyle (S,R,V)}$ :

• ${\displaystyle p}$ platí v množině stavů ${\displaystyle V(p)}$ ;
• ${\displaystyle \phi \wedge \psi }$ platí v každém stavu, kde ${\displaystyle \phi }$ a ${\displaystyle \psi }$ oba platí;
• ${\displaystyle \neg \phi }$ platí v každém stavu, kde ${\displaystyle \phi }$ neplatí.
• ${\displaystyle [a]\phi }$ platí ve stavu ${\displaystyle s}$ pokud každý ${\displaystyle a}$-přechod vedoucí ven z ${\displaystyle s}$ vede do stavu, kde ${\displaystyle \phi }$ platí.
• ${\displaystyle \langle a\rangle \phi }$ platí ve stavu ${\displaystyle s}$ pokud existuje ${\displaystyle a}$-přechod vedoucí ven z ${\displaystyle s}$, který vede ke stavu, kdy ${\displaystyle \phi }$ platí.
• ${\displaystyle \nu Z.\phi }$ platí v libovolném stavu v libovolné množině ${\displaystyle T}$ tak, že když proměnná ${\displaystyle Z}$ je nastaveno na ${\displaystyle T}$, pak ${\displaystyle \phi }$ platí pro všechny ${\displaystyle T}$ . (Z Knaster-Tarského věty vyplývá, že ${\displaystyle [\![\nu Z.\phi ]\!]_{i}}$ je největším pevným bodem ${\displaystyle T\mapsto [\![\phi ]\!]_{i[Z:=T]}}$, a ${\displaystyle [\![\mu Z.\phi ]\!]_{i}}$ jeho nejmenší pevný bod.)

Interpretace formulí ${\displaystyle [a]\phi }$ a ${\displaystyle \langle a\rangle \phi }$ jsou de-facto ony "klasické" z dynamické logiky. Navíc operátor ${\displaystyle \mu }$ lze vyjádřit jako živost („něco dobrého se někdy stane“) a ${\displaystyle \nu }$ jako bezpečnost ("nic špatného se nikdy nestane") v neformální klasifikaci dle Leslie Lamportové.^[6]

Příklady

• ${\displaystyle \nu Z.\phi \wedge [a]Z}$ se vykládá jako "${\displaystyle \phi }$ je platná pro každou cestu."^[6] Myšlenka je taková, že "${\displaystyle \phi }$ je pravdivá podél každé cesty z akcí" lze definovat axiomaticky jako (nejslabší) větu ${\displaystyle Z}$ která implikuje ${\displaystyle \phi }$ a která zůstane pravdivá po zpracování jakéhokoli a-označení.^[7]
• ${\displaystyle \mu Z.\phi \vee \langle a\rangle Z}$ se interpretuje jako existence cesty podél a-přechodů do stavu, kde ${\displaystyle \phi }$ platí.^[8]
• Vlastnost stavu bez deadlocku, což znamená, že žádná cesta z tohoto stavu nedosáhne slepé uličky, je vyjádřena formulí^[8] $${\displaystyle \nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)}$$

Problémy s rozhodnutelností

Splnitelnost modálního formule μ-kalkulu je EXPTIME-úplná.^[9] Stejně jako pro lineární temporální logiku (LTL)^[10] jsou model checkingu, splnitelnosti a platnosti lineárního modálního μ-kalkulu PSPACE-úplné.^[11]

Odkazy

Reference

V tomto článku byl použit překlad textu z článku Modal μ-calculus na anglické Wikipedii.

Literatura

• CLARKE, Edmund M. Jr.; ORNA GRUMBERG; DORON A. PELED. Model Checking. Cambridge, Massachusetts, USA: MIT press, 1999. ISBN 0-262-03270-8. Je zde použita šablona {{Cite book}} označená jako k „pouze dočasnému použití“.
• STIRLING, Colin. Modal and Temporal Properties of Processes. New York, Berlin, Heidelberg: Springer Verlag, 2001. ISBN 0-387-98717-7. Je zde použita šablona {{Cite book}} označená jako k „pouze dočasnému použití“.
• André Arnold; DAMIAN NIWIŃSKI. Rudiments of μ-Calculus. [s.l.]: Elsevier, 2001. ISBN 978-0-444-50620-7. Je zde použita šablona {{Cite book}} označená jako k „pouze dočasnému použití“.

Související články

• Teorie konečných modelů
• Modální μ-kalkul bez alternace

Externí odkazy

• Sophie Pinchinat, Logic, Automata & Games video záznam přednášky na ANU Logic Summer School '09