Mu-kalkki

Vuonna matemaattinen logiikka ja teoreettisen tietojenkäsittelyopin , mu-hammaskivi (tai logiikkaa modaalilajit mu-hammaskiven ) on laajentaa klassisen modaalilogiikan kanssa kiintopisteen operaattoreiden . Bradfieldin ja Walukiewiczin mukaan mu-calculus on yksi tärkeimmistä logiikoista mallien todentamiseksi; se on ilmeikäs ja sillä on hyvät algoritmiset ominaisuudet.

Dana Scott ja Jaco de Bakker esittivät Mu-calculuksen ( propositionaalisen ja modaalisen ) ensin ja sitten Dexter Kozen laajensi sen modernissa versiossa . Tämän logiikan avulla voidaan kuvata tilasiirtymäjärjestelmien ominaisuuksia ja tarkistaa ne. Monet ajalliset logiikat (kuten CTL * tai sen laajalti käytetyt fragmentit, kuten CTL (en) tai LTL ) ovat mu-calculuksen fragmentteja.

Algebrallinen tapa tarkastella MU-laskenta on ajatella sitä algebran on monotoninen funktio yli täydellinen ristikko , operaattorit ollessa toiminnallinen koostumus ja kiinteä pistettä; Tästä näkökulmasta, mu-hammaskiven vaikuttaa ristikko on asetettu algebran . Semantiikka mu-hammaskiven pelejä sidoksissa kahteen pelaajan pelien täydellinen tiedot, erityisesti tasa-pelejä .

Syntaksi

Anna kaksi symbolin P (jäljempänä ehdotuksia) ja (toimet) ja V on ääretön numeroituvia joukko muuttujia. Mu-calculus-kaavojen joukko (propositionaalinen ja modaalinen) määritellään induktiivisesti seuraavasti:

kukin ehdotus on kaava;

kukin muuttuja on kaava;

jos ja ovat kaavoja, niin on kaava; $\ phi$ $\ psi$ ${\ displaystyle (\ phi \ wedge \ psi)}$

jos on kaava, niin on kaava; $\ phi$ ${\ displaystyle \ neg \ phi}$

jos on kaava ja on toiminta, niin on kaava (se on kaava: "jälkeen , välttämättä "); $\ phi$ $klo$ ${\ displaystyle [a] \ phi}$ $klo$ $\ phi$

jos on kaava ja vaihteleva, niin on kaava olettaen, että kussakin tapauksessa on näyttöön tulee positiivisesti, että on, se on alhaalla parillinen määrä kertoja. $\ phi$ $Z$ ${\ displaystyle \ nu Z. \ phi}$ $Z$ $\ phi$

Sidottujen tai vapaiden muuttujien käsitteet määritellään siten, että yleensä kuka on ainoa muuttujaa sitova operaattori. $\alasti$

Yllä olevien määritelmien avulla voimme lisätä syntaktisena sokerina :

${\ displaystyle \ phi \ lor \ psi}$ merkitsijä ; ${\ displaystyle \ neg (\ neg \ phi \ land \ neg \ psi)}$

${\ displaystyle \ langle a \ rangle \ phi}$ merkitsijä (kun se on mahdollista ); ${\ displaystyle \ neg [a] \ neg \ phi}$ $klo$ $\ phi$

${\ displaystyle \ mu Z. \ phi}$ signifier , missä tarkoittaa, että me korvata mennessä jokaista ilmaiseksi esiintyminen vuonna . ${\ displaystyle \ neg \ nu Z. \ neg \ phi [Z: = \ neg Z]}$ ${\ displaystyle \ phi [Z: = \ neg Z]}$ $Z$ ${\ displaystyle \ neg Z}$ $Z$ $\ phi$

Kaksi ensimmäistä ovat tuttuja kaavat hammaskiven ja modaalilogiikan K .

Merkinnät (ja vastaavasti niiden kaksoisolosuhteet ) on innoittamana lambda-laskelmasta ; tavoitteena on tarkoittamaan pienin (vastaavasti suurin) kiinteän pisteen muuttuja Z ilmaisun kuten lambda-hammaskiven on funktio, jolla on kaava on sidottu muuttujaan Z ; Katso lisätietoja alla olevasta merkitsevästä semantiikasta. ${\ displaystyle \ mu Z. \ phi}$ ${\ displaystyle \ nu Z. \ phi}$ $\ phi$ ${\ displaystyle \ lambda Z. \ phi}$ $\ phi$

Denotation-semantiikka

Mu-calculus-kaavan mallit (propositio, modaali) annetaan tilansiirtojärjestelminä, joissa: ${\ displaystyle (S, R, V)}$

$S$ on joukko valtioita;

$R$ liittää kuhunkin leimaan binaarisuhteen ; $klo$ $S$

${\ displaystyle V: P \ oikeanpuoleinen nuoli 2 ^ {S}}$ yhdistää kuhunkin ehdotukseen joukon tiloja, joissa ehdotus on totta. ${\ displaystyle p \ in P}$

Kun otetaan huomioon siirtymäjärjestelmä , tulkinta yhdistää tilajoukon mihin tahansa muuttujaan . Määritämme tilojen osajoukon rakenteellisen induktion avulla kaavalla : ${\ displaystyle (S, R, V)}$ $i$ $Z$ ${\ displaystyle i (Z)}$ ${\ displaystyle [\! [{\ alleviivattu {\ phi}}] \!] _ {i}}$ $\ phi$

${\ 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 \ kaikki t \ in S, (s, t) \ in R_ {a} \ rightarrow t \ sisään [\! [\ phi] \!] _ {i} \}}$ ;
${\ displaystyle [\! [\ nu Z. \ phi] \!] _ {i} = \ bigcup \ {T \ subseteq S \ mid T \ subseteq [\! [\ phi] \!] _ {i [Z : = T]} \}}$ , jossa hän on yhteydessä toisiinsa säilyttäen samalla yhdistykset kaikkialla muualla. ${\ displaystyle i [Z: = T]}$ $Z$ $T$ $i$

Kaksinaisuuden mukaan muiden peruskaavojen tulkinta on:

${\ displaystyle [\! [\ phi \ vee \ psi] \!] _ {i} = [\! [\ phi] \!] _ {i} \ kuppi [\! [\ psi] \!] _ { i}}$ ;
${\ displaystyle [\! [\ langle a \ rangle \ phi] \!] _ {i} = \ {s \ in S \ mid \ on olemassa t \ in S, (s, t) \ in R_ {a} \ kiila t \ sisään [\! [\ phi] \!] _ {i} \}}$ ;
${\ displaystyle [\! [\ mu Z. \ phi] \!] _ {i} = \ bigcap \ {T \ subseteq S \ mid [\! [\ phi] \!] _ {i [Z: = T ]} \ subseteq T \}}$ .

Epävirallisesti siirtymäjärjestelmä : ${\ displaystyle (S, R, V)}$

$s$ pätee valtioihin ; ${\ displaystyle V (p)}$

${\ displaystyle \ phi \ wedge \ psi}$ on totta, jos ja ovat totta; $\ phi$ $\ psi$

${\ displaystyle \ neg \ phi}$ on totta, jos ei ole totta; $\ phi$

${\ displaystyle [a] \ phi}$ on totta tilassa, jos kaikki lähtevät siirtymät johtavat tilaan, jossa on totta; $s$ $klo$ $s$ $\ phi$

${\ displaystyle \ langle a \ rangle \ phi}$ on totta tilassa, jossa on ainakin yksi siirtyminen , joka johtaa tilaan, jossa on totta; $s$ $klo$ $s$ $\ phi$

${\ displaystyle \ nu Z. \ phi}$ On totta missään tilassa tahansa asettaa siten, että jos muuttuja korvataan , niin pätee kaikkeen (mistä Knaster-Tarskin lauseen , päätellään, että on suurin kiinteän pisteen , ja jota on pienin). $T$ $Z$ $T$ $\ phi$ $T$ ${\ displaystyle [\! [\ nu Z. \ phi] \!] _ {i}}$ ${\ displaystyle [\! [\ phi] \!] _ {i [Z: = T]}}$ ${\ displaystyle [\! [\ mu Z. \ phi] \!] _ {i}}$

Dynaamisen logiikan tulkinta ja on "klassinen" tulkinta . Lisäksi voidaan nähdä omaisuutta vilkkaus ( ”jotain hyvää tapahtuu kerrallaan”), kun nähdään turvallisuus ominaisuus ( ”jotain pahaa koskaan tapahdu”) in Leslie epävirallisessa luokitusta. Lamport . ${\ displaystyle [a] \ phi}$ ${\ displaystyle \ langle a \ rangle \ phi}$ $\ mu$ $\alasti$

Esimerkkejä

${\ displaystyle \ nu Z. \ phi \ wedge [a] Z}$ tulkitaan " pätee kukin polku ". $\ phi$

${\ displaystyle \ mu Z. \ phi \ vee \ langle a \ rangle Z}$ tulkitaan siirtymäpolun olemassaolona a tilaan, jossa totta. $\ phi$

Järjestelmän ominaisuus olla estämätön, toisin sanoen siitä, että mistä tahansa esteettömästä tilasta on lähtevä siirtymä, voidaan ilmaista kaavalla . ${\ displaystyle \ nu Z. (\ bigvee _ {a \ in A} \ langle a \ rangle \ top \ wedge \ bigwedge _ {a \ in A} [a] Z)}$
${\ displaystyle \ mu Z. [a] Z}$ : kaikki -siirtymien muodostama polku on valmis.
${\ displaystyle \ nu Z. \ langle a \ rangle Z}$ : On ääretön polku koostuu -transitions.
${\ displaystyle \ nu Z. \ phi \ land \ langle a \ rangle Z}$ : On ääretön polku koostuu -transitions pitkin, joka on totta koko ajan. $\ phi$

Vuorottelu

Pienempien ja suurempien kiinteiden pisteiden vuorottelua kutsutaan vaihtosyvyydeksi. Voimme laskea vaihtoehtojen lukumäärän, mutta yleensä käytämme kehittyneempää määritelmää, jonka Damian Niwiński esitteli ja joka tarkastelee myös muuttujien käyttöä. Vuorotteluhierarkia on tiukka.

Algoritmiset ongelmat

Mu-hammaskiven malli tarkkailun ongelma on NP välinen co-NP ja on P -dur. Mu-calculus- mallin tarkistuksen algoritmi on seuraava:

Rakenna pariteettipeli siirtymäjärjestelmästä ja vahvistettavasta mu-calculus-kaavasta;
Ratkaise pariteettipeli.

Mu-hammaskiven satisfiability ongelma on EXPTIME-valmis .

Kuten lineaarisessa ajallisessa logiikassa (LTL), myös mallintarkastuksen , lineaarisen mu-laskennan tyydyttävyyden ja pätevyyden ongelma on PSPACE-täydellinen .

Keskustelut

Mu-calculuksen alkuperäinen syntaksin muoto oli vektorimainen. Tämän merkinnän etuna on, että sen avulla muuttujat voidaan jakaa useille alikaavoille. Mu-laskelmasta on lineaarinen versio (ei kytketty).

Bibliografia

(en) Edmund M. Clarke, nuorempi, Orna Grumberg ja Doron A. Peled, Model Checking , Cambridge, Massachusetts, USA, MIT press,1999( ISBN 0-262-03270-8 ), luku 7, μ-laskelman mallintarkistus, s. 97–108
(en) Colin Stirling , prosessien modaaliset ja ajalliset ominaisuudet , New York, Berliini, Heidelberg, Springer Verlag,2001, 191 Sivumäärä ( ISBN 0-387-98717-7 , lue verkossa ), luku 5, Modal μ-calculus, s. 103–128
(en) André Arnold ja Damian Niwiński, μ- Calculuksen rudimentit , Elsevier ,2001, 277 Sivumäärä ( ISBN 978-0-444-50620-7 ), luku 6, μ-laskenta PowerSet-algebroille, s. 141–153 koskee μ-laskentaa.
Yde Venema (2008) Luennot modaalisesta μ-laskennasta ; esiteltiin 18. Euroopan logiikan, kielen ja informaation kesäkoulussa.
(en) Julian Bradfield ja Colin Stirling, Modaalisen logiikan käsikirja , Elsevier ,2006, 721–756 Sivumäärä ( lue verkossa ) , "Modal mu-calculi"
(en) E. Allen Emerson (1996). ”Model Checking and the Mu-calculus” Kuvaava monimutkaisuus ja äärelliset mallit : 185–214 s., American Mathematical Society .
(en) Kozen, Dexter, " Tulokset propositionaalisesta μ-laskennasta " , Theoretical Computer Science , voi. 27, n ° 3,1983, s. 333–354 ( DOI 10.1016 / 0304-3975 (82) 90125–6 )

Ulkoiset linkit

Sophie Pinchinat, logiikka, automaatit ja pelit videotallennus luennosta ANU Logic Summer School '09: ssä

Huomautuksia ja viitteitä

(sisään) Julian Bradfield ja Igor Walukiewicz , "The mu-calculus and Model Checking" , Handinger of Model Checking , Springer International Publishing,2018( ISBN 9783319105741 , DOI 10.1007 / 978-3-319-10575-8_26 , luettu verkossa ) , s. 871–919
André Arnold ja Damian Niwiński, rudiments of μ-Calculus , s. viii-x ja luku 6.
André Arnold ja Damian Niwiński, rudiments of μ-Calculus , s. viii-x ja luku 4.
André Arnold ja Damian Niwiński, alkiot μ- Calculuksesta , s. 14.
Julian Bradfield ja Colin Stirling, The Handbook of Modal Logic , s. 731.
(en) Erich Grädel, Phokion G.Kolaitis, Leonid Libkin , Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema ja Scott Weinstein, Finite Model Theory and its Applications , Springer,2007, 437 Sivumäärä ( ISBN 978-3-540-00428-8 , luettu verkossa ) , s. 159.
" Mu-laskennan kurssi Labrissa " .
(in) Damian Niwinski , " Me kiinteän pisteen klooneja " , Automaatit, kielet ja ohjelmointi , Springer, Berliini, Heidelberg, lukea Notes in Computer Science,15. heinäkuuta 1986, s. 464–473 ( ISBN 3540167617 , DOI 10.1007 / 3-540-16761-7_96 , luettu verkossa , käytetty 12. maaliskuuta 2018 )
(vuonna) JC Bradfield , " Modaalilaskuri on tiukka vuorotteluhierarkia " , CONCUR '96 Concurrency Theory , Springer, Berliini, Heidelberg, lue muistiinpanoja tietojenkäsittelytieteestä,26. elokuuta 1996, s. 233–246 ( ISBN 3540616047 , DOI 10.1007 / 3-540-61604-7_58 , luettu verkossa , käytetty 12. maaliskuuta 2018 )
(in) Klaus Schneider, tarkastaminen reaktiivisia järjestelmiä: muodollisia menetelmiä ja algoritmeja , Springer,2004, 602 Sivumäärä ( ISBN 978-3-540-00296-3 , luettu verkossa ) , s. 521.
(sisään) AP Sistla ja EM Clarke , " Propositionaalisen lineaarisen ajallisen logiikan monimutkaisuus " , J. ACM , voi. 32, n ° 3,1. st heinäkuu 1985, s. 733–749 ( ISSN 0004-5411 , DOI 10.1145 / 3828.3837 , lue verkossa ).
(en) MY Vardi , " A Temporal Fixpoint Calculus " , ACM , New York, NY, USA,1 st päivänä tammikuuta 1988, s. 250–259 ( ISBN 0897912527 , DOI 10.1145 / 73560.73582 , lue verkossa ).
Julian Bradfield ja Igor Walukiewicz , Mu-calculus ja mallintarkastus ( lue verkossa )
Howard Barringer , Ruurd Kuiper ja Amir Pnueli , " Todella abstrakti samanaikainen malli ja sen ajallinen logiikka ", POPL 'x86 Proceedings of the 13. ACM SIGACT-SIGPLAN symposium on Principles of programming languages , ACM1986, s. 173–183 ( DOI 10.1145 / 512644.512660 , luettu verkossa , käytetty 12. maaliskuuta 2018 )

(en) Tämä artikkeli on osittain tai kokonaan otettu Wikipedian englanninkielisestä artikkelista " Modal μ-calculus " ( katso tekijäluettelo ) .