Discounting in LTL

DOI10.1007/978-3-642-54862-8_37MaRDI QIDQ5498739zbMATH OpenOpenAlexFDO

Authors Shaull Almagor, Udi Boker, Orna Kupferman

Publication date 10 February 2015

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1406.4249

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given specification, reasoning about quality addresses the question of emph{how well} the system satisfies the specification. One direction in this effort is to refine the "eventually" operators of temporal logic to {em discounting operators}: the satisfaction value of a specification is a value in $[0,1]$, where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is. In this paper we introduce an augmentation by discounting of Linear Temporal Logic (LTL), and study it, as well as its combination with propositional quality operators. We show that one can augment LTL with an arbitrary set of discounting functions, while preserving the decidability of the model-checking problem. Further augmenting the logic with unary propositional quality operators preserves decidability, whereas adding an average-operator makes some problems undecidable. We also discuss the complexity of the problem, as well as various extensions.

Recommendations

• Formally reasoning about quality
• Discounted duration calculus
• Formalizing and Reasoning about Quality
• Model checking discounted temporal properties
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(22)

• Quantitative model checking of linear-time properties based on generalized possibility measures
• Discounted duration calculus
• Quantitative vs. weighted automata
• Synthesis with rational environments
• Formally reasoning about quality
• Averaging in LTL
• scientific article; zbMATH DE number 2038772 (Why is no real title available?)
• Verification of systems with degradation
• LTL Can Be More Succinct
• Weighted linear dynamic logic
• Sensing as a complexity measure
• Tools and Algorithms for the Construction and Analysis of Systems
• Safely Freezing LTL
• On high-quality synthesis
• Reasoning about Quality and Fuzziness of Strategic Behaviors
• Weighted Linear Dynamic Logic
• Policy synthesis and reinforcement learning for discounted LTL
• Discounted-sum automata with multiple discount factors
• Discounted-sum automata with multiple discount factors
• Safety and liveness of quantitative automata
• Safety and liveness of quantitative properties and automata
• Formal verification and synthesis of mechanisms for social choice

This page was built for publication: Discounting in LTL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5498739)