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.
Type de document :
Communication dans un congrès
Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12), 2012, Beijing, China. IEEE Computer Society Press, pp.85-92, 2012, 〈10.1109/TASE.2012.43〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776769
Contributeur : Benedikt Bollig <>
Soumis le : mercredi 16 janvier 2013 - 10:51:38
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

Identifiants

Collections

Citation

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. IEEE Computer Society Press, pp.85-92, 2012, 〈10.1109/TASE.2012.43〉. 〈hal-00776769〉

Partager

Métriques

Consultations de la notice

152