Temporal specifications with accumulative values Journal Article

Author(s): Boker, Udi; Chatterjee, Krishnendu; Henzinger, Thomas A; Kupferman, Orna
Article Title: Temporal specifications with accumulative values
Affiliation IST Austria
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.
Keywords: model checking; Temporal logic; specification; Formal verification; Accumulation; Nondeterminism
Journal Title: ACM Transactions on Computational Logic (TOCL)
Volume: 15
Issue 4
ISSN: 1557-945X
Publisher: ACM  
Date Published: 2014-09-16
Start Page: Article number: 27
DOI: 10.1145/2629686
Notes: The research was supported in part by the Austrian Science Fund (FWF) grant no. P23499-N23, FWF NFN grants S11402-N23 and S11407-N23 (RiSE: Rigorous Systems Engineering), ERC Starting grant 279307 (Graph Games), ERC Starting grant 278410 (QUALITY), ERC Advanced Grant 267989 (QUAREM: Quantitative Reactive Modeling), and Microsoft faculty fellows award. We thank Dejan Nickovic for stimulating discussions on controlled accumulation, Yaron Velner for discussions that led to improving the complexity of LTLlim
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Udi Boker
    12 Boker
Related IST Austria Work