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.