Mu-cálculo

Na lógica matemática e na ciência da computação teórica , mu-calculus (ou lógica do modal mu-calculus ) é a extensão da lógica modal clássica com operadores de ponto fixo . Segundo Bradfield e Walukiewicz, mu-calculus é uma das lógicas mais importantes para a verificação de modelos; é expressivo, embora tenha boas propriedades algorítmicas.

Mu-cálculo ( proposicional e modal ) foi introduzido pela primeira vez por Dana Scott e Jaco de Bakker e, em seguida, estendido em sua versão moderna por Dexter Kozen . Essa lógica permite descrever as propriedades dos sistemas de transição de estado e verificá-las. Muitas lógicas temporais (como CTL * ou seus fragmentos amplamente usados como CTL (en) ou LTL ) são fragmentos de cálculo mu.

Uma maneira algébrica de ver o cálculo mu é pensá-lo como uma álgebra de funções monotônicas sobre uma rede completa , os operadores sendo uma composição funcional mais pontos fixos; deste ponto de vista, mu-calculus atua na rede da álgebra de conjuntos . A semântica dos jogos de mu-cálculo está ligada a jogos para dois jogadores com informações perfeitas, em particular jogos de paridade .

Sintaxe

Sejam dois conjuntos de símbolos P (as proposições) e A (as ações) e V um conjunto enumerável infinito de variáveis. O conjunto de fórmulas de cálculo mu (proposicional e modal) é indutivamente definido como segue:

cada proposição é uma fórmula;

cada variável é uma fórmula;

se e são fórmulas, então é uma fórmula; $\ phi$ $\ psi$ ${\ displaystyle (\ phi \ wedge \ psi)}$

se é uma fórmula, então é uma fórmula; $\ phi$ ${\ displaystyle \ neg \ phi}$

se é uma fórmula e é uma ação, então é uma fórmula (é a fórmula: “depois , necessariamente ”); $\ phi$ $no$ ${\ displaystyle [a] \ phi}$ $no$ $\ phi$

se for uma fórmula e uma variável, então é uma fórmula assumindo que cada ocorrência de in aparece positivamente, ou seja, é negada um número par de vezes. $\ phi$ $Z$ ${\ displaystyle \ nu Z. \ phi}$ $Z$ $\ phi$

As noções de variáveis limitadas ou livres são definidas normalmente com quem é o único operador vinculando uma variável. $\nu$

Com as definições acima, podemos adicionar como açúcar sintático :

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

${\ displaystyle \ langle a \ rangle \ phi}$ significante (depois é possível ); ${\ displaystyle \ neg [a] \ neg \ phi}$ $no$ $\ phi$

${\ displaystyle \ mu Z. \ phi}$ significante , onde significa que substituímos por para cada ocorrência livre de in . ${\ displaystyle \ neg \ nu Z. \ neg \ phi [Z: = \ neg Z]}$ ${\ displaystyle \ phi [Z: = \ neg Z]}$ $Z$ ${\ displaystyle \ neg Z}$ $Z$ $\ phi$

Os dois primeiros são fórmulas familiares de cálculo e modal lógica K .

A notação (e respectivamente seu dual ) é inspirada no cálculo lambda ; o objetivo é denotar o menor (respectivamente o maior) ponto fixo na variável Z da expressão, assim como em lambda-cálculo é uma função da fórmula na variável limitada Z ; consulte a semântica denotacional abaixo para obter mais detalhes. ${\ displaystyle \ mu Z. \ phi}$ ${\ displaystyle \ nu Z. \ phi}$ $\ phi$ ${\ displaystyle \ lambda Z. \ phi}$ $\ phi$

Semântica denotacional

Os modelos de uma fórmula de cálculo mu (proposicional, modal) são dados como sistemas de transição de estado onde: ${\ displaystyle (S, R, V)}$

$S$ é um conjunto de estados;

$R$ associa a cada rótulo uma relação binária ; $no$ $S$

${\ displaystyle V: P \ rightarrow 2 ^ {S}}$ associa a cada proposição o conjunto de estados onde a proposição é verdadeira. ${\ displaystyle p \ in P}$

Dado um sistema de transição , uma interpretação associa um subconjunto de estados a qualquer variável . Definimos o subconjunto de estados por indução estrutural na fórmula : ${\ displaystyle (S, R, V)}$ $eu$ $Z$ ${\ displaystyle i (Z)}$ ${\ displaystyle [\! [{\ underline {\ phi}}] \!] _ {i}}$ $\ phi$

${\ displaystyle [\! [p] \!] _ {i} = V (p)}$ ;
${\ displaystyle [\! [Z] \!] _ {i} = i (Z)}$ ;
${\ displaystyle [\! [\ phi \ wedge \ psi] \!] _ {i} = [\! [\ phi] \!] _ {i} \ cap [\! [\ psi] \!] _ { eu}}$ ;
${\ 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]} \}}$ , onde se associa com preservando associações de todos os outros lugares. ${\ displaystyle i [Z: = T]}$ $Z$ $T$ $eu$

Por dualidade, a interpretação das outras fórmulas básicas é:

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

Informalmente, para um sistema de transição : ${\ displaystyle (S, R, V)}$

$p$ é verdadeiro para estados ; ${\ displaystyle V (p)}$

${\ displaystyle \ phi \ wedge \ psi}$ é verdadeiro se e for verdadeiro; $\ phi$ $\ psi$

${\ displaystyle \ neg \ phi}$ é verdadeiro se não for verdadeiro; $\ phi$

${\ displaystyle [a] \ phi}$ é verdadeiro no estado se todas as transições de saída conduzem a um estado onde é verdadeiro; $s$ $no$ $s$ $\ phi$

${\ displaystyle \ langle a \ rangle \ phi}$ É verdade num estado se houver pelo menos uma transição de que leva a um estado onde é verdadeira; $s$ $no$ $s$ $\ phi$

${\ displaystyle \ nu Z. \ phi}$ é verdadeiro em qualquer estado de qualquer conjunto tal que, se a variável for substituída por , então é verdadeiro para tudo (do teorema de Knaster-Tarski , deduzimos que é o maior ponto fixo de , e por é o menor). $T$ $Z$ $T$ $\ phi$ $T$ ${\ displaystyle [\! [\ nu Z. \ phi] \!] _ {i}}$ ${\ displaystyle [\! [\ phi] \!] _ {i [Z: = T]}}$ ${\ displaystyle [\! [\ mu Z. \ phi] \!] _ {i}}$

A interpretação de e é a interpretação "clássica" da lógica dinâmica . Além disso, pode ser visto como uma propriedade de vivacidade ("algo bom acontece de cada vez"), enquanto é visto como uma propriedade de segurança ("algo ruim nunca acontece") na classificação informal de Leslie . ${\ displaystyle [a] \ phi}$ ${\ displaystyle \ langle a \ rangle \ phi}$ $\ mu$ $\nu$

Exemplos

${\ displaystyle \ nu Z. \ phi \ wedge [a] Z}$ é interpretado como " é verdadeiro para cada caminho de a ". $\ phi$

${\ displaystyle \ mu Z. \ phi \ vee \ langle a \ rangle Z}$ é interpretado como a existência de um caminho de transições de um para um estado em que é verdade. $\ phi$

A propriedade de um sistema de não bloquear, ou seja, de qualquer estado acessível há uma transição de saída, pode ser expressa pela fórmula . ${\ displaystyle \ nu Z. (\ bigvee _ {a \ in A} \ langle a \ rangle \ top \ wedge \ bigwedge _ {a \ in A} [a] Z)}$
${\ displaystyle \ mu Z. [a] Z}$ : qualquer caminho feito de uma -transições é finalizado.
${\ displaystyle \ nu Z. \ langle a \ rangle Z}$ : Existe um caminho infinito composta de um -transitions.
${\ displaystyle \ nu Z. \ phi \ land \ langle a \ rangle Z}$ : Existe um caminho infinito composta de um -transitions ao longo do qual é verdadeiro o tempo todo. $\ phi$

Alternação

A alternância de pontos fixos menores e maiores é chamada de profundidade de alternância. Podemos contar o número de alternâncias, mas geralmente usamos uma definição mais sofisticada introduzida por Damian Niwiński, que também analisa o uso de variáveis. A hierarquia de alternância é estrita.

Problemas de algoritmo

O problema de verificação do modelo de cálculo mu está em NP inter co-NP e é P -dur. Um algoritmo para verificação de modelo de cálculo mu é o seguinte:

Construa um jogo de paridade a partir do sistema de transições e da fórmula mu-cálculo a ser verificada;
Resolva o jogo da paridade.

O problema de satisfatibilidade do cálculo mu está completo em EXPTIME .

Tal como acontece com a lógica temporal linear (LTL), o problema de verificação do modelo , satisfatibilidade e validade do cálculo mu linear é PSPACE-completo .

Discussões

A sintaxe original do mu-calculus era vetorial. A vantagem dessa notação é que ela permite que as variáveis sejam compartilhadas em várias subfórmulas. Existe uma versão linear (não conectada) do cálculo mu.

Bibliografia

(en) Edmund M. Clarke, Jr. , Orna Grumberg e Doron A. Peled, Model Checking , Cambridge, Massachusetts, EUA, MIT press,1999( ISBN 0-262-03270-8 ), capítulo 7, Verificação de modelo para o cálculo µ, pp. 97–108
(pt) Colin Stirling , Modal and Temporal Properties of Processes , New York, Berlin, Heidelberg, Springer Verlag,2001, 191 p. ( ISBN 0-387-98717-7 , leia online ), capítulo 5, cálculo μ modal, pp. 103-128
(pt) André Arnold e Damian Niwiński, Rudiments of μ-Calculus , Elsevier ,2001, 277 p. ( ISBN 978-0-444-50620-7 ), capítulo 6, The μ-calculus over powerset algebras, pp. 141-153 diz respeito ao cálculo µ.
Yde Venema (2008) Palestras sobre o μ-cálculo Modal ; foi apresentado na 18ª Escola Europeia de Verão em Lógica, Linguagem e Informação.
(pt) Julian Bradfield e Colin Stirling, The Handbook of Modal Logic , Elsevier ,2006, 721–756 p. ( leia online ) , "Modal mu-calculi"
(en) E. Allen Emerson (1996). “Model Checking and the Mu-calculus” Descritiva Complexidade e Modelos Finitos : 185-214 p., American Mathematical Society .
(en) Kozen, Dexter, “ Results on the Propositional μ-Calculus ” , Theoretical Computer Science , vol. 27, n o 3,1983, p. 333–354 ( DOI 10.1016 / 0304-3975 (82) 90125-6 )

links externos

Sophie Pinchinat, Logic, Automata & Games gravação de vídeo de uma palestra na ANU Logic Summer School '09

Notas e referências

(em) Julian Bradfield e Igor Walukiewicz , "The mu-cálculo e verificação de modelo" , em Handbook of Modelo Verificação , Springer Publishing Internacional,2018( ISBN 9783319105741 , DOI 10.1007 / 978-3-319-10575-8_26 , ler online ) , p. 871-919
André Arnold e Damian Niwiński, Rudiments of μ-Calculus , pp. viii-xe capítulo 6.
André Arnold e Damian Niwiński, Rudiments of μ-Calculus , pp. viii-xe capítulo 4.
André Arnold e Damian Niwiński, Rudiments of μ-Calculus , p. 14
Julian Bradfield e Colin Stirling, O Manual de Lógica Modal , p. 731.
(en) Erich Grädel, Phokion G. Kolaitis, Leonid Libkin , Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema e Scott Weinstein, Teoria do Modelo Finito e suas Aplicações , Springer,2007, 437 p. ( ISBN 978-3-540-00428-8 , leitura online ) , p. 159.
" Curso de cálculo mu na Labri " .
(em) Damian Niwinski , " We fixed-point clones " , Automata, Languages and Programming , Springer, Berlin, Heidelberg, leia Notes in Computer Science,15 de julho de 1986, p. 464-473 ( ISBN 3540167617 , DOI 10.1007 / 3-540-16761-7_96 , lido online , acessado em 12 de março de 2018 )
(em) JC Bradfield , " The modal mu-calculus is strict alternation hierarchy " , CONCUR '96 Concurrency Theory , Springer, Berlin, Heidelberg, ler Notes in Computer Science,26 de agosto de 1996, p. 233–246 ( ISBN 3540616047 , DOI 10.1007 / 3-540-61604-7_58 , lido online , acessado em 12 de março de 2018 )
(in) Klaus Schneider, Verificação de sistemas reativos: métodos e algoritmos formais , Springer,2004, 602 p. ( ISBN 978-3-540-00296-3 , leitura online ) , p. 521.
(em) AP Sistla e EM Clarke , " The Complexity of Propositional Linear Temporal Logics " , J. ACM , vol. 32, n o 3,1 r jul 1985, p. 733-749 ( ISSN 0004-5411 , DOI 10.1145 / 3828.3837 , ler online ).
(en) MY Vardi , " A Temporal Fixpoint Calculus " , ACM , New York, NY, USA,1 r janeiro 1988, p. 250–259 ( ISBN 0897912527 , DOI 10.1145 / 73560.73582 , leia online ).
Julian Bradfield e Igor Walukiewicz , The mu-calculus and model-checking ( leia online )
Howard Barringer , Ruurd Kuiper e Amir Pnueli , “ Um modelo concorrente realmente abstrato e sua lógica temporal ”, POPL 'x86 Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , ACM,1986, p. 173–183 ( DOI 10.1145 / 512644.512660 , ler online , acessado em 12 de março de 2018 )

(pt) Este artigo foi retirado parcial ou totalmente do artigo da Wikipedia em inglês intitulado " Modal μ-calculus " ( ver a lista de autores ) .