Cost-Utility Analysis in Probabilistic Models

Christel BaierChristel Baier

DOI Link

Christel Baier
Cost-Utility Analysis in Probabilistic Models
Proc. of the 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), 1, 2016. IEEE

Details
Bibtex

KurzfassungAbstract
The article deals with discrete-time Markovian models and addresses algorithmic problems for a cost-utility analysis. First, it reports on results on linear temporal specifications extended by weight assertions. The latter are linear constraints for the accumulated weights in finite path fragments satisfying a regular condition (formalized by a finite automaton, called “weight monitor”). For the full class of weight monitors immediately leads to undecidability. However, decidability can be achieved for acyclic weight monitors, which, e.g., can be used to specify protocols whose behavior depends on predictions for the near future (e.g. the wheather forecast) and/or the near past (e.g. the work load of the last hour). Moreover, the model checking problem becomes decidable for the full class of weight monitors when restricting to models with non-negative weights and a simple form of weight assertions. The second part addresses algorithms to compute optimal weight bounds for probabilistic reachability or invariance conditions and assertions on cost-utility ratios in models with nonnegative weights.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{B2016,
  author    = {Christel Baier},
  title     = {Cost-Utility Analysis in Probabilistic Models},
  booktitle = {Proc. of the 10th International Symposium on Theoretical Aspects
               of Software Engineering (TASE)},
  publisher = {IEEE},
  year      = {2016},
  pages     = {1},
  doi       = {http://dx.doi.org/10.1109/TASE.2016.10}
}