Mostrar código-fonte de Lógica de Árvore de Computação

{{Sem fontes|data=outubro de 2024}}

'''Lógica de Árvore de Computação&nbsp;(LAC)''' é uma ramificação-temporal da [[Lógica Matemática|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]]&nbsp;(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 regular|linguagem]] das [[Fórmula bem formada|fórmulas bem formadas]] para LAC é gerada pela seguinte [[Gramática Livre de Contexto|gramática]]:
:<math>\phi::=\bot |\top |p|(\neg\phi
)|(\phi\and\phi)|(\phi\or\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]</math>

onde <math>p</math> varia sobre o conjunto das [[Fórmula atômica|fórmulas atômicas]]. Nem todas esses conectivos são necessários&nbsp;– por exemplo,
<math>\{\neg, \and, \mbox{AX}, \mbox{AU}, \mbox{EU}\}</math> Comprime um completo conjunto de conectivos , e os outros podem ser definidos utilizando eles.

*<math>\mbox{A}</math> significa por todos os Caminhos ''(Inevitável)''
*<math>\mbox{E}</math> significa pelo menos (existe) um caminho ''(Possível)''

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

:<math>\mbox{EF }(\mbox{EG } p \Rightarrow \mbox{AF } r </math>)

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

:<math>\mbox{EF }\big(r \mbox{ U } q\big) </math>

O problema com essa ''string'' é que  <math>U</math> pode ocorrer quando emparelhada com <math>A</math> ou <math>E</math>.
Essa usa [[Sentença atômica| 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 [[Conectivo lógico| operadores lógicos]] são os usuais: <math>\neg,\or,\and,\Rightarrow</math> e
<math>\Leftrightarrow</math>. 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:
* [[Quantificação|Quantificadores]] através de caminhos
**'''A''' <math>\phi</math>&nbsp;– '''A'''ll: <math>\phi</math> tem que dizer para manter todos os caminhos começando do estado atual.
**'''E''' <math>\phi</math>&nbsp;– '''E'''xists: existe ao menos um caminho começando do estado atual onde <math>\phi</math> é mantido.
* Quantificadores de caminhos-específicos
**'''X''' <math>\phi</math>&nbsp;– Ne'''x'''t: <math>\phi</math> precisa para manter o próximo estado (este operador é algumas vezes notado como '''N''' em vez de '''X''').
**'''G''' <math>\phi</math>&nbsp;– '''G'''lobally: <math>\phi</math> tem que manter todo o caminho subsequente.
**'''F''' <math>\phi</math>&nbsp;– '''F'''inally: <math>\phi</math> eventualmente tem que manter (em alguns momentos no caminho subsequente).
**<math>\phi</math> '''U''' <math>\psi</math>&nbsp;– '''U'''ntil: <math>\phi</math> precisa manter ''ao menos'' antes de alguma posição <math>\psi</math> manter. Isso implica que <math>\psi</math> irá ser verificada no futuro.
**<math>\phi</math> '''W''' <math>\psi</math>&nbsp;– '''W'''eak até: <math>\phi</math> tiver que manter <math>\psi</math> mantém.
A diferença com '''U''' É que aqui não é garantido que   <math>\psi</math>  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, <math>\or, \neg</math>, '''EG''', '''EU''', '''EX'''}.

Algumas das transformações usadas para operadores temporais são:
*'''EF'''<math>\phi</math> == '''E'''[true'''U'''(<math>\phi</math>)]   ( porque '''F'''<math>\phi</math> == [true'''U'''(<math>\phi</math>)] )
*'''AX'''<math>\phi</math> == <math>\neg</math>'''EX'''(<math>\neg</math><math>\phi</math>)
*'''AG'''<math>\phi</math> == <math>\neg</math>'''EF'''(<math>\neg</math><math>\phi</math>) == <math>\neg</math> '''E'''[true'''U'''(<math>\neg</math><math>\phi</math>)]
*'''AF'''<math>\phi</math> == '''A'''[true'''U'''<math>\phi</math>] == <math>\neg</math>'''EG'''(<math>\neg</math><math>\phi</math>)
*'''A'''[<math>\phi</math>'''U'''<math>\psi</math>] == <math>\neg</math>( '''E'''[(<math>\neg</math><math>\psi</math>)'''U'''<math>\neg</math>(<math>\phi</math><math>\or</math><math>\psi</math>)] <math>\or</math> '''EG'''(<math>\neg</math><math>\psi</math>) )
<!---
*'''F''' <math>\phi</math> = '''true''' '''U''' <math>\phi</math>
*'''G''' <math>\phi</math> = <math>\neg</math> '''F''' <math>\neg</math><math>\phi</math>
--->

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

Então a relação de semântica <math>(\mathcal{M}, s \models \phi)</math> é definida por [[Indução Estrutural| indução estrutural ]] em <math>\phi</math>:
# <math>\Big( (\mathcal{M}, s) \models \top \Big) \Leftrightarrow \Big( (\mathcal{M}, s) \not\models \bot \Big)</math>
# <math>\Big( (\mathcal{M}, s) \models p \Big) \Leftrightarrow \Big( p \in L(s) \Big)</math>
# <math>\Big( (\mathcal{M}, s) \models \neg\phi \Big) \Leftrightarrow \Big( (\mathcal{M}, s) \not\models \phi \Big)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>
# <math>\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)</math>

===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 <math>s</math>.

===Equivalências semânticas ===
A fórmula <math>\phi</math> e <math>\psi</math> são ditas como semanticamente equivalentes se algum estado em algum modelo que satisfaz uma também satisfaz a outra.
Isso é chamado <math>\phi \equiv \psi</math>

Nisto pode ser ver que A e A são duplas, sendo quantificadores de caminhos de computações universais e existencies respectivamente:
<math>\neg A\phi \equiv E \neg \phi </math>.

Ainda mais são G e F.

E uma instância da [[Teoremas de De Morgan|Lei de De Morgan]] pode ser formulada em LAC:
:<math>\neg AF\phi \equiv EG\neg\phi</math>
:<math>\neg EF\phi \equiv AG\neg\phi</math>
:<math>\neg AX\phi \equiv EX\neg\phi</math>

Isto ppde ser mostrado usando os identificadores que [[subconjunto]] de conectivos temporais de LAC é adequado se ele contém <math>EU</math>, ao menos um de  <math>\{AX,EX\}</math> e ao menos um de <math>\{EG,AF,AU\}</math> 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.
:<math>AG\phi \equiv \phi \land AX AG \phi</math>
:<math>EG\phi \equiv \phi \land EX EG \phi</math>
:<math>AF\phi \equiv \phi \lor AX AF \phi</math>
:<math>EF\phi \equiv \phi \lor EX EF \phi</math>
:<math>A[\phi U \psi] \equiv \psi \lor (\phi \land AX A [\phi U \psi])</math>
:<math>E[\phi U \psi] \equiv \psi \lor (\phi \land EX E [\phi U \psi])</math>

==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'''(P'''U'''Q)
:"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==
<!-- LAC é um subconjunto de LAC* -->
Lógica de Árvore de Computação (LAC) é um subconjunto de de LAC* assim como da [[modal mu cLACulus|modal µ cLACulus]]. LAC é também um fragmento de  Alur, Henzinger and Kupferman's [[Lógica Temporal Alternativa]] (LTA).

<!-- LAC é um complemento para LLT -->
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<math>\Rightarrow</math>(('''EX'''.Q)<math>\land</math>('''EX'''¬Q))) existe em LAC mas não existe em LLT.

== Ver também ==
*[[Lógica Temporal]]

{{Referências}}

== Bibliografia ==
* {{citar periódico|autor =Michael Huth and Mark Ryan |título=Logic in Computer Science (Second Edition) |ano=2004|página=207 |publicado=Cambridge University Press | isbn=0-521-54310-X}}
* {{citar periódico|autor =Emerson, E. A. and Halpern, J. Y. |título=Decision  procedures and expressiveness in the temporal logic of branching time |periódico=Journal of Computer and System Sciences|ano=1985| volume=30 |número=1 |páginas=1–24 | doi=10.1016/0022-0000(85)90001-7}}
* {{citar periódico|autor =Clarke, E. M., Emerson, E. A., and Sistla, A. P. |título=Automatic verification of finite-state concurrent systems using temporal logic specifications |periódico=ACM Transactions on Programming Languages and Systems|ano=1986| volume=8 |número=2 |páginas=244–263 | doi=10.1145/5397.5399}}
* {{citar livro|autor =Emerson, E. A. |ano=1990 |capítulo=Temporal and modal logic | editor=[[Jan van Leeuwen]] |título=Handbook of Theoretical Computer Science, vol. B |páginas=955–1072 |publicado=MIT Press | isbn=0-262-22039-3}}

==Ligações externas==
*[http://www.inf.unibz.it/~artale/FM/slide4.pdf Teaching slides of CTL]

[[Categoria:Teoria dos autômatos]]