---
res:
bibo_abstract:
- Recently, there has been an effort to add quantitative objectives to formal verification
and synthesis. We introduce and investigate the extension of temporal logics with
quantitative atomic assertions. At the heart of quantitative objectives lies the
accumulation of values along a computation. It is often the accumulated sum, as
with energy objectives, or the accumulated average, as with 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 (or Boolean) 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 in time. We also allow the path-accumulation assertions LimInfAvg(v)
≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite
computation. We study the border of decidability for such quantitative 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 with both prefix-accumulation
assertions, or extending LTL with both path-accumulation assertions, results in
temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation
assertions may be generalized 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 this branching-time logic is,
in a sense, the maximal logic with one or both of the prefix-accumulation assertions
that permits a decidable model-checking procedure. Extending a temporal logic
that has the EG or EU modalities, such as CTL or 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.1145/2629686
bibo_issue: '4'
bibo_volume: 15
dct_date: 2014^xs_gYear
dct_language: eng
dct_publisher: ACM@
dct_title: Temporal specifications with accumulative values@
...