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
|
Betreuer | Leucker, Martin |
Eingabedatum | 14. Juli 2011 |
---|