Temporal Specifications with Accumulative Values
================================================
There is recently a significant effort to add quantitative objectives
to formal verification and synthesis. We introduce and investigate
the extension of temporal logics with quantitative atomic assertions,
aiming for a general and flexible framework for quantitative-oriented
specifications.
In the heart of quantitative objectives lies the accumulation of
values along a computation. It is either the accumulated summation, as
with the energy objectives, or the accumulated average, as with the
mean-payoff objectives. We investigate the extension of temporal
logics with the {\em prefix-accumulation assertions\/} $\Sum(v) \geq
c$ and $\Avg(v) \geq c$, where $v$ is a numeric variable of the
system, $c$ is a constant rational number, and $\Sum(v)$ and $\Avg(v)$
denote the accumulated sum and average of the values of $v$ from the
beginning of the computation up to the current point of time. We also
allow the {\em path-accumulation assertions\/} $\LimInfAvg(v)\geq c$
and $\LimSupAvg(v)\geq c$, referring to the average value along an
entire computation.
We study the border of decidability for extensions of various temporal
logics. In particular, we show that extending the fragment of CTL that
has only the EX, EF, AX, and AG temporal modalities by
prefix-accumulation assertions and extending LTL with
path-accumulation assertions, result in temporal logics whose
model-checking problem is decidable. The extended logics allow to
significantly extend the currently known energy and mean-payoff
objectives. Moreover, the prefix-accumulation assertions may be
refined with "controlled-accumulation", allowing, for example, to
specify constraints on the average waiting time between a request and
a grant. On the negative side, we show that the fragment we point to
is, in a sense, the maximal logic whose extension with
prefix-accumulation assertions permits a decidable model-checking
procedure. Extending a temporal logic that has the EG or EU
modalities, and in particular CTL and LTL, makes the problem
undecidable.