ADDSON ARAUJO DA COSTA IGOR LINNIK CAMARA ARAUJO LUANA WANDECY PEREIRA SILVA MARCOS AURÉLIO C. DOS SANTOS ROSANA CAETANO DE FARIA MONTEIRO SILVIO ROMERO DE AZEVEDO COSTA Introdução Histórico Motivação Estrutura de Kripke Caminhos Padrões LTL CTL*/CTL Expressividade Aplicações Verificação de modelos Conclusão Introdução Histórico Motivação Estrutura de Kripke Tempo Linear X Tempo Ramificado Na lógica temporal, o tempo não é mencionado explicitamente, mas visto como possíveis seqüências de estados associados às suas transições. Estado é a descrição do sistema em um dado instante de tempo, ou seja, os valores associados às suas variáveis naquele instante, enquanto transição é uma relação entre dois estados. Tipicamente, as afirmações sobre o comportamento do sistema em um determinado estado são feitas através de propriedades, e estas por sua vez são expressas como fórmulas de uma linguagem de lógica temporal, que especificam os comportamentos desejados. A maneira como é feita a representação do tempo nas propriedades, isto é, de maneira linear ou ramificada, faz com que haja dois modelos básicos de lógicas temporais: Linear Temporal Logic (LTL) e Computation Tree Logic (CTL). Tempo Linear É Tempo Ramificado aquele em que o Todo o comportamento comportamento do do sistema é sistema consiste no representado por uma conjunto de traços árvore computacional de infinitos que começam profundidade ilimitada no estado inicial i. cuja raiz é o estado inicial i. Exemplo: Exemplo: É uma lógica temporal de tempo linear que interpreta fórmulas sobre funcionamentos do sistema, e faz a caracterização de cada caminho linear proporcionado pelas máquinas de estados finitos. A lógica LTL considera que há somente um único estado sucessor, ou seja, um único futuro possível, a cada momento do tempo. As fórmulas LTL são avaliadas sobre caminhos lineares, e uma fórmula somente é considerada verdadeira em um modelo se ela é verdadeira para todos os caminhos iniciando num dos estados iniciais daquele modelo. Sintaxe: Uma fórmula LTL sintaticamente válida é formada pelas variáveis proposicionais p1, p2, (...), os conectivos usuais da lógica proposicional (, , , ), e os seguintes operadores temporais: o Next: X - é verdadeiro no próximo estado; o Future: F - é eventualmente válida (em algum estado do caminho); o Globally: G - é sempre válida (em todo estado no caminho); o Until: U - é verdadeira no caminho até que seja verdadeira; o Release: R - quando a ocorrência de um estado onde é válida liberta de o ser. o Exists: E - é verdadeiro num caminho S se existe um caminho começando em um estado S o All: A - é verdadeiro para todo caminho começando no estado S. Os conectivos são X, F e G são usados algumas vezes através dos símbolos , , , respectivamente. Caminho - Um caminho em M é uma seqüência infinita de estados s0 , s1 , s2 , ... tal que s0 ∈ I e (si , si+1 ∈ R para todo i ≥ 0). Semântica - Sejam p ∈ AP uma proposição atômica, σ caminho infinito e φ, ψ fórmulas LTL, a relação “satisfaz”, denotada por |=, é definida por: σ |= p ⇔ p ∈ Label(σ[0]) σ |= ¬φ ⇔ not(σ |= φ) σ |= φ ∧ ψ ⇔ (σ |= φ) and (σ |= ψ) σ |=Xφ ⇔ σ 1 |= φ σ |= φUψ ⇔ ∃j ≥ 0, (σ j |= ψ and (∀0 ≤ k < j, σ k |= φ)) Os padrões mais freqüentes são: Ausência: quando no contexto se pretende que não ocorram certos eventos ou estados. Universalidade: quando se pretende que em todo o contexto certa propriedade se verifique. Existência: quando se pretende que uma propriedade ocorra alguma vez no contexto. Resposta: dentro do contexto a ocorrência de certo evento (causa) deve ser seguida da ocorrência de outro (efeito). Axiomas: - Leis de distribuitividade X ( ) X X X ( ) X X X X F ( ) F F Leis de distribuitividade F G G( ) G G G F ( ) U ( U ) ( U ) U ( ) ( U ) ( U ) - Leis de idempotência FF GG FGF GFG U ( U ) F G GF FG U - Leis de expansão F XF G XG U ( X ( U )) Verificação de modelos usando LTL: Dado um modelo M formalmente representado pela estrutura de Kripke M = ( S, I, R, Label) e uma fórmula LTL φ: M |= φ se e somente se ∀s ∈ I, (∀ Caminhos(s), σ |= φ) LTL considera apenas um único estado Em meados de 80, Clarke e Emerson Considerar diferentes estados possíveis Utilizada em vários verificadores de modelos LTL considera apenas um único estado Em meados de 80, Clarke e Emerson Considerar diferentes estados possíveis Utilizada em vários verificadores de modelos Possibilidade de descrever MEF como uma árvore de estados infinita Desdobramento de uma estrutura de Kripke em árvore de computação infinita Composta por: Fórmulas de estados (ФS) Fórmulas de caminhos (ФP) • Acrescenta a LTL, quantificadores de caminho: Existencial (E) Universal (A) Eα É verdadeira em um estado s se existe um caminho começando em s tal que α é verdadeira neste caminho; Aα É verdadeira em um estado s se para todo um caminho começando em s, α é verdadeira neste caminho. Operadores X F G U Xα: é verdadeira em um caminho π, se no próximo estado do caminho α é verdadeira α Fα: é verdadeira em um caminho π, se em algum estado no caminho α é verdadeira α Gα: é verdadeira em um caminho π, se em todo estado no caminho α é verdadeira α α α α αUβ: é verdadeira em um caminho π, se α é verdadeira no caminho até que β seja verdadeira α α β Gerada pela BNF: ФS ::= P | (¬ФS) | (ФS ∧ ФS) | (ФS ∨ ФS) | (ФS → ФS) | (EФP) | (AФP) ФP ::= ФS | (¬ФP) | (ФP ∧ ФP) | (ФP ∨ ФP) | (ФP → ФP) | (XФP) | (FФP) | (GФP) | (ФP U ФP) Dada pela definição ⊨ de CTL Satisfação em estado K ⊨s α Satisfação em caminho K ⊨π α K ⊨s P ⇔ P ∈ L(s) K ⊨s (¬α) ⇔ NOT K ⊨s α K ⊨s (α ∧ β) ⇔ K ⊨s α E K ⊨s β K ⊨s (α ∨ β) ⇔ K ⊨s α OU K ⊨s β K ⊨s (α → β) ⇔ SE K ⊨s α ENTÃO K ⊨s β K ⊨s (Eα) ⇔ Existe um caminho π a partir de s tal que K ⊨π α K ⊨s (Aα) ⇔ Para todo caminho π a partir de s vale que K ⊨π α K ⊨π α ⇔ se α é uma fórmula da linguagem Фs, K ⊨π0 α K ⊨π (¬α) ⇔ NOT K ⊨π α K ⊨π (α ∧ β) ⇔ K ⊨π α E K ⊨π β K ⊨π (α ∨ β) ⇔ K ⊨π α OU K ⊨π β K ⊨s (α → β) ⇔ SE K ⊨π α ENTÃO K ⊨π β K ⊨π (Xα) ⇔ K ⊨π1,∞ α K ⊨π (Fα) ⇔ Existe um k ≥ 0 tal que K ⊨πk,∞ α K ⊨π (Gα) ⇔ Para todo k ≥ 0 vale que K ⊨πk,∞ α K ⊨π (αUβ) ⇔ Existe k ≥ 0 tal que K ⊨πk,∞ β e para todo 0 ≤ l < k vale que K ⊨πl,∞ α Subconjunto da CTL* Operador temporal precedido por quantificador de caminho Semântica e operadores = CTL* [EX]α – existe um caminho tal que no próximo estado vale α α [AX]α – para todo caminho no próximo estado vale α α α [EF]α – existe um caminho tal que no futuro vale α α [AF]α – para todo caminho no futuro vale α α α α [EG]α – existe um caminho tal que sempre vale α α α α [AG]α – para todo caminho vale sempre α α α α α α α α E(αUβ) – existe um caminho tal que vale α até que vale β α β A(αUβ) – para todo caminho vale α até que vale β α α β β β Existe uma discussão sobre a melhor lógica para expressar propriedades, LTL ou CTL. Contudo, as propriedades usualmente utilizadas na verificação de tais sistemas podem ser expressas nas duas lógicas. Propriedades podem ser descritas em uma lógica e não podem na outra, e vice-versa. A maior parte das propriedades pode ser expressa tanto em CTL quanto em LTL. Por exemplo, a invertibilidade apenas pode ser expressa em CTL. Propriedades existenciais não podem ser expressas na lógica LTL. Este tipo de propriedade é muito útil na procura de possíveis deadlocks em um sistema. Já a lógica CTL, não é capaz de expressar algumas propriedades de razoabilidade. Cada uma destas lógicas é usada em situações diferentes, pois o uso de uma lógica ou da outra depende do tipo de propriedade que se quer verificar. O quantificador existencial (E) foi incluso na lógica CTL, mas isso não faz com que a mesma tenha um poder de expressividade maior do que a lógica LTL. As expressividades de LTL e CTL são incomparáveis. Sistema de controle de uma aeronave Sistema de controle de uma usina nuclear Sistema de controle de tráfego aéreo Produção em massa de produtos eletrônicos. Programa de Estimativa de vendas Simulador de investimentos Principal aplicação Exemplos: "será sempre o caso que...“ será o caso que...“ "sempre foi o caso que...“ "foi o caso que..." Exemplos de implementações de verificação de modelos: SMV: Symbolic Model Verifier SMVNu: software livre SPIN UPPAAL: trata de tempo-real HYTECH: autômatos híbridos PRISM: autômatos estocásticos Lógicas temporais formalizam de modo natural problemas computacionais. A verificação das especificações de modelos pode ser feita automaticamente, através de provadores de teorema ou checagem de modelos. http://poesiagnosticaefilosofia.blogspot.com/2006/05/lgica-temporal-algo-descartavelfrente_12.html http://es.wikipedia.org/wiki/L%C3%B3gica_temporal http://pt.wikipedia.org/wiki/Regra_de_infer%C3%AAncia http://en.wikipedia.org/wiki/Temporal_logic http://plato.stanford.edu/entries/logic-temporal/ http://pt.wikibooks.org/wiki/L%C3%B3gica:_L%C3%B3gicas_N%C3%A3ocl%C3%A1ssicas:_Introdu%C3%A7%C3%A3o http://books.google.com.br/books?id=ZFY3S8iinfMC&pg=PA2842&lpg=PA2842&dq=l%C3%B3gica+t emporal&source=bl&ots=MomERmQf3j&sig=_bbRg7A7GNx8Tr8tZkvQNAgBXkQ&hl=ptBR&ei=HGB3SqCbMcmptgfVgc2WCQ&sa=X&oi=book_result&ct=result&resnum=9#v=onepage&q=l %C3%B3gica%20temporal&f=false http://www.itl.nist.gov/div897/sqg/dads/HTML/temporllogic.html http://lat.inf.tu-dresden.de/teaching/ss2006/tl/ http://books.google.com.br/books?id=ghy2CMU2FIoC&pg=PA995&lpg=PA995&dq=E.+Allen+Emers on:+Temporal+and+Modal+Logic.+In+J.+van+Leeuwen&source=bl&ots=5dMvWy4Aih&sig=XyaR2rJKHN7C4pTcbGgRioOM5o&hl=pt-BR&ei=Rox4SuBLYajtgfFh92WCQ&sa=X&oi=book_result&ct=result&resnum=1#v=onepage&q=&f=false Slides explicativos relacionados ao tema.