Affordable Access

Temporal Logic for Properties with Relative Frequency

Authors
Publication Date
Source
Universität Stuttgart, Fakultät 5, Germany, Computer Science Archive
Keywords
License
Unknown
External links

Abstract

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

Statistics

Seen <100 times