Temporal Logics and Probabilistic Model Checking for Weighted Structures

点击翻译按钮获取中文摘要

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.