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 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).

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. Herní sémantika μ-kalkulu souvisí s hrami dvou hráčů s úplnou informací, zejména s nekonečnými paritovými hrami.

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 $\varphi$ a $\psi$ formule, potom $\varphi \wedge \psi$ je formule;
• je-li $\varphi$ formule, potom $\mathrm{\neg }\varphi$ je formule;
• je-li $\varphi$ je formule a $a$ je akce, potom $[a]\varphi$ je formule; (vyslovuje se buď: $a$ box $\varphi$ nebo po $a$ nutně $\varphi$)
• je-li $\varphi$ formule a $Z$ proměnná $\nu Z.\varphi$ je formule, za předpokladu, že každý volný výskyt $Z$ ve $\varphi$ 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 $\nu$ je jediným vázacím operátorem.)

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

• $\varphi \vee \psi$ znamenající $\mathrm{\neg }(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$
• $⟨a⟩\varphi$ (vyslovuje se buď $a$ diamant $\varphi$, nebo po $a$ možná $\varphi$) znamenající $\mathrm{\neg }[a]\mathrm{\neg }\varphi$
• $\mu Z.\varphi$ znamenající $\mathrm{\neg }\nu Z.\mathrm{\neg }\varphi [Z:=\mathrm{\neg }Z]$, kde $\varphi [Z:=\mathrm{\neg }Z]$ značí substituci $\mathrm{\neg }Z$ za $Z$ ve všech volných výskytech $Z$ ve $\varphi$ .

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

Notace $\mu Z.\varphi$ (a opak tohoto) jsou inspirovány lambda kalkulem. Záměrem je označit nejmenší (a respektive největší) pevný bod formule $\varphi$ kde "minimalizace" či "maximalizace" jsou v proměnné $Z$, podobně jako v lambda kalkulu $\lambda Z.\varphi$ je funkce se vzorcem $\varphi$ ve vázané proměnné $Z$. 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 $(S,R,V)$ kde:

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

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

• $[[p]{]}_i=V(p)$ ;
• $[[Z]{]}_i=i(Z)$ ;
• $[[\varphi \wedge \psi ]{]}_i=[[\varphi ]{]}_i\cap [[\psi ]{]}_i$ ;
• $[[\mathrm{\neg }\varphi ]{]}_i=S\setminus [[\varphi ]{]}_i$ ;
• $[[[a]\varphi ]{]}_i=\{s\in S\mid \mathrm{\forall }t\in S,(s,t)\in R_a\to t\in [[\varphi ]{]}_i\}$ ;
• $[[\nu Z.\varphi ]{]}_i=\bigcup \{T\subseteq S\mid T\subseteq [[\varphi ]{]}_{i[Z:=T]}\}$, kde $i[Z:=T]$ mapuje $Z$ na $T$ při zachování mapování $i$ všude jinde.

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

• $[[\varphi \vee \psi ]{]}_i=[[\varphi ]{]}_i\cup [[\psi ]{]}_i$ ;
• $[[⟨a⟩\varphi ]{]}_i=\{s\in S\mid \mathrm{\exists }t\in S,(s,t)\in R_a\wedge t\in [[\varphi ]{]}_i\}$ ;
• $[[\mu Z.\varphi ]{]}_i=\bigcap \{T\subseteq S\mid [[\varphi ]{]}_{i[Z:=T]}\subseteq T\}$

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

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

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

Příklady

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

Problémy s rozhodnutelností

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

Odkazy

Literatura

• Šablona:Cite book
• Šablona:Cite book
• Šablona:Cite book

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