Please use this identifier to cite or link to this item: http://dx.doi.org/10.18419/opus-2727
Authors: Decker, Normann
Title: Temporal logic for properties with relative frequency
Issue Date: 2011
metadata.ubs.publikation.typ: Abschlussarbeit (Diplom)
URI: http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-66043
http://elib.uni-stuttgart.de/handle/11682/2744
http://dx.doi.org/10.18419/opus-2727
Abstract: Inherently unreliable or fault-tolerant systems demand for a specification formalism that allows the user to express a required ratio of certain observations. Such a requirement can be, e.g. that deadlines in a real-time system must be met in at least 80% of all cases. Logics and in particular temporal logics provide powerful, flexible and well established specification formalisms. We therefore propose fLTL, an extension to linear-time temporal logic that allows for expressing relative frequencies by an intuitive generalization of the temporal operators. We develop a game theoretical methodology and a semantics for temporal logic with counters. For our novel logic, we establish an undecidability result regarding the satisfiability problem but identify a decidable fragment which strictly increases the expressiveness of linear-time temporal logic by allowing, e.g., to express non-context-free properties.
Appears in Collections:05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Files in This Item:
File Description SizeFormat 
DIP_3125.pdf546,67 kBAdobe PDFView/Open


Items in OPUS are protected by copyright, with all rights reserved, unless otherwise indicated.