Rachunek Mu

W logice matematycznej i informatyki teoretycznej , mu-rachunek (lub logiki modalnej mu-rachunek ) jest rozszerzenie klasycznej logiki modalnej z punktów stacjonarnych operatorów . Według Bradfielda i Walukiewicza mu-rachunek jest jedną z najważniejszych logik weryfikacji modeli; jest wyrazisty, a jednocześnie ma dobre właściwości algorytmiczne.

Rachunek Mu ( zdaniowy i modalny ) został po raz pierwszy wprowadzony przez Dana Scotta i Jaco de Bakkera, a następnie rozszerzony w jego nowoczesnej wersji przez Dextera Kozen . Ta logika umożliwia opisanie właściwości układów przejść stanów i ich weryfikację. Wiele logik czasowych (takich jak CTL * lub jego szeroko stosowane fragmenty, takie jak CTL (en) lub LTL ) to fragmenty mu-rachunku.

Algebraiczny sposób patrzenia na rachunek mu jest traktowany jako algebra funkcji monotonicznych w całej sieci , gdzie operatory są kompozycją funkcjonalną i punktami stałymi; Z tego punktu widzenia, Mu-rachunek działa na siatce o zadanej Algebra . W semantyka mu-nazębnego gier są połączone do dwóch graczy gier z doskonałej informacji, w szczególności gra parzystości .

Składnia

Niech dwa zestawy symboli P (propozycji) i A (działań) i V będzie nieskończony przeliczalny zbiór zmiennych. Zbiór wzorów mu-rachunku (zdaniowego i modalnego) definiuje się indukcyjnie następująco:

każda propozycja jest formułą;

każda zmienna jest formułą;

jeśli i są formułami, to jest formułą; $\ phi$ $\ psi$ ${\ Displaystyle (\ phi \ wedge \ psi)}$

jeśli jest formułą, to jest formułą; $\ phi$ ${\ displaystyle \ neg \ phi}$

jeśli jest formułą i jest działaniem, to jest formułą (jest to formuła: „po , koniecznie ”); $\ phi$ $w$ ${\ displaystyle [a] \ phi}$ $w$ $\ phi$

jeśli jest formułą i zmienną, to jest formułą zakładającą, że każde wystąpienie w pojawia się dodatnio, to znaczy jest parzystą liczbę razy. $\ phi$ $Z$ ${\ Displaystyle \ nu Z. \ phi}$ $Z$ $\ phi$

Pojęcia zmiennych ograniczonych lub dowolnych są definiowane jak zwykle z who jest jedynym operatorem wiążącym zmienną. $\nagi$

Mając powyższe definicje, możemy dodać jako cukier syntaktyczny :

${\ Displaystyle \ phi \ lor \ psi}$ znaczący ; ${\ displaystyle \ neg (\ neg \ phi \ land \ neg \ psi)}$

${\ displaystyle \ langle a \ rangle \ phi}$ signifier (po tym, jak jest to możliwe ); ${\ displaystyle \ neg [a] \ neg \ phi}$ $w$ $\ phi$

${\ displaystyle \ mu Z. \ phi}$ signifier , gdzie oznacza, że zastępujemy przez dla każdego swobodnego wystąpienia w . ${\ Displaystyle \ neg \ nu Z. \ neg \ phi [Z: = \ neg Z]}$ ${\ Displaystyle \ phi [Z: = \ neg Z]}$ $Z$ ${\ displaystyle \ neg Z}$ $Z$ $\ phi$

Dwa pierwsze są znane formuły rachunku i modalnej logicznego K .

Notacja (i odpowiednio jej podwójna ) jest inspirowana rachunkiem lambda ; celem jest oznaczenie najmniejszego (odpowiednio największego) stałego punktu w zmiennej Z wyrażenia, tak jak w rachunku lambda jest funkcją wzoru w zmiennej ograniczonej Z ; zobacz semantykę denotacyjną poniżej, aby uzyskać więcej informacji. ${\ displaystyle \ mu Z. \ phi}$ ${\ Displaystyle \ nu Z. \ phi}$ $\ phi$ ${\ Displaystyle \ lambda Z. \ phi}$ $\ phi$

Semantyka denotacyjna

Modele wzoru mu-rachunku (zdaniowego, modalnego) podano jako układy przejść stanów , w których: ${\ Displaystyle (S, R, V)}$

$S$ jest zbiorem stanów;

$R$ kojarzy z każdą etykietą relację binarną ; $w$ $S$

${\ Displaystyle V: P \ rightarrow 2 ^ {S}}$ kojarzy z każdym zdaniem zbiór stanów, w których zdanie jest prawdziwe. ${\ displaystyle p \ in P}$

Mając system przejść , interpretacja wiąże podzbiór stanów z dowolną zmienną . Podzbiór stanów definiujemy za pomocą indukcji strukturalnej według wzoru : ${\ Displaystyle (S, R, V)}$ $ja$ $Z$ ${\ displaystyle i (Z)}$ ${\ Displaystyle [\! [{\ podkreślenie {\ phi}}] \!] _ {i}}$ $\ phi$

${\ Displaystyle [\! [p] \!] _ {i} = V (p)}$ ;
${\ Displaystyle [\! [Z] \!] _ {i} = ja (Z)}$ ;
${\ Displaystyle [\! [\ phi \ wedge \ psi] \!] _ {i} = [\! [\ phi] \!] _ {i} \ czapka [\! [\ psi] \!] _ { ja}}$ ;
${\ 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]} \}}$ , gdzie łączy się z , zachowując skojarzenia z innych miejsc. ${\ displaystyle i [Z: = T]}$ $Z$ $T$ $ja$

Zgodnie z dwoistością, interpretacja innych podstawowych formuł jest następująca:

${\ Displaystyle [\! [\ phi \ vee \ psi] \!] _ {i} = [\! [\ phi] \!] _ {i} \ filiżanka [\! [\ psi] \!] _ { ja}}$ ;
${\ Displaystyle [\! [\ langle a \ rangle \ phi] \!] _ {i} = \ {s \ w S \ mid \ istnieje t \ w S, (s, t) \ w R_ {a} \ klin t \ in [\! [\ phi] \!] _ {i} \}}$ ;
${\ Displaystyle [\! [\ mu Z. \ phi] \!] _ {i} = \ bigcap \ {T \ subseteq S \ mid [\! [\ phi] \!] _ {i [Z: = T ]} \ subseteq T \}}$ .

Nieformalnie, w przypadku systemu przejściowego : ${\ Displaystyle (S, R, V)}$

$p$ jest prawdziwe dla stanów ; ${\ Displaystyle V (p)}$

${\ Displaystyle \ phi \ wedge \ psi}$ jest prawdziwe, jeśli i są prawdziwe; $\ phi$ $\ psi$

${\ displaystyle \ neg \ phi}$ jest prawdą, jeśli nie jest prawdą; $\ phi$

${\ displaystyle [a] \ phi}$ jest prawdziwe w stanie, jeśli wszystkie wychodzące przejścia od prowadzą do stanu, w którym są prawdziwe; $s$ $w$ $s$ $\ phi$

${\ displaystyle \ langle a \ rangle \ phi}$ jest prawdziwe w stanie, jeśli jest przynajmniej jedno przejście z tego stanu, które prowadzi do stanu, w którym jest prawdziwe; $s$ $w$ $s$ $\ phi$

${\ Displaystyle \ nu Z. \ phi}$ jest prawdziwe w każdym stanie dowolnego zbioru, takim, że jeśli zmienna zostanie zastąpiona przez , to jest prawdziwa dla wszystkich (z twierdzenia Knastera-Tarskiego wnioskujemy , że jest to największy stały punkt i przez jest najmniejszy). $T$ $Z$ $T$ $\ phi$ $T$ ${\ Displaystyle [\! [\ nu Z. \ phi] \!] _ {i}}$ ${\ Displaystyle [\! [\ phi] \!] _ {i [Z: = T]}}$ ${\ Displaystyle [\! [\ mu Z. \ phi] \!] _ {i}}$

Interpretacja i jest „klasyczną” interpretacją logiki dynamicznej . Ponadto może być postrzegane jako właściwość żywotności („coś dobrego dzieje się na raz”), podczas gdy jest postrzegane jako właściwość bezpieczeństwa („coś złego nigdy się nie dzieje”) w nieformalnej klasyfikacji Lesliego . ${\ displaystyle [a] \ phi}$ ${\ displaystyle \ langle a \ rangle \ phi}$ $\ mu$ $\nagi$

Przykłady

${\ Displaystyle \ nu Z. \ phi \ klin [a] Z}$ jest interpretowany jako „ jest prawdziwe dla każdej ścieżki A ”. $\ phi$

${\ displaystyle \ mu Z. \ phi \ vee \ langle a \ rangle Z}$ interpretowana jest jako istnienie ścieżki przemian a do stanu, w którym jest prawdą. $\ phi$

Właściwość systemu polegająca na tym, że nie blokuje się, to znaczy, że z dowolnego stanu dostępnego następuje przejście wychodzące, można wyrazić wzorem . ${\ Displaystyle \ nu Z. (\ bigvee _ {a \ w A} \ langle a \ rangle \ top \ wedge \ bigwedge _ {a \ in A} [a] Z)}$
${\ displaystyle \ mu Z. [a] Z}$ : Każda ścieżka składa się z ciągu -transitions jest zakończona.
${\ displaystyle \ nu Z. \ langle a \ rangle Z}$ : istnieje nieskończona ścieżka złożona z przejść- a .
${\ displaystyle \ nu Z. \ phi \ land \ langle a \ rangle Z}$ : Istnieje nieskończona droga składa się z ciągu -transitions wzdłuż której jest prawda cały czas. $\ phi$

Alternacja

Przemienność mniejszych i większych punktów stałych nazywana jest przemienną głębokością. Możemy policzyć liczbę przemian, ale generalnie używamy bardziej wyrafinowanej definicji wprowadzonej przez Damiana Niwińskiego, który również przygląda się zastosowaniu zmiennych. Hierarchia naprzemienności jest ścisła.

Problemy algorytmiczne

Problem sprawdzania modelu mu-rachunku jest w NP inter co-NP i jest P- dur. Algorytm sprawdzania modelu mu-rachunek jest następujący:

Zbuduj grę z parzystością z systemu przejść i wzoru mu-rachunku do weryfikacji;
Rozwiąż grę z parzystością.

MU rachunek problemem spełnialności jest EXPTIME uzupełniania .

Podobnie jak w przypadku liniowej logiki czasowej (LTL), problem weryfikacji modelu , spełnialności i trafności liniowego rachunku mu jest zakończony PSPACE .

Dyskusje

Oryginalna składnia mu-rachunku była wektorowa. Zaletą tego zapisu jest to, że umożliwia współdzielenie zmiennych w kilku formułach podrzędnych. Istnieje liniowa wersja (niepołączona) mu-rachunku.

Bibliografia

(en) Edmund M. Clarke, Jr. , Orna Grumberg i Doron A. Peled, Model Checking , Cambridge, Massachusetts, USA, MIT press,1999( ISBN 0-262-03270-8 ), rozdział 7, Sprawdzanie modelu pod kątem rachunku μ, s. 97–108
(en) Colin Stirling , Modal and Temporal Properties of Processes , Nowy Jork, Berlin, Heidelberg, Springer Verlag,2001, 191 s. ( ISBN 0-387-98717-7 , czytaj online ), rozdział 5, rachunek modalny μ, s. 103-128
(en) André Arnold i Damian Niwiński, Rudiments of μ-Calculus , Elsevier ,2001, 277 s. ( ISBN 978-0-444-50620-7 ), rozdział 6, Rachunek μ nad algebrami potęgowymi, s. 141-153 dotyczy rachunku μ.
Yde Venema (2008) Wykłady o modalnym rachunku μ ; został zaprezentowany na 18. Europejskiej Letniej Szkole Logiki, Języka i Informacji.
(en) Julian Bradfield i Colin Stirling, The Handbook of Modal Logic , Elsevier ,2006, 721–756 s. ( czytaj online ) , „Modalne rachunki mu”
(en) E. Allen Emerson (1996). „Sprawdzanie modeli i rachunek Mu”. Złożoność opisowa i modele skończone : 185–214 str., American Mathematical Society .
(en) Kozen, Dexter, „ Results on the propositional μ-Calculus ” , Theoretical Computer Science , vol. 27 N O 3,1983, s. 333–354 ( DOI 10.1016 / 0304-3975 (82) 90125-6 )

Linki zewnętrzne

Sophie Pinchinat, Logic, Automata & Games nagranie wideo z wykładu w ANU Logic Summer School '09

Uwagi i odniesienia

(w) Julian Bradfield i Igor Walukiewicz , "The mu-calculator and Model Checking" , w Handbook of Model Checking , Springer International Publishing,2018( ISBN 9783319105741 , DOI 10.1007 / 978-3-319-10575-8_26 , czytaj online ) , s. 871–919
André Arnold i Damian Niwiński, Podstawy μ-Calculus , str. VIII-X i rozdział 6.
André Arnold i Damian Niwiński, Podstawy μ-Calculus , str. VIII-X i rozdział 4.
André Arnold i Damian Niwiński, Podstawy μ-Calculus , str. 14.
Julian Bradfield i Colin Stirling, Handbook of logiki modalnej , s. 731.
(en) Erich Grädel, Phokion G. Kolaitis, Leonid Libkin , Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema i Scott Weinstein, Finite Model Theory and Its Applications , Springer,2007, 437 s. ( ISBN 978-3-540-00428-8 , czytaj online ) , str. 159.
„ Kurs rachunku różniczkowego mu w Labri ” .
(w) Damian Niwinski , " We fixed-point clones " , Automata, Languages and Programming , Springer, Berlin, Heidelberg, przeczytaj Notes in Computer Science,15 lipca 1986, s. 464-473 ( ISBN 3540167617 , DOI 10.1007 / 3-540-16761-7_96 , czytaj online , dostęp 12 marca 2018 )
(w) JC Bradfield , " The modal mu- calcus is strict alternation hierarchy " , CONCUR '96 Concurrency Theory , Springer, Berlin, Heidelberg, przeczytaj Uwagi w informatyce,26 sierpnia 1996, s. 233-246 ( ISBN 3540616047 , DOI 10.1007 / 3-540-61604-7_58 , czytaj online , dostęp 12 marca 2018 )
(w) Klaus Schneider, Weryfikacja systemów reaktywnych: metody formalne i algorytmy , Springer,2004, 602 str. ( ISBN 978-3-540-00296-3 , czytaj online ) , str. 521.
(w) AP Sistla i EM Clarke , " The Complexity of Propositional Linear Temporal Logics " , J. ACM , tom. 32, n o 3,1 st lipca 1985, s. 733–749 ( ISSN 0004-5411 , DOI 10.1145 / 3828.3837 , czytaj online ).
(en) MY Vardi , „ A Temporal Fixpoint Calculus ” , ACM , Nowy Jork, NY, USA,1 st styczeń 1988, s. 250–259 ( ISBN 0897912527 , DOI 10.1145 / 73560.73582 , czytaj online ).
Julian Bradfield i Igor Walukiewicz , Mu-rachunek i sprawdzanie modeli ( czytaj online )
Howard Barringer , Ruurd Kuiper i Amir Pnueli , „ Naprawdę abstrakcyjny model współbieżny i jego logika czasowa ”, POPL 'x86 Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages , ACM,1986, s. 173-183 ( DOI 10.1145 / 512644.512660 , odczyt online , dostęp 12 marca 2018 )

(en) Ten artykuł jest częściowo lub w całości zaczerpnięty z artykułu w Wikipedii w języku angielskim zatytułowanego „ Modal μ-calculator ” ( zobacz listę autorów ) .