Lógica de Árvore de Computação

Lógica de Árvore de Computação (LAC) é uma ramificação-temporal da Lógica, significando que seu modelo de tempo é como a estrutura árvore no qual o futuro não é determinado. Não tem caminhos diferentes no futuro, qualquer um deles pode ser um caminho atual que é realizado. É usado na verificação formal de artefatos de software ou hardware, tipicamente por aplicações de software conhecidas como verificadores de modelos que determina se um dado artefato possui propriedades de segurança ou liveness. Por exemplo, LAC pode especificar que quando alguma condição inicial é satisfeita (ex: todas as variáveis do programa são positivas ou não há carros na estrada que escarrancham duas pistas ), então todas as possíveis execuções do programa evitam alguma condição indesejável (ex: dividir um número por zero ou o a colisão de dois carros na estrada) . Neste exemplo, a propriedade de segurança pode ser verificada por um modelo verificador que explora todas as possibilidades de transações para fora de um programa de estados satisfazendo a condição inicial que garante que todos as execuções satisfazem esta propriedade. Lógica de Árvore de Computação está na classe de Lógica temporal que inclui Lógica Temporal (LLT). Embora aqui existam propriedades expressáveis em apenas uma das LAC ou LLT, todas as propriedades em ambas as lógicas podem ser expressas em LAC*.

Sintaxe da LAC

A linguagem das fórmulas bem formadas para LAC é gerada pela seguinte gramática:

${\displaystyle \phi ::=\bot |\top |p|(\neg \phi )|(\phi \land \phi )|(\phi \lor \phi )|(\phi \Rightarrow \phi )|(\phi \Leftrightarrow \phi )|{\mbox{AX }}\phi |{\mbox{EX }}\phi |{\mbox{AF }}\phi |{\mbox{EF }}\phi |{\mbox{AG }}\phi |{\mbox{EG }}\phi |{\mbox{A }}[\phi {\mbox{ U }}\phi ]|{\mbox{E }}[\phi {\mbox{ U }}\phi ]}$

onde ${\displaystyle p}$ varia sobre o conjunto das fórmulas atômicas. Nem todas esses conectivos são necessários – por exemplo, ${\displaystyle \{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}}$ Comprime um completo conjunto de conectivos , e os outros podem ser definidos utilizando eles.

• ${\displaystyle {\mbox{A}}}$ significa por todos os Caminhos (Inevitável)
• ${\displaystyle {\mbox{E}}}$ significa pelo menos (existe) um caminho (Possível)

Por exemplo, a seguinte é uma fórmula LAC bem formada:

${\displaystyle {\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r}$)

Por exemplo, a seguinte não é uma fórmula LAC bem formada:

${\displaystyle {\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}}$

O problema com essa string é que ${\displaystyle U}$ pode ocorrer quando emparelhada com ${\displaystyle A}$ ou ${\displaystyle E}$. Essa usa proposições atômicas como essa constrói os blocos para fazer declarações sobre os estados do sistema. LAC então combina essas proposições em fórmulas utilizando operadores lógicos e lógica temporal.

Operadores

Operadores Lógicos

Os operadores lógicos são os usuais: ${\displaystyle \neg ,\lor ,\land ,\Rightarrow }$ e ${\displaystyle \Leftrightarrow }$. Por todos esses operadores, fórmulas LAC podem ser também fzer uso de constantes booleanas Verdadeiro e Falso.

Operadores Temporais

Os operadores temporais são os seguintes:

• Quantificadores através de caminhos
  • A ${\displaystyle \phi }$ – All: ${\displaystyle \phi }$ tem que dizer para manter todos os caminhos começando do estado atual.
  • E ${\displaystyle \phi }$ – Exists: existe ao menos um caminho começando do estado atual onde ${\displaystyle \phi }$ é mantido.
• Quantificadores de caminhos-específicos
  • X ${\displaystyle \phi }$ – Next: ${\displaystyle \phi }$ precisa para manter o próximo estado (este operador é algumas vezes notado como N em vez de X).
  • G ${\displaystyle \phi }$ – Globally: ${\displaystyle \phi }$ tem que manter todo o caminho subsequente.
  • F ${\displaystyle \phi }$ – Finally: ${\displaystyle \phi }$ eventualmente tem que manter (em alguns momentos no caminho subsequente).
  • ${\displaystyle \phi }$ U ${\displaystyle \psi }$ – Until: ${\displaystyle \phi }$ precisa manter ao menos antes de alguma posição ${\displaystyle \psi }$ manter. Isso implica que ${\displaystyle \psi }$ irá ser verificada no futuro.
  • ${\displaystyle \phi }$ W ${\displaystyle \psi }$ – Weak até: ${\displaystyle \phi }$ tiver que manter ${\displaystyle \psi }$ mantém.

A diferença com U É que aqui não é garantido que ${\displaystyle \psi }$ nunca irá ser verificada. O operador W é algumas vezes chamado de "ao menos".

Na LAC*, os operadores temporais podem ser livremente misturados. Na LAC, o operador precisa sempre estar agrupado em dois: um operador de caminho seguido de um operador de estado. Veja o exemplo abaixo. LAC* é estritamente mais expressiva que LAC.

Conjunto mínimo de operadores

Na LAC existe um conjunto mínimo de operadores. Todas fórmulas LAC podem ser transformadas para usarem apenas aqueles operadores. Isto é útil na Checagem de modelo. Um conjunto mínimo de operadores é: {true, ${\displaystyle \lor ,\neg }$, EG, EU, EX}.

Algumas das transformações usadas para operadores temporais são:

• EF${\displaystyle \phi }$ == E[trueU(${\displaystyle \phi }$)] ( porque F${\displaystyle \phi }$ == [trueU(${\displaystyle \phi }$)] )
• AX${\displaystyle \phi }$ == ${\displaystyle \neg }$EX(${\displaystyle \neg }$${\displaystyle \phi }$)
• AG${\displaystyle \phi }$ == ${\displaystyle \neg }$EF(${\displaystyle \neg }$${\displaystyle \phi }$) == ${\displaystyle \neg }$ E[trueU(${\displaystyle \neg }$${\displaystyle \phi }$)]
• AF${\displaystyle \phi }$ == A[trueU${\displaystyle \phi }$] == ${\displaystyle \neg }$EG(${\displaystyle \neg }$${\displaystyle \phi }$)
• A[${\displaystyle \phi }$U${\displaystyle \psi }$] == ${\displaystyle \neg }$( E[(${\displaystyle \neg }$${\displaystyle \psi }$)U${\displaystyle \neg }$(${\displaystyle \phi }$${\displaystyle \lor }$${\displaystyle \psi }$)] ${\displaystyle \lor }$ EG(${\displaystyle \neg }$${\displaystyle \psi }$) )

Semanticas da LAC

Definição

Fórmulas LAC são interpretadas através de sistemas de transições. Um sistema de transação é uma tripla ${\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}$, onde ${\displaystyle S}$ é um conjunto de estados, ${\displaystyle \rightarrow \subseteq S\times S}$ é uma transição relativa, assumida para ser serializada, isto é, cada estado tem ao menos um sucessor, e ${\displaystyle L}$ é uma função de rotulação, assinando letras proposicionais à estados. Deixe ${\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}$ ser uma transição de modelo :with ${\displaystyle s\in S,\phi \in F}$ onde F é o conjunto de fórmulas bem formadas sobre a linguagem de ${\displaystyle {\mathcal {M}}}$.

Então a relação de semântica ${\displaystyle ({\mathcal {M}},s\models \phi )}$ é definida por indução estrutural em ${\displaystyle \phi }$:

1. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}$
2. ${\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}$
3. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}}$
4. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
5. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
6. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
7. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}{\bigg )}}$
8. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
9. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
10. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
11. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
12. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
13. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
14. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$
15. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$

Caracterização de uma LAC

As 10 à 15 regras acima referem-se à caminhos de computação em modelos e são o que ultimamente caracterizam a "Árvore de Computação"; São assertivas sobre a natureza do profundo infinito da árvore de computação enraizada no dado estado ${\displaystyle s}$.

Equivalências semânticas

A fórmula ${\displaystyle \phi }$ e ${\displaystyle \psi }$ são ditas como semanticamente equivalentes se algum estado em algum modelo que satisfaz uma também satisfaz a outra. Isso é chamado ${\displaystyle \phi \equiv \psi }$

Nisto pode ser ver que A e A são duplas, sendo quantificadores de caminhos de computações universais e existencies respectivamente: ${\displaystyle \neg A\phi \equiv E\neg \phi }$.

Ainda mais são G e F.

E uma instância da Lei de De Morgan pode ser formulada em LAC:

${\displaystyle \neg AF\phi \equiv EG\neg \phi }$

${\displaystyle \neg EF\phi \equiv AG\neg \phi }$

${\displaystyle \neg AX\phi \equiv EX\neg \phi }$

Isto ppde ser mostrado usando os identificadores que subconjunto de conectivos temporais de LAC é adequado se ele contém ${\displaystyle EU}$, ao menos um de ${\displaystyle \{AX,EX\}}$ e ao menos um de ${\displaystyle \{EG,AF,AU\}}$ e os conectivos booleanos.

A equivalência importante abaixo chamada de lei da expansão; elas permitem para desvirar as verificações de um conectivo LAC à frente de seu sucessor no tempo.

${\displaystyle AG\phi \equiv \phi \land AXAG\phi }$

${\displaystyle EG\phi \equiv \phi \land EXEG\phi }$

${\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$

${\displaystyle EF\phi \equiv \phi \lor EXEF\phi }$

${\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$

${\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}$

Exemplos

Seja "P" significando "Eu amo chocolate" e Q significando "Está frio lá fora"

• AG.P

"Eu irei gostar de chocolate a partir de agora, não importa o que aconteça"

• EF.P

"É possível que eu ame chocolate algum dia, ao menos por um dia."

• AF.EG.P

"É sempre possível (AF) que eu comece a amar chocolate pelo resto de minha vida."

(Note: não apenas o resto da minha vida, desde que minha vida é finita, enquanot G é infinito).

• EG.AF.P

"Isso é um momento crítico da vida. Dependendo do que venha a acontecer (E), é sempre possível que pelo resto de meu tempo (G), irá existir sempre algo no tempo no futuro (AF) quando eu amar chocolate. De qualquer maneira, se a coisa errada acontecer em seguinte, então todas as apostas são desligadas e não há garantias se eu irei sempre amar chocolate."

Os dois examplos seguintes mostram o exempre entre LAC e LAC*, assim como eles permitem o operador para não ser qualificado com nenhum operador de caminho (A or E):

• AG(PUQ)

"A partir de agora, antes que fique quente lá fora, eu irei amar chocolate todo dia. Uma vez que fique quente lá fora, todas as apostas são desligadas para se eu irei gostar de chocolate mais. Ah, e é garantido ficar quente lá fora eventualmente, mesmo se por apenas um único dia."

• EF((EX.P)U(AG.Q))

"É possível que: irá eventualmente existir um tempo quando ficar quente para sempre (AG.Q) e que antes desse tempo irá existir sempre algum jeito de eu vir a gostar de chocolate no próximo dia (EX.P)."

Relações com outras lógicas

Lógica de Árvore de Computação (LAC) é um subconjunto de de LAC* assim como da modal µ cLACulus. LAC é também um fragmento de Alur, Henzinger and Kupferman's Lógica Temporal Alternativa (LTA).

Lógica de Árvore de Computação (LAC) e Lógica Temporal (LLT) são todos subconjuntos de LAC*. CTL e LLT não são equivalentes e eles não possuem subconjuntos em comum, o que é um próprio subconjunto de LAC e LLT.

• FG.P existe em LLT mas não em LAC.
• AG(P${\displaystyle \Rightarrow }$((EX.Q)${\displaystyle \land }$(EX¬Q))) existe em LAC mas não existe em LLT.

Ver também

• Lógica Temporal

Referências

Bibliografia

• Michael Huth and Mark Ryan (2004). «Logic in Computer Science (Second Edition)». Cambridge University Press: 207. ISBN 0-521-54310-X 
• Emerson, E. A. and Halpern, J. Y. (1985). «Decision procedures and expressiveness in the temporal logic of branching time». Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7  !CS1 manut: Nomes múltiplos: lista de autores (link)
• Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). «Automatic verification of finite-state concurrent systems using temporal logic specifications». ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399  !CS1 manut: Nomes múltiplos: lista de autores (link)
• Emerson, E. A. (1990). «Temporal and modal logic». In: Jan van Leeuwen. Handbook of Theoretical Computer Science, vol. B. [S.l.]: MIT Press. pp. 955–1072. ISBN 0-262-22039-3 

Ligações externas

• Teaching slides of CTL