Timed temporal logics

Patricia Bouyer (1) , François Laroussinie (2) , Nicolas Markey (3) , Joël Ouaknine (4, 5) , James Worrell (5)

1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
3 SUMO - SUpervision of large MOdular and distributed systems
4 MPI-SWS - Max Planck Institute for Software Systems
5 OUCL - Computing Laboratory

Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressive-ness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.

Domaines: Logique en informatique [cs.LO]; Théorie et langage formel [cs.FL]

Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, James Worrell. Timed temporal logics. Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, LNCS-10460, Springer, pp.211-230, 2017, Lecture Notes in Computer Science, 978-3-319-63120-2. ⟨10.1007/978-3-319-63121-9_11⟩. ⟨hal-01566439⟩