Temporal Specifications with Accumulative Values
Temporal Specifications with Accumulative Values
复制标题
DOI：
10.1145/2629686
复制
发表时间：
2014-11-01
影响因子：
0.5
通讯作者：
Kupferman, Orna
中科院分区：
文献类型：
--
作者：
Boker, Udi;Chatterjee, Krishnendu;Kupferman, Orna
最近，人们努力在形式验证和综合中增加量化目标。我们引入并研究了带有定量原子断言的时态逻辑的扩展。定量目标的核心在于值的积累沿着计算。它通常是累计总和，如能源目标，或累计平均值，如平均收益目标。我们研究了带有前缀累加断言Sum（v）>= c和Avg（v）>= c的时态逻辑的扩展，其中v是系统的数值（或布尔）变量，c是常数有理数，Sum（v）和Avg（v）表示从计算开始到当前时间点的v值的累加和和平均值。我们还允许路径累积断言LimInfAvg（v）>= c和LimSupAvg（v）>= c，指的是沿着整个无限计算的平均值。我们研究了各种时态逻辑的这种定量扩展的可判定性边界。特别是，我们表明，扩展CTL的片段，只有EX，EF，AX和AG的时间模态与前缀积累断言，或扩展LTL与路径积累断言，结果在时间逻辑的模型检查问题是可判定的。此外，前缀累积断言可以用“controlledaccumulation”来概括，从而允许例如指定对请求和授权之间的平均等待时间的约束。在消极的一面，我们表明，这个分支时间逻辑是，在某种意义上说，最大的逻辑与一个或两个前缀积累断言，允许一个可判定的模型检查过程。扩展具有EG或EU模态的时态逻辑，例如CTL或LTL，使问题不可判定。
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 "controlledaccumulation," 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.