--- 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@ ...