Cost-Utility Analysis in Weighted Markovian Models

Various types of automata models with weights attached to the states and/or transitions have been introduced to model and analyze the resource-awareness and other quantitative phenomena of systems. In this context, weight accumulation appears as a natural concept to reason about cost and utility measures. The accumulation of non-negative weights can, for instance, 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. The conceptual similarity between accumulated weights and counter machines causes the undecidability of many verification problems for multi-weighted models and temporal logics with weight accumulation over finite paths of unbounded length. However, decidability can be achieved for verification tasks in specialized structures, such as energy games or models with non-negative weight functions. Likewise, decidability results have been established for temporal logics with restricted forms of weight accumulation, such as modalities for weight accumulation along finite windows or limit-average properties. This extended abstract deals with discrete-time Markovian models and addresses algorithmic problems for a cost-utility analysis. First, it reports on results on linear temporal specifications with weight assertions. The second part addresses algorithms to compute optimal weight bounds for probabilistic reachability constraints and assertions on cost-utility ratios. 09: 30 09: 40 Break

Authors

• Christel Baier Technische Universität Dresden

Keywords

No keywords are indexed for this paper.