---
res:
  bibo_abstract:
  - 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 prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ 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
    path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Udi
      foaf_name: Boker, Udi
      foaf_surname: Boker
      foaf_workInfoHomepage: http://www.librecat.org/personId=31E297B6-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Orna
      foaf_name: Kupferman, Orna
      foaf_surname: Kupferman
  bibo_doi: 10.15479/AT:IST-2011-0003
  dct_date: 2011^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2664-1690
  dct_language: eng
  dct_publisher: IST Austria@
  dct_title: Temporal specifications with accumulative values@
...