Lógica temporal linear

Na lógica, lógica temporal linear ou linear-tempo lógico temporal (LTL) é um modal da lógica temporal com modalidades referindo-se ao tempo. Em LTL, pode-se codificar fórmulas sobre o futuro de caminhos, por exemplo, uma condição de, eventualmente, ser verdadeiro, a condição será verdadeira, até que outro fato torna-se verdadeiro, etc. É um fragmento do mais complexo CTL*, que além disso permite ramificações de tempo e quantificadores. Posteriormente LTL é às vezes chamado lógica proposicional temporal, abreviado PTL. Lógica Temporal Linear(LTL) é um fragmento de S1S.

LTL foi proposto pela primeira vez para a verificação formal de programas de computador por Amir Pnueli , em 1977.

Sintaxe

LTL é construída a partir de um conjunto finito de variáveis proposicionais AP, os operadores lógicos ¬ e ∨, e o operador modal temporal X (alguma literatura usa O ou N) e U. Formalmente, o conjunto de fórmulas LTL através de AP é definido indutivamente como se segue:

• se p ∈ AP , então p é uma fórmula LTL;
• se ψ e φ são fórmulas LTL, em seguida, ψ, φ ∨ ψ, X ψ e φ U ψ são fórmulas LTL.

X é lido como próximo e U é lido como até. Para além destes operadores fundamentais, existem operadores lógicos e temporais adicionais definidos em termos dos operadores fundamentais para escrever sucintamente fórmulas LTL. Os operadores lógicos adicionais são ∧, →, ← →, verdadeiro e falso. Seguem-se os operadores temporais adicionais.

• G para sempre (globalmente)
• F para, eventualmente, ( futuro)
• R para liberação
• W para fraca até

Semântica

Uma fórmula LTL pode ser satisfeita por uma sequência infinita de avaliações de verdade de variáveis em AP. Estas sequências podem ser vistos como uma palavra em um caminho de uma estrutura de Kripke ( ω-palavra sobre o alfabeto 2^AP). Deixe w = ₀,₁,₂,... ser um ω-palavra. Deixe w(i) = _i. Deixe wⁱ = _i,_i+1,..., que é um sufixo de w. Formalmente, a relação de satisfação entre uma palavra e uma fórmula LTL é definida da seguinte forma:

• w ⊨${\displaystyle }$p se p ∈ w(0)
• w ⊨${\displaystyle }$ψ se w ${\displaystyle }$ ψ
• w ⊨ φ ∨ ψ se w ${\displaystyle }$ φ ou w ${\displaystyle }$ ψ
• w ⊨${\displaystyle }$ X ψ se w¹ ⊨ ψ (No próximo passo de tempo ψ deve ser verdade)
• w ⊨ φ U ψ se existe i ≥ 0 tal que wⁱ ⊨ ψ e para todo 0 ≤ k < i, w^k ⊨ φ (φ deve manter-se fiel até ψ torna-se verdadeiro)

Dizemos que um ω-palavra w satisfaz uma fórmula LTL ψ quando w ⊨ ψ. O ω-linguagem L(ψ) definida por ψ é {w | w ⊨ ψ}, que é o conjunto de ω-palavras que satisfaz ψ. Uma fórmula ψ é satisfatível se existe um ω-palavra w tal que w ⊨ ψ. Uma fórmula ψ é válido se, para cada ω-palavra w sobre o alfabeto 2^AP, w ⊨ ψ.

O adicional de operadores lógicos são definidos da seguinte forma:

• φ ∧ ψ ≡ ¬(¬φ ∨¬ ψ)
• φ → ψ ≡ ¬φ ∨ ψ
• φ ↔ ψ ≡ (φ → ψ) ∧ ( ψ → φ)
• verdadeiro ≡ p ∨ ¬p, onde p ∈ AP
• falso ≡ ¬verdadeiro

Os operadores temporais adicionais R, F e G são definidas como se segue:

• φ R ψ ≡ ¬(¬φ U ¬ψ) ( ψ permanece verdadeiro até e incluindo uma vez que φ torna-se verdadeiro. Se φ nunca se tornar realidade, ψ deve permanecer verdadeiro para sempre.)
• F ψ ≡ verdadeiro U ψ (eventualmente ψ torna-se verdadeiro)
• G ψ ≡ falso R ψ ≡ ¬F ¬ψ (ψ permanece sempre verdadeiro)

Fraca até

Alguns autores também definem um fraco até que o operador binário, denotado W, com semântica semelhante ao do operador até, mas a condição de parada não é necessária para ocorrer (semelhante a liberação). às vezes é útil, pois ambos U e R pode ser definido em termos de fraca até:

• φ W ψ ≡ (φ U ψ) ∨ G φ ≡ φ U (ψ ∨ G φ) ≡ ψ R (ψ ∨ φ)
• φ U ψ ≡ Fψ ∧ (φ W ψ)
• φ R ψ ≡ ψ W (ψ ∧ φ)

A semântica para o temporal, os operadores são pictórica apresentado como segue.

Textual	Simbólico†	Explicação	Diagrama
Unary operators:
X $\phi$	$\bigcirc \phi$	neXt(Próximo): $\phi$ Tem de manter no próximo estado.
G $\phi$	$\Box \phi$	Globally( Globalmente): $\phi$ Tem que segurar todo o caminho subseqüente.
F $\phi$	$\Diamond \phi$	Finally(Finalmente): $\phi$ Eventualmente tem que segurar (em algum lugar no caminho subseqüente).
Binary operators:
$\psi$ U $\phi$	$\psi \;{\mathcal {U}}\,\phi$	Until(Até): $\psi$ Tem de manter pelo menos até $\phi$, Que se mantém na posição atual ou futura.
$\psi$ R $\phi$	$\psi \;{\mathcal {R}}\,\phi$	Release( Lançamento): $\phi$ Tem de ser verdade até e incluindo o ponto onde $\psi$ Primeiro se torna verdadeira; E se $\psi$Nunca se torna verdade, $\phi$ Deve permanecer verdadeiro para sempre.

Equivalências

Seja Φ, ψ, e ρ fórmulas LTL . As tabelas a seguir listam algumas das equivalências úteis que estendem as equivalências padrão entre os operadores lógicos usuais.

Distribuição
X (Φ ∨ ψ) ≡ (X, Φ) ∨ (X, ψ)	X (Φ ∧ ψ)≡ (X, Φ) ∧ (X, ψ)	X (Φ U ψ)≡ (X, Φ) U (X, ψ)
F (Φ ∨ ψ) ≡ (F Φ) ∨ (F ψ)	G (Φ ∧ ψ)≡ (G Φ) ∧ (G, ψ)
ρ U (Φ ∨ ψ) ≡ (ρ U Φ) ∨ (ρ U ψ)	(Φ ∧ ψ) U ρ ≡ (Φ U ρ) ∧ (ψ U ρ)

Negação de propagação
X Φ ≡ X Φ	G Φ ≡ F Φ	F Φ ≡ G Φ
(Φ U ψ) ≡ (Φ R ψ)	(Φ R ψ) ≡ (Φ U ψ)

Especial Temporal propriedades
F Φ ≡ F F Φ	G Φ ≡ G G Φ	Φ U ψ ≡ Φ U (Φ U ψ)
Φ U ψ ≡ ψ ∨ ( Φ ∧ X(Φ U ψ) )	Φ W ψ ≡ ψ ∨ ( Φ ∧ X(Φ W ψ) )	Φ R ψ ≡ ψ ∧ (Φ ∨ X(Φ R ψ) )
G Φ ≡ Φ ∧ X(G Φ)	F Φ ≡ Φ ∨ X(F Φ)

Negação forma normal

Todas as fórmulas LTL pode ser transformada em negação forma normal, onde

• todas as negações só aparecem na frente das proposições atômicas,
• apenas outros operadores lógicos verdadeiro, falso, ∧ e ∨ pode aparecer, e
• apenas temporais, operadores X, U, e, R pode aparecer.

Usando as equivalências acima para a propagação da negação, é possível derivar a forma normal. Esta forma normal permite - R, verdadeiro, falso, e ∧ a apareçam na fórmula, que não são operadores fundamentais de LTL. Note que a transformação para forma normal de negação não explode o tamanho da fórmula. Esta forma normal é útil na tradução de LTL para autômato Büchi.

Relações com outras lógicas

LTL pode ser equivalentes para à lógica monádica de primeira ordem FO[<]—um resultado conhecido como teorema de Kamp— ou línguas equivalentemente livres de estrelas.

Lógica de árvore de computação (CTL) e Lógica temporal linar (LTL) são ambas um subconjunto de CTL*, mas são incomparáveis. Por exemplo,

• Nenhuma fórmula CTL pode definir o idioma que é definido pela fórmula LTL F(G p).
• Nenhuma fórmula LTL pode definir o idioma que é definido pelo fórmulas CTL AG( p → (EXq ∧ EXq) ) ou AG(EF(P)).

No entanto, existe um subconjunto de CTL* que é superconjunto adequado de CTL e LTL.

Aplicações

Autômatos teórico lógica temporal linar modelo de verificação

Uma maneira importante de verificar o modelo é expressar propriedades desejadas (como as descritas acima) usando operadores LTL e realmente verificar se o modelo satisfaz esta propriedade. Uma técnica é obter um autômato Büchi que é equivalente ao modelo e outro que é equivalente à negação da propriedade (ver a lógica temporal linear ao autômato de Büchi) A intersecção dos dois não-determinísticos, autômatos de Büchi é vazia se o modelo satisfaz a propriedade.

Expressar propriedades importantes na verificação formal

Existem dois tipos principais de propriedades que podem ser expressas usando a lógica temporal linear: propriedades de segurança normalmente afirmam que algo ruim nunca acontece (G¬${\displaystyle }$), enquanto algo de bom continua acontecendo (GF${\displaystyle }$ ou G${\displaystyle }$F${\displaystyle }$)). Mas geralmente: propriedades de Segurança são aqueles para os quais cada contra-exemplo é um prefixo finito, que, no entanto, é expandido para a um caminho infinito, ainda é um contra-exemplo. Para a propriedade de vivacidade, por outro lado, cada prefixo finito de um contra-exemplo pode ser estendido para um caminho infinito que satisfaça a fórmula.

Especificação de linguagem

Uma das aplicações da lógica temporal linear é a especificação de preferências no Planejamento de Domínio da Linguagem de Definição para o propósito de preferência baseada em planejamento.^{[carece de fontes]}

Veja também

• Ação idioma