A CEGAR-like Approach for Cost LTL Bounds
Citations Over Time
Abstract
Qualitative formal verification, that seeks boolean answers about the behavior of a system, is often insufficient for practical purposes. Observing quantitative information is of interest, e.g. for the proper calibration of a battery or a real-time scheduler. Historically, the focus has been on quantities in a continuous domain, but recent years showed a renewed interest for discrete quantitative domains. Cost Linear Temporal Logic (CLTL) is a quantitative extension of classical LTL. It integrates into a nice theory developed in the past few years that extends the qualitative setting, with counterparts in terms of logics, automata and algebraic structure. We propose a practical usage of this logics for model-checking purposes. A CLTL formula defines a function from infinite words to integers. Finding the bounds of such a function over a given set of words can be seen as an extension of LTL universal and existential model-checking. We propose a CEGAR-like algorithm to find these bounds by relying on classical LTL model-checking, and use Büchi automata with counters to implement it. This method constitutes a first step towards the practical use of such a discrete quantitative logic.
Related Papers
- → Model checking for extended timed temporal logics(1996)19 cited
- → Improving Pattern-Based LTL Formulas for Automata Model Checking(2008)3 cited
- Logics for Mazurkiewicz Traces(2002)
- A Model Checking of Real-Time Systems in Linear Temporal Logic with Clocks(2002)
- Linear Temporal Logic and Buchi Automata(2009)