Logique temporelle linéaire

En logique, la logique temporelle linéaire^[1],[2] (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais)^[3]. La logique temporelle linéaire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur.

LTL a d'abord été proposé pour la vérification formelle des programmes informatiques par Amir Pnueli en 1977^[4].

Syntaxe

La LTL est construite à partir d'un ensemble fini de variables propositionnelles AP, opérateurs logiques ¬ et ∨, et des opérateurs temporels modaux X (certaines notations utilisent O ou N) et U. Formellement, l'ensemble des formules de LTL sur AP est inductivement défini comme suit :

• si p ∈ AP alors p est une formule de LTL ;
• si ψ et φ sont des formules de LTL alors ¬ψ, φ ∨ ψ, X ψ, et φ U ψ sont des formules de LTL^[5].

X est lu comme suivant (next en anglais) et U est lu comme jusqu'à (until en anglais). On peut ajouter d'autres opérateurs, non nécessaires mais qui simplifient l'écriture de certaines formules.

Par exemple, les opérateurs logiques ∧, →, ↔, vrai et faux sont généralement ajoutés. Les opérateurs temporels ci-dessous le sont également :

• G pour toujours (globalement (globally en anglais)) ;
• F pour finalement (dans le futur (in the future en anglais)) ;
• R pour libération (release en anglais) ;
• W pour faible jusqu'à (weak until en anglais).

Sémantique

Une formule de LTL peut être satisfaite par une suite infinie d'évaluations de vérité des variables dans AP. Soit w = a₀,a₁,a₂,... tel un mot-ω. Soit w(i) = a_i. Soit wⁱ = a_i,a_i+1,..., qui est un suffixe de w. Formellement, la relation de satisfaction ${\displaystyle \vDash }$ entre un mot et une formule de LTL est définie comme suit :

• w ${\displaystyle \vDash }$ p si p ∈ w(0)
• w ${\displaystyle \vDash }$ ¬ψ si w ${\displaystyle \nvDash }$ ψ
• w ${\displaystyle \vDash }$ φ ∨ ψ si w ${\displaystyle \vDash }$ φ ou w ${\displaystyle \vDash }$ ψ
• w ${\displaystyle \vDash }$ X ψ si w¹ ${\displaystyle \vDash }$ ψ (ψ doit être vrai à l'étape suivante)
• w ${\displaystyle \vDash }$ φ U ψ s'il existe i ≥ 0 tel que wⁱ ${\displaystyle \vDash }$ ψ et pour tout 0 ≤ k < i, w^k ${\displaystyle \vDash }$ φ (φ doit rester vrai jusqu'à ce que ψ devienne vrai)

On dit qu'un mot-ω w satisfait une formule LTL ψ quand w ${\displaystyle \vDash }$ ψ.

Les opérateurs logiques supplémentaires sont définis comme suit :

• φ ∧ ψ ≡ ¬(¬φ ∨ ¬ψ)
• φ → ψ ≡ ¬φ ∨ ψ
• φ ↔ ψ ≡ (φ → ψ) ∧ ( ψ → φ)
• vrai ≡ p ∨ ¬p, où p ∈ AP
• faux ≡ ¬vrai

Les opérateurs temporels supplémentaires R, F et G sont définis comme suit :

• φ R ψ ≡ ¬(¬φ U ¬ψ)
• F ψ ≡ vrai U ψ (ψ devient éventuellement vrai)
• G ψ ≡ faux R ψ ≡ ¬F ¬ψ (ψ reste toujours vrai)

La sémantique des opérateurs temporels peut se représenter comme suit :

Opérateur	Symbole alternatif[N 1]	Explication	Diagramme
Opérateurs unaires :
X ${\displaystyle \phi }$	${\displaystyle \bigcirc \phi }$	suivant (neXt) : ${\displaystyle \phi }$ doit être satisfaite dans l'état suivant.
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	Globalement : ${\displaystyle \phi }$ doit être satisfaite dans l'intégralité des états futurs.
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	Finalement : ${\displaystyle \phi }$ doit être satisfaite dans un état futur.
Opérateurs binaires:
${\displaystyle \psi }$ U ${\displaystyle \phi }$	${\displaystyle \psi \;{\mathcal {U}}\,\phi }$	Jusqu'à (Until) : ${\displaystyle \psi }$ doit être satisfaite dans tous les états jusqu'à un état où ${\displaystyle \phi }$ est satisfaite, non inclus.
${\displaystyle \psi }$ R ${\displaystyle \phi }$	${\displaystyle \psi \;{\mathcal {R}}\,\phi }$	Réaliser : ${\displaystyle \phi }$ doit être satisfaite dans tous les états tant que ${\displaystyle \psi }$ n'est pas satisfaite. Si ${\displaystyle \psi }$ n'est jamais satisfaite, ${\displaystyle \phi }$ doit être vraie partout.

Équivalences

Soit Φ, ψ, et ρ des formules de LTL. Les tableaux suivants présentent des équivalences utiles.

Distributivité
X (Φ ∨ ψ) ≡ (X Φ) ∨ (X ψ)	X (Φ ∧ ψ)≡ (X Φ) ∧ (X ψ)	X (Φ U ψ)≡ (X Φ) U (X ψ)
F (Φ ∨ ψ) ≡ (F Φ) ∨ (F ψ)	G (Φ ∧ ψ)≡ (G Φ) ∧ (G ψ)
ρ U (Φ ∨ ψ) ≡ (ρ U Φ) ∨ (ρ U ψ)	(Φ ∧ ψ) U ρ ≡ (Φ U ρ) ∧ (ψ U ρ)

Négation
¬X Φ ≡ X ¬Φ	¬G Φ ≡ F ¬Φ	¬F Φ ≡ G ¬Φ
¬ (Φ U ψ) ≡ (¬Φ R ¬ψ)	¬ (Φ R ψ) ≡ (¬Φ U ¬ψ)

Propriétés temporelles spéciales
F Φ ≡ F F Φ	G Φ ≡ G G Φ	Φ U ψ ≡ Φ U (Φ U ψ)
Φ U ψ ≡ ψ ∨ ( Φ ∧ X(Φ U ψ) )	Φ W ψ ≡ ψ ∨ ( Φ ∧ X(Φ W ψ) )	Φ R ψ ≡ ψ ∧ (Φ ∨ X(Φ R ψ) )
G Φ ≡ Φ ∧ X(G Φ)	F Φ ≡ Φ ∨ X(F Φ)

Forme normale négative

Toutes les formules de LTL peuvent être transformées en forme normale négative, où

• toutes les négations apparaissent seulement en face des propositions atomiques,
• seuls les opérateurs logiques vrai, faux, ∧ et ∨ peuvent apparaître, et
• seuls les opérateurs logiques X, U, et R peuvent apparaître.

Automates de Büchi

Toute formule LTL est équivalente à un automate de Büchi de taille au plus exponentielle en la taille de la formule^[6]. Pour LTL sur les traces finies, appelée LTLf, toute formule est équivalente à un automate fini non déterministe de taille au plus exponentielle en la taille de la formule^[7].

Problèmes algorithmiques

Le model checking et le problème de satisfiabilité est PSPACE-complet. La synthèse LTL et le problème de vérification d'un jeu avec un objectif LTL sont 2EXPTIME-complet^[8].

Apprentissage par renforcement

Les buts des agents sont parfois écrits en LTL, à la fois pour des approches avec modèles^[9],[10] ou sans^{[11],[12],[13]}.

Extensions

Quantification du second ordre

Dans le chapitre 3 de sa thèse^[14], Sistla étend LTL en rajoutant des quantifications du second ordre. À l'époque LTL se nommait plutôt PTL (pour propositional temporal logic). Cette extension s'appelle QPTL (quantified propositional temporal logic). Par exemple ${\displaystyle \exists p,\forall q,G(p\leftrightarrow Xq)}$ est une formule de QPTL qui se lit "il existe une façon de donner des valeurs à la proposition p sur toute la ligne temporelle, telle que quelle que soit la façon d'attribuer les valeurs à la proposition q sur toute la ligne temporelle, on a toujours que p est équivalent au fait que demain q". Sistla, dans le chapitre 3 de sa thèse, démontre que décider si une formule sous forme prénexe et avec une seule alternation de QPTL est vraie est EXPSPACE-complet.

Comme mentionné par Sistla et al.^[15], on peut réduire S1S qui est non-élémentaire^[16] à QPTL. La véracité d'une formule de QPTL est donc non-élémentaire. Plus précisément, Sistla et al.^[15] démontrent que le problème de véracité de QPTL restreint aux formules avec k alternations est kNEXPSPACE-complet.

Voir aussi

• Logique linéaire
• Logique ternaire

Notes et références

Notes

1. Ces symboles sont parfois utilisés dans la littérature pour désigner ces opérateurs.

Références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Linear temporal logic » (voir la liste des auteurs).

1. Logic in Computer Science: Modelling and Reasoning about Systems: page 175
2. Linear-time Temporal Logic
3. (en) Dov M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional modal logics : theory and applications, Amsterdam/Boston, Elsevier, 2003 (ISBN 978-0-444-50826-3, lire en ligne), p. 46
4. Amir Pnueli, The temporal logic of programs.
5. Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press [1]
6. Christel Baier et Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 31 mai 2008, 975 p. (ISBN 978-0-262-02649-9 et 0-262-02649-X, lire en ligne)
7. Giuseppe De Giacomo et Moshe Y. Vardi, « Synthesis for LTL and LDL on finite traces », IJCAI, AAAI Press,‎ 25 juillet 2015, p. 1558–1564 (ISBN 9781577357384, lire en ligne, consulté le 7 février 2018)
8. (en) A. Pnueli et R. Rosner, « On the synthesis of a reactive module », 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (conférence),‎ 1989 (lire en ligne, consulté le 7 novembre 2019)
9. Jie Fu et Ufuk Topcu, « Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints », arXiv:1404.7073 [cs],‎ 28 avril 2014 (lire en ligne, consulté le 5 décembre 2019)
10. D. Sadigh, E. S. Kim, S. Coogan et S. S. Sastry, « A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications », 53rd IEEE Conference on Decision and Control,‎ décembre 2014, p. 1091–1096 (DOI 10.1109/CDC.2014.7039527, lire en ligne, consulté le 5 décembre 2019)
11. (en) Giuseppe De Giacomo, Luca Iocchi, Marco Favorito et Fabio Patrizi, « Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf Restraining Specifications », Proceedings of the International Conference on Automated Planning and Scheduling, vol. 29,‎ 6 juillet 2019, p. 128–136 (ISSN 2334-0843, lire en ligne, consulté le 5 décembre 2019)
12. Mohammadhosein Hasanbeig, Alessandro Abate et 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, lire en ligne, consulté le 5 décembre 2019)
13. Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Valenzano et Sheila A. McIlraith, « Teaching Multiple Tasks to an 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 (lire en ligne, consulté le 5 décembre 2019)
14. « Theoretical issues in the design and verification of distributed systems | Guide books », sur dl.acm.org (DOI 10.5555/911361, consulté le 7 février 2020)
15. (en) A. Prasad Sistla, Moshe Y. Vardi et Pierre Wolper, « The complementation problem for Büchi automata with applications to temporal logic », Theoretical Computer Science, vol. 49, n^o 2,‎ 1^er janvier 1987, p. 217–237 (ISSN 0304-3975, DOI 10.1016/0304-3975(87)90008-9, lire en ligne, consulté le 7 février 2020)
16. « WEAK MONADIC SECOND ORDER THEORY OF SUCCESSOR IS NOT ELEMENTARY-RECURSIVE | Guide books », sur dl.acm.org (DOI 10.5555/889571, consulté le 7 février 2020)

Liens externes

• Une présentation de la LTL
• Linear-Time Temporal Logic and Büchi Automata
• LTL Teaching slides, Free University of Bozen-Bolzano
• LTL to Buchi translation algorithms, Spot