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

Institute of Software Engineering and Programming Languages

CNRS and Inria

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.

Original language	English
Title of host publication	2012 Sixth International Symposium on Theoretical Aspects of Software Engineering
Number of pages	8
Publisher	IEEE
Publication date	05.10.2012
Pages	85-92
Article number	6269631
ISBN (Print)	978-1-4673-2353-6
DOIs	https://doi.org/10.1109/TASE.2012.43
Publication status	Published - 05.10.2012
Event	IEEE 6th International Symposium on Theoretical Aspects of Software Engineering - Beijing , China Duration: 04.07.2012 → 06.07.2012 Conference number: 92946

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1109/TASE.2012.43

Cite this

@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/record/display.uri?eid=2-s2.0-84866924495&origin=inward&txGid=3185b000c7d9b5cede0278b6bc03f94e

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

Access to Document

Other files and links

Fingerprint

Cite this