
Unambiguous automata are nondeterministic automata in which every word has at
most one accepting run. In this paper we give a polynomialtime algorithm for
model checking discretetime Markov chains against $\omega$regular
specifications represented as unambiguous automata. We furthermore show that
the complexity of this model checking problem lies in NC: the subclass of P
comprising those problems solvable in polylogarithmic parallel time. These
complexity bounds match the known bounds for model checking Markov chains
against specifications given as deterministic automata, notwithstanding the
fact that unambiguous automata can be exponentially more succinct than
deterministic automata. We report on an implementation of our procedure,
including an experiment in which the implementation is used to model check LTL
formulas on Markov chains.

The paper addresses the problem of computing maximal conditional expected
accumulated rewards until reaching a target state (briefly called maximal
conditional expectations) in finitestate Markov decision processes where the
condition is given as a reachability constraint. Conditional expectations of
this type can, e.g., stand for the maximal expected termination time of
probabilistic programs with nondeterminism, under the condition that the
program eventually terminates, or for the worstcase expected penalty to be
paid, assuming that at least three deadlines are missed. The main results of
the paper are (i) a polynomialtime algorithm to check the finiteness of
maximal conditional expectations, (ii) PSPACEcompleteness for the threshold
problem in acyclic Markov decision processes where the task is to check whether
the maximal conditional expectation exceeds a given threshold, (iii) a
pseudopolynomialtime algorithm for the threshold problem in the general
(cyclic) case, and (iv) an exponentialtime algorithm for computing the maximal
conditional expectation and an optimal scheduler.

In a software product line (SPL), a collection of software products is
defined by their commonalities in terms of features rather than explicitly
specifying all products onebyone. Several verification techniques were
adapted to establish temporal properties of SPLs. Symbolic and familybased
model checking have been proven to be successful for tackling the combinatorial
blowup arising when reasoning about several feature combinations. However,
most formal verification approaches for SPLs presented in the literature focus
on the static SPLs, where the features of a product are fixed and cannot be
changed during runtime. This is in contrast to dynamic SPLs, allowing to adapt
feature combinations of a product dynamically after deployment. The main
contribution of the paper is a compositional modeling framework for dynamic
SPLs, which supports probabilistic and nondeterministic choices and allows for
quantitative analysis. We specify the feature changes during runtime within an
automatabased coordination component, enabling to reason over strategies how
to trigger dynamic feature changes for optimizing various quantitative
objectives, e.g., energy or monetary costs and reliability. For our framework
there is a natural and conceptually simple translation into the input language
of the prominent probabilistic model checker PRISM. This facilitates the
application of PRISM's powerful symbolic engine to the operational behavior of
dynamic SPLs and their familybased analysis against various quantitative
queries. We demonstrate feasibility of our approach by a case study issuing an
energyaware bonding network device.

Reliability in terms of functional properties from the safetyliveness
spectrum is an indispensable requirement of lowlevel operatingsystem (OS)
code. However, with evermore complex and thus less predictable hardware,
quantitative and probabilistic guarantees become more and more important.
Probabilistic model checking is one technique to automatically obtain these
guarantees. First experiences with the automated quantitative analysis of
lowlevel operatingsystem code confirm the expectation that the naive
probabilistic model checking approach rapidly reaches its limits when
increasing the numbers of processes. This paper reports on our workinprogress
to tackle the state explosion problem for lowlevel OScode caused by the
exponential blowup of the model size when the number of processes grows. We
studied the symmetry reduction approach and carried out our experiments with a
simple testandtestandset lock case study as a representative example for a
wide range of protocols with natural interprocess dependencies and longrun
properties. We quickly see a statespace explosion for scenarios where
interprocess dependencies are insignificant. However, once interprocess
dependencies dominate the picture models with hundred and more processes can be
constructed and analysed.