
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 deals with finitestate Markov decision processes (MDPs) with
integer weights assigned to each stateaction pair. New algorithms are
presented to classify end components according to their limiting behavior with
respect to the accumulated weights. These algorithms are used to provide
solutions for two types of fundamental problems for integerweighted MDPs.
First, a polynomialtime algorithm for the classical stochastic shortest path
problem is presented, generalizing known results for special classes of
weighted MDPs. Second, qualitative probability constraints for weightbounded
(repeated) reachability conditions are addressed. Among others, it is shown
that the problem to decide whether a disjunction of weightbounded reachability
conditions holds almost surely under some scheduler belongs to $\textrm{NP}\cap
\textrm{coNP}$, is solvable in pseudopolynomial time and is at least as hard
as solving twoplayer meanpayoff games, while the corresponding problem for
universal quantification over schedulers is solvable in polynomial time.

Repair mechanisms are important within resilient systems to maintain the
system in an operational state after an error occurred. Usually, constraints on
the repair mechanisms are imposed, e.g., concerning the time or resources
required (such as energy consumption or other kinds of costs). For systems
modeled by Markov decision processes (MDPs), we introduce the concept of
resilient schedulers, which represent control strategies guaranteeing that
these constraints are always met within some given probability. Assigning
rewards to the operational states of the system, we then aim towards resilient
schedulers which maximize the longrun average reward, i.e., the expected mean
payoff. We present a pseudopolynomial algorithm that decides whether a
resilient scheduler exists and if so, yields an optimal resilient scheduler. We
show also that already the decision problem asking whether there exists a
resilient scheduler is PSPACEhard.

Continuoustime Markov chains with alarms (ACTMCs) allow for alarm events
that can be nonexponentially distributed. Within parametric ACTMCs, the
parameters of alarmevent distributions are not given explicitly and can be
subject of parameter synthesis. An algorithm solving the $\varepsilon$optimal
parameter synthesis problem for parametric ACTMCs with longrun average
optimization objectives is presented. Our approach is based on reduction of the
problem to finding longrun average optimal strategies in semiMarkov decision
processes (semiMDPs) and sufficient discretization of parameter (i.e., action)
space. Since the set of actions in the discretized semiMDP can be very large,
a straightforward approach based on explicit actionspace construction fails to
solve even simple instances of the problem. The presented algorithm uses an
enhanced policy iteration on symbolic representations of the action space. The
soundness of the algorithm is established for parametric ACTMCs with
alarmevent distributions satisfying four mild assumptions that are shown to
hold for uniform, Dirac and Weibull distributions in particular, but are
satisfied for many other distributions as well. An experimental implementation
shows that the symbolic technique substantially improves the efficiency of the
synthesis algorithm and allows to solve instances of realistic size.

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.

Probabilistic model checking mainly concentrates on techniques for reasoning
about the probabilities of certain path properties or expected values of
certain random variables. For the quantitative system analysis, however, there
is also another type of interesting performance measure, namely quantiles. A
typical quantile query takes as input a lower probability bound p and a
reachability property. The task is then to compute the minimal reward bound r
such that with probability at least p the target set will be reached before the
accumulated reward exceeds r. Quantiles are wellknown from mathematical
statistics, but to the best of our knowledge they have not been addressed by
the model checking community so far.
In this paper, we study the complexity of quantile queries for until
properties in discretetime finitestate Markov decision processes with
nonnegative rewards on states. We show that qualitative quantile queries can
be evaluated in polynomial time and present an exponential algorithm for the
evaluation of quantitative quantile queries. For the special case of Markov
chains, we show that quantitative quantile queries can be evaluated in time
polynomial in the size of the chain and the maximum reward.

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.

Probabilistic omegaautomata are variants of nondeterministic automata for
infinite words where all choices are resolved by probabilistic distributions.
Acceptance of an infinite input word can be defined in different ways: by
requiring that (i) the probability for the accepting runs is positive (probable
semantics), or (ii) almost all runs are accepting (almostsure semantics), or
(iii) the probability measure of the accepting runs is greater than a certain
threshold (threshold semantics). The underlying notion of an accepting run can
be defined as for standard omegaautomata by means of a Buechi condition or
other acceptance conditions, e.g., Rabin or Streett conditions. In this paper,
we put the main focus on the probable semantics and provide a summary of the
fundamental properties of probabilistic omegaautomata concerning
expressiveness, efficiency, and decision problems.

Lossy channel systems (LCSs) are systems of finite state automata that
communicate via unreliable unbounded fifo channels. In order to circumvent the
undecidability of model checking for nondeterministic
LCSs, probabilistic models have been introduced, where it can be decided
whether a lineartime property holds almost surely. However, such fully
probabilistic systems are not a faithful model of nondeterministic protocols.
We study a hybrid model for LCSs where losses of messages are seen as faults
occurring with some given probability, and where the internal behavior of the
system remains nondeterministic. Thus the semantics is in terms of
infinitestate Markov decision processes. The purpose of this article is to
discuss the decidability of lineartime properties formalized by formulas of
linear temporal logic (LTL). Our focus is on the qualitative setting where one
asks, e.g., whether a LTLformula holds almost surely or with zero probability
(in case the formula describes the bad behaviors). Surprisingly, it turns out
that  in contrast to finitestate Markov decision processes  the
satisfaction relation for LTL formulas depends on the chosen type of schedulers
that resolve the nondeterminism. While all variants of the qualitative LTL
model checking problem for the full class of historydependent schedulers are
undecidable, the same questions for finitememory scheduler can be solved
algorithmically. However, the restriction to reachability properties and
special kinds of recurrent reachability properties yields decidable
verification problems for the full class of schedulers, which  for this
restricted class of properties  are as powerful as finitememory schedulers,
or even a subclass of them.