Lógica temporal linear

Na lógica , a lógica temporal linear ( LTL ) é uma lógica temporal modal com modalidades referentes ao tempo. Em LTL, pode-se codificar fórmulas sobre o futuro de um caminho infinito em um sistema de transições, por exemplo, uma condição acabará sendo verdadeira, uma condição será verdadeira até que outra se torne verdadeira, etc. Essa lógica é mais fraca do que a lógica CTL * , que permite que as condições sejam expressas em ramificações de caminhos e não apenas em um único caminho. O LTL também é algumas vezes chamado de lógica proposicional temporal , abreviado LTP ( PTL em inglês). A lógica linear temporal (LTL) é um fragmento de S1S (para segunda ordem com 1 sucessor), lógica monádica de segunda ordem com um sucessor.

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

Sintaxe

LTL é construído a partir de um conjunto finito de variáveis proposicional AP , operadores lógicos ¬ e ∨ e operadores temporais modal X (algumas notações usar S ou N ) e L . Formalmente, o conjunto de fórmulas de LTL em AP é indutivamente definido como segue:

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

X é lido como próximo ( ne x t em Inglês) e U é lido como até ( u té em Inglês). Podemos adicionar outros operadores, não necessários, mas que simplificam a escrita de certas fórmulas.

Por exemplo, os operadores lógicos ∧, →, ↔, verdadeiro e falso são geralmente adicionados. Os operadores temporais abaixo também são:

G para sempre ( g verall ( g lobally inglês));
F finalmente (na f utur ( na f uture Inglês));
R para liberação ( r elease em inglês);
W para fraco até ( w eak até em inglês).

Semântica

Uma fórmula LTL pode ser satisfeita por uma série infinita de avaliações verdade das variáveis em AP . Seja w = a 0 , a 1 , a 2 , ... tal palavra-ω. Seja w (i) = a i . Seja w i = a i , a 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: ${\ displaystyle \ vDash}$

w p se p ∈ w (0) ${\ displaystyle \ vDash}$
w ¬ψ se w ψ ${\ displaystyle \ vDash}$ ${\ displaystyle \ nvDash}$
w φ ∨ ψ se w φ ou w ψ ${\ displaystyle \ vDash}$ ${\ displaystyle \ vDash}$ ${\ displaystyle \ vDash}$
w X ψ se w 1 ψ (ψ deve ser verdadeiro na próxima etapa ) ${\ displaystyle \ vDash}$ ${\ displaystyle \ vDash}$
w φ U ψ se existe i ≥ 0 tal que w i ψ e para todo 0 ≤ k <i, w k φ (φ deve permanecer verdadeiro até que ψ se torne verdadeiro) ${\ displaystyle \ vDash}$ ${\ displaystyle \ vDash}$ ${\ displaystyle \ vDash}$

Dizemos que uma palavra-ω w satisfaz uma fórmula LTL ψ quando w ψ. ${\ displaystyle \ vDash}$

Operadores lógicos adicionais são definidos da seguinte forma:

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

Os operadores de tempo adicional R , F e G são definidos da seguinte forma:

φ R ψ ≡ ¬ (¬φ U ¬ψ)
F ψ ≡ U verdadeiro ψ (ψ eventualmente torna-se verdadeiro)
G ψ ≡ falso R ψ ≡ ¬ F ¬ψ (ψ sempre permanece verdadeiro)

A semântica dos operadores temporais pode ser representada da seguinte forma:

Operador	Símbolo alternativo	Explicação
Operadores unários :
X $\ phi$	${\ displaystyle \ bigcirc \ phi}$	próximo: deve ser satisfeito no próximo estado. $\ phi$
G $\ phi$	${\ displaystyle \ Box \ phi}$	G verall: deve ser cumprido em todos os estados futuros. $\ phi$
F $\ phi$	${\ displaystyle \ Diamond \ phi}$	F inalmente: deve ser satisfeita em um estado futuro. $\ phi$
Operadores binários :
$\ psi$ você $\ phi$	${\ displaystyle \ psi \; {\ mathcal {U}} \, \ phi}$	Até: deve ser satisfeito em todos os estados até um determinado estado ou está satisfeito, não incluído. $\ psi$ $\ phi$
$\ psi$ R $\ phi$	${\ displaystyle \ psi \; {\ mathcal {R}} \, \ phi}$	R o alcançar: estar satisfeito em todos os estados como não está satisfeito. $\ phi$ $\ psi$ Se nunca está satisfeito, deve ser verdadeiro em todos os lugares. $\ psi$ $\ phi$

Equivalências

Sejam Φ, ψ e ρ fórmulas LTL. As tabelas a seguir mostram equivalências úteis.

Distributividade
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
¬ X Φ ≡ X ¬Φ	¬ G Φ ≡ F ¬Φ	¬ F Φ ≡ G ¬Φ
¬ (Φ U ψ) ≡ (¬Φ R ¬ψ)	¬ (Φ R ψ) ≡ (¬Φ U ¬ψ)

Propriedades temporais especiais
F Φ ≡ F F Φ	G Φ ≡ G G Φ	Φ U ψ ≡ Φ U (Φ U ψ)
Φ U ψ ≡ ψ ∨ (Φ ∧ X (Φ U ψ))	Φ W ψ ≡ ψ ∨ (Φ ∧ X (Φ W ψ))	Φ R ψ ≡ ψ ∧ (Φ ∨ X (Φ R ψ))
G Φ ≡ Φ ∧ X ( G Φ)	F Φ ≡ Φ ∨ X ( F Φ)

Forma normal negativa

Todas as fórmulas LTL podem ser transformadas na forma normal negativa , onde

todas as negações aparecem apenas na frente de proposições atômicas,
apenas os operadores lógicos verdadeiro , falso , ∧ e ∨ podem aparecer, e
apenas os operadores lógicos X , U e R podem aparecer.

Autômatos Büchi

Qualquer fórmula LTL é equivalente a um autômato de Büchi de tamanho no máximo exponencial no tamanho da fórmula. Para LTL sobre traços finitos, chamados LTLf, qualquer fórmula é equivalente a um autômato finito não determinístico de tamanho no máximo exponencial no tamanho da fórmula.

Problemas de algoritmo

A verificação do modelo e o problema de satisfatibilidade são PSPACE-completos. A síntese LTL e o problema de verificação de um jogo com uma meta LTL estão concluídos em 2EXPTIME.

Aprendizagem por reforço

As metas do agente às vezes são escritas em LTL, para abordagens de modelos e não modelos.

Extensões

Quantização de segunda ordem

No capítulo 3 de sua tese, Sistla estende LTL adicionando quantificações de segunda ordem. Na época, LTL era chamado de PTL (para lógica temporal proposicional ). Essa extensão é chamada de QPTL ( lógica temporal proposicional quantificada ). Por exemplo, é uma fórmula de QPTL que diz "há uma maneira de dar valores à proposição p ao longo de toda a linha do tempo, como independentemente de como atribuir valores à proposição q ao longo de toda a linha do tempo, sempre temos que p é equivalente ao fato de que amanhã q ". Sistla, no capítulo 3 de sua tese, demonstra que decidir se uma fórmula em forma de apêndice e com uma única alternância de QPTL é verdadeira é EXPSPACE-complete. ${\ displaystyle \ existe p, \ forall q, G (p \ leftrightarrow Xq)}$

Conforme mencionado por Sistla et al., Pode-se reduzir S1S que não é elementar para QPTL. A veracidade de uma fórmula QPTL é, portanto, não elementar. Mais especificamente, Sistla et al. mostram que o problema de veracidade de QPTL restrito a fórmulas com k alternâncias é kNEXPSPACE-completo.

Veja também

Notas e referências

Notas

Esses símbolos são algumas vezes usados na literatura para designar esses operadores.

Referências

(fr) Este artigo foi retirado parcial ou totalmente do artigo da Wikipedia em inglês intitulado " Linear temporal logic " ( veja a lista de autores ) .

Lógica em ciência da computação: modelagem e raciocínio sobre sistemas: página 175
Lógica Temporal de Tempo Linear
(em) Dov M. Gabbay , A. Kurucz, F. Wolter, Sr. Zakharyaschev, Lógica modal multidimensional: teoria e aplicações , Amsterdam / Boston, Elsevier ,2003( ISBN 978-0-444-50826-3 , leitura online ) , p. 46
Amir Pnueli , A lógica temporal dos programas.
Sec. 5.1 de Christel Baier e Joost-Pieter Katoen, Principles of Model Checking, MIT Press [1]
Christel Baier e Joost-Pieter Katoen , Principles of Model Checking (Representation and Mind Series) , The MIT Press ,31 de maio de 2008, 975 p. ( ISBN 978-0-262-02649-9 e 0-262-02649-X , leia online )
Giuseppe De Giacomo e Moshe Y. Vardi , " Synthesis for LTL and LDL on finite traces ", IJCAI , AAAI Press,25 de julho de 2015, p. 1558–1564 ( ISBN 9781577357384 , lido online , acessado em 7 de fevereiro de 2018 )
(em) A. Pnueli e R. Rosner, " Na síntese de uma unidade reativa " , 16º Simpósio ACM é SIGPLAN-SIGACT Princípios de linguagens de programação (conferência) ,1989( leia online , consultado em 7 de novembro de 2019 )
Jie Fu e Ufuk Topcu , " Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints ", arXiv: 1404.7073 [cs] ,28 de abril de 2014( leia online , consultado em 5 de dezembro de 2019 )
D. Sadigh , ES Kim , S. Coogan e SS Sastry , " Uma abordagem baseada em aprendizagem para controlar a síntese de processos de decisão de Markov para especificações de lógica temporal linear ", 53ª Conferência IEEE sobre Decisão e Controle ,dezembro de 2014, p. 1091–1096 ( DOI 10.1109 / CDC.2014.7039527 , ler online , acessado em 5 de dezembro de 2019 )
(in) Giuseppe De Giacomo Luca Iocchi Marco Favorito e Fabio Patrizi , " Fundamentos para parafusos de restrição: Aprendizagem por reforço com especificações de restrição LTLf / LdlF " , Anais da Conferência Internacional sobre Planejamento e Programação Automatizada , vol. 29,6 de julho de 2019, p. 128–136 ( ISSN 2334-0843 , lido online , acessado em 5 de dezembro de 2019 )
Mohammadhosein Hasanbeig , Alessandro Abate e Daniel Kroening , " Logically-Constrained Neural Fitted Q-iteration ", Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems , International Foundation for Autonomous Agents and Multiagent Systems, aAMAS '19,2019, p. 2012–2014 ( ISBN 978-1-4503-6309-9 , lido online , acessado em 5 de dezembro de 2019 )
Rodrigo Toro Icarte , Toryn Q. Klassen , Richard Valenzano e Sheila A. McIlraith , “ Teaching Multiple Tasks to a RL Agent Using LTL ”, Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems , International Foundation for Autonomous Agents and Multiagent Systems, aAMAS '18,2018, p. 452-461 ( ler online , consultado em 5 de dezembro de 2019 )
“ Questões teóricas na concepção e verificação de sistemas distribuídos | Guide books ” , em dl.acm.org ( DOI 10.5555 / 911361 , acessado em 7 de fevereiro de 2020 )
(en) A. Prasad Sistla , Moshe Y. Vardi e Pierre Wolper , “ O problema de complementação para autômatos de Büchi com aplicações para lógica temporal ” , Theoretical Computer Science , vol. 49, n o 21 ° de janeiro de 1987, p. 217-237 ( ISSN 0304-3975 , DOI 10.1016 / 0304-3975 (87) 90008-9 , ler online , acessado em 7 de fevereiro de 2020 )
" FRACA TEORIA MONADICA DE SEGUNDA ORDEM DO SUCESSOR NÃO É ELEMENTAR-RECURSIVA | Guide books ” , em dl.acm.org ( DOI 10.5555 / 889571 , acessado em 7 de fevereiro de 2020 )

links externos