A CEGAR-like Approach for Cost LTL Bounds

TL;DR

This paper introduces a CEGAR-like algorithm for computing bounds of Cost LTL formulas, enabling practical model-checking of quantitative properties in discrete systems using automata-based techniques.

Contribution

It presents a novel CEGAR-inspired approach leveraging classical LTL model-checking and automata with counters to analyze quantitative bounds in Cost LTL.

Findings

The proposed method effectively computes bounds for Cost LTL formulas.

Automata with counters are used to implement the bounds computation.

This approach advances the practical application of discrete quantitative logics.

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\"{u}chi automata with counters to implement it. This method constitutes a first step towards the practical use of such a discrete quantitative logic.