Frequency Linear-time Temporal Logic

Benedikt Bollig; Normann Decker; Martin Leucker

doi:10.1109/TASE.2012.43

Frequency Linear-time Temporal Logic

Benedikt Bollig, Normann Decker, Martin Leucker

Institut für Softwaretechnik und Programmiersprachen

CNRS and Inria

17 Zitate (Scopus)

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 percent 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.

Originalsprache	Englisch
Titel	2012 Sixth International Symposium on Theoretical Aspects of Software Engineering
Seitenumfang	8
Herausgeber (Verlag)	IEEE
Erscheinungsdatum	05.10.2012
Seiten	85-92
Aufsatznummer	6269631
ISBN (Print)	978-1-4673-2353-6
DOIs	https://doi.org/10.1109/TASE.2012.43
Publikationsstatus	Veröffentlicht - 05.10.2012
Veranstaltung	IEEE 6th International Symposium on Theoretical Aspects of Software Engineering - Beijing , China Dauer: 04.07.2012 → 06.07.2012 Konferenznummer: 92946

UN SDGs

Dieser Output leistet einen Beitrag zu folgendem(n) Ziel(en) für nachhaltige Entwicklung

SDG 9 – Industrie, Innovation und Infrastruktur

Dokumente

10.1109/TASE.2012.43

Weitere Links

https://www.scopus.com/pages/publications/84866924495

Zitieren

@inproceedings{3381f3ea40a84542b590744e0d032c9c,

title = "Frequency Linear-time Temporal Logic",

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 percent 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.",

author = "Benedikt Bollig and Normann Decker and Martin Leucker",

year = "2012",

month = oct,

day = "5",

doi = "10.1109/TASE.2012.43",

language = "English",

isbn = "978-1-4673-2353-6",

series = "IEEE Proceedings",

publisher = "IEEE",

pages = "85--92",

booktitle = "2012 Sixth International Symposium on Theoretical Aspects of Software Engineering",

note = "IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012 ; Conference date: 04-07-2012 Through 06-07-2012",

}

TY - GEN

T1 - Frequency Linear-time Temporal Logic

AU - Bollig, Benedikt

AU - Decker, Normann

AU - Leucker, Martin

N1 - Conference code: 92946

PY - 2012/10/5

Y1 - 2012/10/5

N2 - 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 percent 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.

AB - 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 percent 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.

UR - https://www.scopus.com/pages/publications/84866924495

U2 - 10.1109/TASE.2012.43

DO - 10.1109/TASE.2012.43

M3 - Conference contribution

SN - 978-1-4673-2353-6

T3 - IEEE Proceedings

SP - 85

EP - 92

BT - 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering

PB - IEEE

T2 - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering

Y2 - 4 July 2012 through 6 July 2012

ER -

Frequency Linear-time Temporal Logic

Abstract

UN SDGs

Dokumente

Weitere Links

Fingerprint

Zitieren