Temporal Logics and Probabilistic Model Checking for Weighted Structures

在分析资源意识和系统的其他定量方面时，权重积累是相当自然的。例如，非负权重的累积，称为奖励，可以用于形式化给定任务时间表的总能量消耗或错过最后期限所要支付的总罚款。具有负值和正值的权重函数可以用来模拟电池供电设备的能量水平，或者股票市场一天内的总盈亏。继最近对具有累积权重断言的时间逻辑的研究之后，该项目的目标是深入研究在具有多个权重函数的离散时间马尔可夫模型上解释的加权线性时间和分支时间时间时间逻辑的模型检查问题。项目的重点将放在加权时间逻辑（片段）的识别上，其中概率模型检查技术是可行的。更具体地说，该项目旨在(1)为分支时间逻辑提供模型检查算法，其中算子指定有权路径属性的概率界限，以及条件期望累积权重和期望成本效用比的算子；(2)为具有非负权函数的马尔可夫模型开发复杂的模型检查算法；(3)研究马尔可夫决策过程中具有最优稳态行为的调度程序的新的长期算子。理论工作将伴随着一个原型实现的实验研究。

Weight accumulation occurs rather naturally in the analysis of resource-awareness and other quantitative aspects of systems. For example, the accumulation of non-negative weights, called rewards, can serve to formalize the total energy consumption of a given task schedule or the total penalty to be paid for missed deadlines. Weight functions with negative and positive values can be used to model the energy level in battery-operated devices or the total win or loss of a share at the stock market over one day. Following the line of recent work on temporal logics with assertions on accumulated weights, the goal of the project is an in-depth investigation of model-checking problems for weighted linear- and branching-time temporal logics interpreted over discrete-time Markovian models with multiple weight functions. The focus of the project will be on the identification of (fragments of) weighted temporal logics where probabilistic model-checking techniques are feasible. More specifically, the project aims to (1) provide model-checking algorithms for a branching-time logic with operators specifying bounds on the probability for weight-bounded path properties as well as operators for conditional expected accumulated weights and expected cost-utility ratios, (2) develop sophisticated model-checking algorithms for Markovian models with non-negative weight functions, and (3) investigate new long-run operators for reasoning about schedulers with optimal steady-state behavior in Markov decision processes. The theoretical work will be accompanied by experimental studies with a prototype implementation.