You are here

Home › Research › Publications ›

Frequency Linear-time Temporal Logic

TitleFrequency Linear-time Temporal Logic
Publication TypeConference Paper
Year of Publication2012
AuthorsBenedikt Bollig, Decker, N, Leucker, M
Conference NameSixth IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2012)
PublisherIEEE Computer Society
Conference LocationBeijing, China
Keywordsavailability, counters, frequency, LTL, specification, 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\% 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.
Refereed DesignationRefereed
Bibtex: 
@inproceedings {742,
	title = {Frequency Linear-time Temporal Logic},
	booktitle = {Sixth IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2012)},
	year = {2012},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Beijing, China},
	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.
},
	keywords = {availability, counters, frequency, LTL, specification, temporal logic},
	author = {Benedikt Bollig and Normann Decker and Martin Leucker}
}