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.