Frequency Linear-time Temporal Logic

Benedikt Bollig 1, 2 Normann Decker 3 Martin Leucker 3
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We propose fLTL, an extension to linear-time temporal logic (LTL) that allows for expressing relative frequencies by a generalization of temporal operators. This facilitates the specification of requirements such as the deadlines in a real-time system must be met in at least 95% of all cases. For our novel logic, we establish an undecidability result regarding the satisfiability problem but identify a decidable fragment which strictly increases the expressiveness of LTL by allowing, e.g., to express non-context-free properties.
Document type :
Conference papers
Liste complète des métadonnées
Contributor : Benedikt Bollig <>
Submitted on : Wednesday, January 16, 2013 - 10:51:38 AM
Last modification on : Thursday, January 11, 2018 - 6:23:37 AM

Links full text




Benedikt Bollig, Normann Decker, Martin Leucker. Frequency Linear-time Temporal Logic. Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12), 2012, Beijing, China. pp.85-92, ⟨10.1109/TASE.2012.43⟩. ⟨hal-00776769⟩



Record views