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 editovat

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

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

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

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

Notace $\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 $\phi$ kde "minimalizace" či "maximalizace" jsou v proměnné $Z$ , podobně jako v lambda kalkulu $\lambda Z.\phi$ je funkce se vzorcem $\phi$ ve vázané proměnné $Z$ .^[5] Podrobnosti viz denotační sémantika níže.

Denotační sémantika editovat

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}:\phi \to 2^{S}$ , je funkce definovaná následujícími pravidly:

$[\![p]\!]_{i}=V(p)$ ;
$[\![Z]\!]_{i}=i(Z)$ ;
$[\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}$ ;
$[\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}$ ;
$[\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}$ ;
$[\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{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:

$[\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}$ ;
$[\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}$ ;
$[\![\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ů $(S,R,V)$ :

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

Interpretace formulí $[a]\phi$ a $\langle a\rangle \phi$ 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é.^[6]

Příklady editovat

$\nu Z.\phi \wedge [a]Z$ se vykládá jako " $\phi$ je platná pro každou cestu."^[6] Myšlenka je taková, že " $\phi$ je pravdivá podél každé cesty z akcí" lze definovat axiomaticky jako (nejslabší) větu $Z$ která implikuje $\phi$ a která zůstane pravdivá po zpracování jakéhokoli a-označení.^[7]
$\mu Z.\phi \vee \langle a\rangle Z$ se interpretuje jako existence cesty podél a-přechodů do stavu, kde $\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] $\nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)$

Problémy s rozhodnutelností editovat

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 editovat

Reference editovat

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

↑ In: [s.l.]: [s.n.] ISBN 978-3-540-11576-2. DOI 10.1007/BFb0012782.
↑ Clarke p.108, Theorem 6; Emerson p. 196
↑ Arnold and Niwiński, pp. viii-x and chapter 6
↑ Arnold and Niwiński, pp. viii-x and chapter 4
↑ Arnold and Niwiński, p. 14
↑ ^a ^b Bradfield and Stirling, p. 731
↑ Bradfield and Stirling, p. 6
↑ ^a ^b Leonid Libkin. [s.l.]: [s.n.] Dostupné online. ISBN 978-3-540-00428-8.
↑ ; Klaus Schneider. [s.l.]: [s.n.] Dostupné online. ISBN 978-3-540-00296-3.
↑ Chybí název periodika!
↑ [s.l.]: [s.n.] ISBN 0897912527. DOI 10.1145/73560.73582.

Literatura editovat

CLARKE, Edmund M. Jr.; ORNA GRUMBERG; DORON A. PELED. Model Checking. Cambridge, Massachusetts, USA: MIT press, 1999. ISBN 0-262-03270-8.
STIRLING, Colin. Modal and Temporal Properties of Processes. New York, Berlin, Heidelberg: Springer Verlag, 2001. ISBN 0-387-98717-7.
André Arnold; DAMIAN NIWIŃSKI. Rudiments of μ-Calculus. [s.l.]: Elsevier, 2001. ISBN 978-0-444-50620-7.

Související články editovat

Externí odkazy editovat

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

[Kozen1982-1] In: [s.l.]: [s.n.] ISBN 978-3-540-11576-2. DOI 10.1007/BFb0012782.

[2] Clarke p.108, Theorem 6; Emerson p. 196

[3] Arnold and Niwiński, pp. viii-x and chapter 6

[4] Arnold and Niwiński, pp. viii-x and chapter 4

[5] Arnold and Niwiński, p. 14

[Bradfield_and_Stirling,_p._731-6] Bradfield and Stirling, p. 731

[7] Bradfield and Stirling, p. 6

[GrädelKolaitis2007-8] Leonid Libkin. [s.l.]: [s.n.] Dostupné online. ISBN 978-3-540-00428-8.

[Schneider2004-9] ; Klaus Schneider. [s.l.]: [s.n.] Dostupné online. ISBN 978-3-540-00296-3.

[10] Chybí název periodika!

[11] [s.l.]: [s.n.] ISBN 0897912527. DOI 10.1145/73560.73582.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]