Diplomarbeit DIP-3125

Bibliograph.
Daten
Decker, Normann: Temporal Logic for Properties with Relative Frequency.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Diplomarbeit Nr. 3125 (2011).
84 Seiten, englisch.
CR-Klassif.F.4.1 (Mathematical Logic)
D.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
Kurzfassung

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.

Keywords. Specification and Verification, Temporal Logic, Relative Frequency, Availability, Counter Logic

Volltext und
andere Links
PDF (559793 Bytes)
Abteilung(en)Universität Stuttgart, Institut für Formale Methoden der Informatik, Theoretische Informatik
BetreuerLeucker, Martin
Eingabedatum14. Juli 2011
   Publ. Informatik