
Christoph Scholl, JieHong Roland Jiang, Ralf Wimmer, Aile GeErnst: A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
Proceedings of the 33^{rd} AAAI Conference on Artificial Intelligence (AAAI), pages 1584–1591, AAAI Press, 2019
pdffile, BibTeX
, Original Publication
► Abstract
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which
subsumes quantified Boolean formulas (QBFs) and allows an explicit specification
of dependencies of existential variables on universal variables. This enables a
succinct encoding of decision problems in the NEXPTIME complexity class. As
solving general DQBFs is NEXPTIME complete, in contrast to the PSPACE
completeness of QBF solving, characterizing DQBF subclasses of lower
computational complexity allows their effective solving and is of practical
importance.
Recently a DQBF proof calculus based on a notion of fork extension, in addition
to resolution and universal reduction, was proposed by Rabe in 2017. We show
that this calculus is in fact incomplete for general DQBFs, but complete for a
subclass of DQBFs, where any two existential variables have either identical or
disjoint dependency sets over the universal variables. We further characterize
this DQBF subclass to be $\Sigma_3^\mathrmP$ complete in the polynomial time
hierarchy. Essentially using fork extension, a DQBF in this subclass can be
converted to an equisatisfiable 3QBF with only a linear increase in formula
size. We exploit this conversion for effective solving of this DQBF subclass and
point out its potential as a general strategy for DQBF quantifier localization.
Experimental results show that the method outperforms stateoftheart DQBF
solvers on a number of benchmarks, including the 2018 DQBF evaluation
benchmarks.

Aile GeErnst, Christoph Scholl, Ralf Wimmer: Localizing Quantifiers for DQBF
Proceedings of the 2019 International Conference on Formal Methods in ComputerAided Design (FMCAD), IEEE, 2019
pdffile, BibTeX
► Abstract
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which
subsumes quantified Boolean formulas (QBFs) and allows an explicit specification
of dependencies of existential variables on universal variables.
Driven by the needs of various applications that
can be encoded by DQBFs in a natural, compact, and elegant way,
research on DQBF solving has emerged in the past few years.
However, most works focus on closed DQBFs in prenex form (where all quantifiers
are placed in front of a propositional formula),
and nonprenex DQBFs have almost not been studied in the literature.
In this paper we provide a formal definition for syntax and semantics of
nonclosed nonprenex DQBFs and prove useful properties enabling quantifier localization.
Moreover, we make use of our theory by integrating quantifier localization into
a stateoftheart DQBF solver. Experiments with prenex DQBF benchmarks, including those from
the QBFEVAL'18 competition, clearly show that quantifier localization pays off in this context.

Steven Carr, Nils Jansen, Ralf Wimmer and
Alexandru Constantin Serban, Bernd Becker, Ufuk Topcu: CounterexampleGuided Strategy Improvement for POMDPs using
Recurrent Neural Networks
Proceedings of the 28^{th} International Joint Conference on Artificial Intelligence (IJCAI), pages 5532–5539, ijcai.org, 2019
pdffile, BibTeX
, Original Publication
► Abstract
We study strategy synthesis for POMDPs. The particular problem is to determine strategies that
provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable
and theoretically hard. We propose a novel method that combines techniques from machine learning and formal
verification. First, we train an RNN to encode POMDP strategies. The RNN accounts for memorybased decisions
without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNNbased strategy
to represent a finitememory strategy and implement it on a specific POMDP. For the resulting finite Markov
chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications.
If the specification is not satisfied, counterexamples supply diagnostic information. We use this
information to improve the strategy by iteratively training the RNN. Numerical experiments show that the
proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms
of solving times and model sizes.

Aile GeErnst, Christoph Scholl, Ralf Wimmer: Quantifier Localization for DQBF
Informal Proceedings of the 28^{th} International Workshop
on Logic & Synthesis (IWLS), 2019
pdffile, BibTeX
► Abstract
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which
subsumes quantified Boolean formulas (QBFs) and allows an explicit specification
of dependencies of existential variables on universal variables.
Driven by the needs of various applications which
can be encoded by DQBFs in a natural, compact and elegant way,
research on DQBF solving has emerged in the past few years.
However, research focused on closed DQBFs in prenex form (where all quantifiers
are placed in front of a propositional formula); nonprenex DQBFs
have almost not been studied, apart from one seminal work \citeBalabanovCJ14,
which considers –~as a side remark~–
quantifier localization for DQBF, transforming prenex DQBFs into nonprenex DQBFs.
However, in that work the semantics of nonprenex DQBFs is not formally defined and, in addition,
the two propositions allowing quantifier localization are not sound, as we will show in our paper.
We close this gap by providing a definition for syntax and semantics of
nonclosed nonprenex DQBFs and by formally proving useful properties.
Moreover, we make use of our theory by integrating quantifier localization into
a stateoftheart DQBF solver. Experiments with prenex DQBF benchmarks from the QBFEVAL'18 competition
clearly show that quantifier localization pays off in this context.

Ralf Wimmer, Christoph Scholl, Bernd Becker: The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation
Journal on Satisfiability, Boolean Modeling and Computation, 11, pages 1–51, 2019
pdffile, BibTeX
► Abstract
Preprocessing turned out to be an essential step for SAT, QBF, and DQBF
solvers to reduce/modify the number of variables and clauses of the formula,
before the formula is passed to the actual solving algorithm.
These preprocessing techniques often reduce the computation time of the solver
by orders of magnitude. In this paper, we present the preprocessor HQSpre that
was developed for Dependency Quantified Boolean Formulas (DQBFs) and
generalizes different preprocessing techniques for SAT and QBF problems to DQBF.
We give a presentation of the underlying theory together with detailed proofs
as well as implementation details contributing to the efficiency of the preprocessor.
HQSpre has been used with obvious success by the winners of the DQBF track, and,
even more interestingly, the QBF tracks of QBFEVAL'18.

Nils Jansen, Steven Carr, Alexandru Constantin Serban, Ralf Wimmer
and Ufuk Topcu, Bernd Becker: Coun\ter\exampleGuided Strategy Improvement for POMDPs using Recurrent Neural Networks
Proceedings of the 3^{rd} Workshop on Learning in Verification (LiVe), 2019
pdffile, BibTeX

Aile GeErnst, Christoph Scholl, Ralf Wimmer: Localizing Quantifiers for DQBF
Proceedings of the International Workshop on Quantified Boolean Formulas and Beyond (QBF), 2019
pdffile, BibTeX
► Abstract
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism which
allows a variety of applications to be encoded in a natural and elegant way.
So far, research has focused on closed DQBFs in prenex form, and nonprenex DQBFs
have almost not been studied in the literature. In our work, we provide a formal definition
for the syntax and semantics of nonclosed nonprenex DQBFs and prove useful properties to
enable quantifier localization. We show the effectiveness of applying our approach on prenex DQBF
benchmarks including those from the QBFEVAL'18 competition.

Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen
and Ufuk Topcu, JoostPieter Katoen, Bernd Becker: Strategy Synthesis in POMDPs via GameBased Abstractions
Proceedings of the RSSWorkshop on Safe Autonomy (RSSSafe), 2019
pdffile, BibTeX
► Abstract

Nils Jansen, Sebastian Junges, JoostPieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer: CorrectbyConstruction Policies for POMDPs
Proceedings of the 5^{th} International Workshop on SymbolicNumeric Methods for Reasoning about CPS and IoT (SNR), pages 6–8, ACM Press, 2019
pdffile, BibTeX
, Original Publication
► Abstract
In this extended abstract, we discuss how to compute policies with finite memory–socalled finitestate controllers
(FSCs)–for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications.
In particular, for a POMDP $M$ and a specification $\varphi$, we want to solve the decision problem whether there is a
policy $\sigma$ for $M$ with $k$ memory states, such that $\varphi$ is satisfied by $M$ and $\sigma$ ($M^\sigma\models\varphi$).
The underlying method is achieved via a marriage of formal verification and artificial intelligence.
The key insight is that computing (randomized) FSCs on POMDPs is equivalent to–and computationally as hard as–synthesis
for parametric Markov chains (pMCs). The parameter synthesis problem is to decide whether for a parametric Markov chain (pMC)
$D$ and a specification $\varphi$ there is a parameter instantiation $u$ such that in the Markov chain (MC) induced by $u$
the specification is satisfied ($M[u]\models\varphi$). The correspondence allows to utilize efficient tools for synthesis
in pMCs to compute correctbyconstruction FSCs on POMDPs.

Steven Carr, Nils Jansen, Ralf Wimmer
and Alexandru Constantin Serban, Bernd Becker, Ufuk Topcu: Coun\ter\exampleGuided Strategy Improvement for POMDPs Using
Recurrent Neural Networks
Technical report.
pdffile, BibTeX
► Abstract
We study strategy synthesis for POMDPs. The particular problem is to determine
strategies that provably adhere to (probabilistic) temporal logic constraints.
This problem is computationally intractable and theoretically hard.
We propose a novel method that combines techniques from machine learning and formal verification.
First, we train a RNN to encode POMDP strategies.
The RNN accounts for memorybased decisions without the need to expand the full belief space of
a POMDP. Secondly, we restrict the RNNbased strategy to represent a finitememory strategy
and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal
verification techniques provide provable guarantees against temporal logic specifications.
If the specification is not satisfied, counterexamples supply diagnostic information.
We use this information to improve the strategy by iteratively training the RNN.
Numerical experiments show that the proposed method elevates the state of the art in POMDP
solving by up to three orders of magnitude in terms of solving times and model sizes.

Aile GeErnst, Christoph Scholl, Ralf Wimmer: Quantifier Localization for DQBF
Technical report.
pdffile, BibTeX
► Abstract
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism,
which subsumes quantified Boolean formulas (QBFs) and allows an explicit
specification of dependencies of existential variables on universal variables.
Driven by the needs of various applications which can be encoded by DQBFs in a
natural, compact, and elegant way, research on DQBF solving has emerged in the
past few years. However, research focused on closed DQBFs in prenex form (where
all quantifiers are placed in front of a propositional formula) and nonprenex
DQBFs have almost not been studied in the literature. In this paper we provide
a formal definition for syntax and semantics of nonclosed nonprenex DQBFs and
prove useful properties enabling quantifier localization. Moreover, we make use
of our theory by integrating quantifier localization into a stateoftheart
DQBF solver. Experiments with prenex DQBF benchmarks including those from the
QBFEVAL'18 competition clearly show that quantifier localization pays off in
this context.

Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker: Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
Advanced Logic Synthesis, pages 151–168, Springer, 2018
pdffile, BibTeX
, Original Publication
► Abstract
We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization
of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural
calculus to exactly express the realizability problem of incomplete
combinational and sequential circuits with an arbitrary number of
(combinational or boundedmemory) black boxes.
In contrast to usual approaches for controller synthesis, restrictions to
the interfaces of missing circuit parts in distributed architectures are
strictly taken into account. We present a solution method for DQBFs
together with the extraction of Skolem functions for existential variables,
which can directly serve as implementations for the black boxes. First
experimental results are provided.

Bernd Becker, Christoph Scholl, Ralf Wimmer: Verification of Incomplete Designs
Formal System Verification – State of the Art and Future Trends, pages 37–72, Springer, 2018
pdffile, BibTeX
, Original Publication
► Abstract
We consider the verification of digital systems which are incomplete in the sense
that for some modules only their interfaces (i.e., the signals entering and
leaving the module) are known, but not their implementations. For such designs,
we study realizability („Is it possible to implement the missing modules
such that the complete design has certain properties?”) and validity
(„Does a property hold no matter how the missing parts are implemented?”).

Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu, Ufuk Topcu: HumanintheLoop Synthesis for Partially Observable Markov Decision Processes
Proceedings of the 2018 Annual American Control Conference (ACC), pages 762–769, IEEE, 2018
pdffile, BibTeX
, Original Publication
► Abstract
We study planning problems where autonomous agents operate inside environments
that are subject to uncertainties and not fully observable. Partially observable Markov
decision processes (POMDPs) are a natural formal model to capture such problems. Because
of the potentially huge or even infinite belief space in POMDPs, synthesis with safety
guarantees is, in general, computationally intractable. We propose an approach that aims
to circumvent this difficulty: in scenarios that can be partially or fully simulated in a
virtual environment, we actively integrate a human user to control an agent. While the user
repeatedly tries to safely guide the agent in the simulation, we collect data from the
human input. Via behavior cloning, we translate the data into a strategy for the POMDP.
The strategy resolves all nondeterminism and nonobservability of the POMDP, resulting in
a discretetime Markov chain (MC). The efficient verification of this MC gives quantitative
insights into the quality of the inferred human strategy by proving or disproving given
system specifications. For the case that the quality of the strategy is not sufficient,
we propose a refinement method using counterexamples presented to the human. Experiments
show that by including humans into the POMDP verification loop we improve the state of
the art by orders of magnitude in terms of scalability.

Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker: From DQBF to QBF by Dependency Elimination (Extended Abstract)
Proceedings of the 21^{st} GI/ITG/GMMWorkshop
„Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2018
pdffile, BibTeX
, Original Publication
► Abstract
Dependency quantified Boolean formulas (DQBFs) are a generalization of QBFs, which allows
to have existential variables that depend on arbitrary subsets of the universal variables.
We present an effective way to solve such DQBFs by eliminating individual dependencies such that
an equisatisfiable QBF is obtained, which can be solved by an arbitrary QBF solver. We also
present how to use dependency schemes in order to obtain smaller equisatisfiable QBFs, which
can typically be solved more efficiently.

Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, JoostPieter Katoen, Bernd Becker: Abstraktionsbasierte Verifikation von POMDPs im MotionPlanning Kontext (Extended Abstract)
Proceedings of the 21^{st} GI/ITG/GMMWorkshop
„Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2018
pdffile, BibTeX
, Original Publication
► Abstract
Wir untersuchen Pfadplanungsprobleme aus der Robotik
und die Berechnung von Strategien, die beweisbare Garantien für Sicherheitseigenschaften
liefern. Dabei soll ein Agent mit hoher Wahrscheinlichkeit einen Zielort
erreichen, ohne mit einem Hindernis zusammenzustoßen, das sich probabilistisch
durch den Raum bewegt. Schwierig wird dieses Problem dadurch, dass der Agent
seine Umgebung nur eingeschränkt beobachten kann. Dieses Szenario lässt
sich auf natürliche Art und Weise als ein sogenannter
partiell beobachtbarer MarkowEntscheidungsprozess (POMDP) modellieren.
Da viele interessante Eigenschaften auf POMDPs unentscheidbar sind, beschäftigt
sich die hier vorgestellte Arbeit mit der Entwicklung einer spielbasierten
Abstraktionsmethode, um für solche Pfadplanungsprobleme
und Sicherheitseigenschaften gute Approximationen zu berechnen.

Yuliya Butkova, Ralf Wimmer, Holger Hermanns: Markov Automata on Discount!
Proceedings of the 19^{th} International GI/ITG Conference on Measurement, Modelling and Evaluation of Computing Systems (MMB), Lecture Notes in Computer Science, vol. 10740, pages 19–34, Springer, 2018
pdffile, BibTeX
, Original Publication
► Abstract
Markov automata (MA) are a rich modelling formalism for complex systems
combining compositionality with probabilistic choices and
continuous stochastic timing. Model checking algorithms for
different classes of properties involving probabilities and
rewards have been devised for MA, opening up a spectrum of applications
in dependability engineering and artificial intelligence, reaching
out into economy and finance. In the latter more general contexts, several
quantities of considerable importance are based on the idea of discounting reward
expectations, so that the near future is more important than the far future.
This paper introduces the expected discounted reward value for MA
and develops effective iterative algorithms to quantify it, based on
value as well as policyiteration. To arrive there, we reduce the problem
to the computation of expected discounted rewards and expected total rewards
in Markov decision processes. This allows us to adapt wellknown algorithms to
the MA setting. Experimental results clearly show that our algorithms are
efficient and scale to MA with hundred thousands of states.

Christoph Scholl, Ralf Wimmer: Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
Proceedings of the 21^{st} International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 10929, pages 3–16, Springer, 2018
pdffile, BibTeX
, Original Publication
► Abstract
Dependency quantified Boolean formulas (DQBFs) as a generalization
of quantified Boolean formulas (QBFs) have received considerable
attention in research during the last years. Here we give an overview
of the solution methods developed for DQBF so far. The exposition is
complemented with the discussion of various applications that can be
handled with DQBF solving.

Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu, Ufuk Topcu: HumanintheLoop Synthesis for Partially Observable Markov Decision Processes
Technical report.
pdffile, BibTeX
► Abstract
We study planning problems where autonomous agents operate inside environments that
are subject to uncertainties and not fully observable. Partially observable Markov decision
processes (POMDPs) are a natural formal model to capture such problems. Because of the potentially
huge or even infinite belief space in POMDPs, synthesis with safety guarantees is, in general,
computationally intractable. We propose an approach that aims to circumvent this difficulty:
in scenarios that can be partially or fully simulated in a virtual environment, we actively integrate
a human user to control an agent. While the user repeatedly tries to safely guide the agent in the
simulation, we collect data from the human input. Via behavior cloning, we translate the data into
a strategy for the POMDP. The strategy resolves all nondeterminism and nonobservability of the POMDP,
resulting in a discretetime Markov chain (MC). The efficient verification of this MC gives
quantitative insights into the quality of the inferred human strategy by proving or disproving given
system specifications. For the case that the quality of the strategy is not sufficient, we propose a
refinement method using counterexamples presented to the human. Experiments show that by including
humans into the POMDP verification loop we improve the state of the art by orders of magnitude in terms
of scalability.

Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, JoostPieter Katoen, Bernd Becker: FiniteState Controllers of POMDPs via Parameter Synthesis
Proceedings of the 34^{th} Conference on Uncertainty in Artificial Intelligence (UAI), pages 519–529, AUAI Press, 2018
pdffile, BibTeX
► Abstract
We study finitestate controllers (FSCs) for partially observable Markov decision processes (POMDPs)
that are provably correct with respect to given specifications. The key insight is that computing (randomised)
FSCs on POMDPs is equivalent to (and computationally as hard as) synthesis for parametric Markov chains (pMCs).
This correspondence enables using blackbox techniques to compute correctbyconstruction FSCs for POMDPs for
a wide range of properties. Our experimental evaluation on typical POMDP problems shows that we are competitive
to stateoftheart POMDP solvers.

Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, JoostPieter Katoen, Bernd Becker: Motion Planning under Partial Observability using GameBased Abstraction
Proceedings of the 56^{th} IEEE Conference on Decision and Control (CDC), pages 2201–2208, IEEE, 2017
pdffile, BibTeX
, Original Publication
► Abstract
We study motion planning problems where agents move inside environments that are
not fully observable and subject to uncertainties. The goal is to compute a
strategy for an agent that is guaranteed to satisfy certain safety and
performance specifications. Such problems are naturally modeled by partially
observable Markov decision processes (POMDPs). Because of the potentially huge
or even infinite belief space of POMDPs, verification and strategy synthesis is
in general computationally intractable. We tackle this difficulty by exploiting
typical structural properties of such scenarios; for instance, we assume that
agents have the ability to observe their own positions inside an environment.
Ambiguity in the state of the environment is abstracted into nondeterministic
choices over the possible states of the environment. Technically, this
abstraction transforms POMDPs into probabilistic twoplayer games (PGs). For
these PGs, efficient verification tools are able to determine strategies that
approximate certain measures on the POMDP. If an approximation is too coarse to
provide guarantees, an abstraction refinement scheme further resolves the belief
space of the POMDP. We demonstrate that our method improves the state of the art
by orders of magnitude compared to a direct solution of the POMDP.

Hassan Hatefi, Ralf Wimmer, Bettina Braitling
and Luis María Ferrer Fioriti, Bernd Becker, Holger Hermanns: Cost vs. Time in Stochastic Games and Markov Automata
Formal Aspects of Computing, 29(4), pages 629–649, 2017
pdffile, BibTeX
, Original Publication
► Abstract
Costs and rewards are important tools for analysing quantitative
aspects of models like energy consumption and costs of maintenance
and repair. Under the assumption of transient costs, this
paper considers the computation of expected costbounded
rewards and costbounded reachability for Markov automata and
Markov games. We provide a fixed point characterization of this class of
properties under early schedulers. Additionally, we give a
transformation to expected timebounded rewards and timebounded
reachability, which can be computed by available algorithms.
We prove the correctness of the transformation and show its
effectiveness on a number of Markov automata case studies.

Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, JoostPieter Katoen, Bernd Becker: Abstractionbased Model Checking of POMDPs in Motion Planning
Proceedings of the PhD Symposium at iFM'17 on Formal Methods: Algorithms, Tools and Applications (PhDiFM), 2017
pdffile, BibTeX
► Abstract
Partially observable Markov decision processes (POMDPs) are a natural model for
many applications where one has to deal with incomplete knowledge and random phenomena, including,
but not limited to, robotics and motion planning. However, many interesting properties of POMDPs
are undecidable or otherwise very expensive to decide in terms of both runtime and memory usage.
In our work, we develop abstractionbased methods that can deliver safe bounds and good
approximations for certain classes of properties.

Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker: From DQBF to QBF by Dependency Elimination
Proceedings of the 20^{th} International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 10491, pages 326–343, Springer, 2017
pdffile, BibTeX
, Original Publication
► Abstract
In this paper, we propose the elimination of dependencies
to convert a given dependency quantified Boolean formula (DQBF)
to an equisatisfiable QBF. We show how to select a set of
dependencies to eliminate such that we arrive at a smallest equisatisfiable
QBF in terms of existential variables that is achievable using
dependency elimination. This approach is improved
by taking socalled don'tcare dependencies into account, which
result from the application of dependency schemes to the formula
and can be added to or removed from the formula at no cost.
We have implemented this new method in the stateoftheart
DQBF solver HQS. Experiments show that dependency elimination is
clearly superior to the previous method using variable elimination.

Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker: HQSpre – An Effective Preprocessor for QBF and DQBF
Proceedings of the 23^{rd} International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part~I, Lecture Notes in Computer Science, vol. 10205, pages 373–390, Springer, 2017
pdffile, BibTeX
, Original Publication
► Abstract
We present our new preprocessor HQSpre, a stateoftheart tool for
simplifying quantified Boolean formulas (QBFs) and the first available
preprocessor for dependency quantified Boolean formulas (DQBFs). The
latter are a generalization of QBFs, resulting from adding socalled
Henkinquantifiers to QBFs. HQSpre applies most of the
preprocessing techniques that have been proposed in the literature. It
can be used both as a standalone tool and as a library. It is possible
to tailor it towards different solver backends, e. g., to preserve
the circuit structure of the formula when a nonCNF solver backend is
used. Extensive experiments show that HQSpre allows QBF solvers to
solve more benchmark instances and is able to decide more instances
on its own than stateoftheart tools. The same impact can be observed
in the DQBF domain as well.

Yuliya Butkova, Ralf Wimmer, Holger Hermanns: Longrun Rewards for Markov Automata
Proceedings of the 23^{rd} International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part~II, Lecture Notes in Computer Science, vol. 10206, pages 188–203, Springer, 2017
pdffile, BibTeX
, Original Publication
► Abstract
Markov automata are a powerful formalism for modelling systems which
exhibit nondeterminism, probabilistic choices and continuous stochastic
timing. We consider the computation of longrun average rewards,
the most classical problem in continuoustime Markov model analysis.
We propose an algorithm based on value iteration. It improves the
state of the art by orders of magnitude. The contribution is rooted
in a fresh look on Markov automata, namely by treating them as an
efficient encoding of CTMDPs with –~in the worst case~– exponentially
more transitions.

Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen
and Ufuk Topcu, JoostPieter Katoen, Bernd Becker: Motion Planning under Partial Observability using GameBased Abstraction
Technical report.
pdffile, BibTeX
► Abstract
We study motion planning problems where agents move inside environments
that are not fully observable and subject to uncertainties. The goal is to compute
a strategy for an agent that is guaranteed to satisfy certain safety and performance
specifications. Such problems are naturally modelled by partially observable Markov
decision processes (POMDPs). Because of the potentially huge or even infinite belief
space of POMDPs, verification and strategy synthesis is in general computationally
intractable. We tackle this difficulty by exploiting typical structural properties of
such scenarios; for instance, we assume that agents have the ability to observe their
own positions inside an environment. Ambiguity in the state of the environment is
abstracted into nondeterministic choices over the possible states of the environment.
Technically, this abstraction transforms POMDPs into probabilistic twoplayer games
(PGs). For these PGs, efficient verification tools are able to determine strategies
that approximate certain measures on the POMDP. If an approximation is too coarse to
provide guarantees, an abstraction refinement scheme further resolves the belief space
of the POMDP. We demonstrate that our method improves the state of the art by orders
of magnitude compared to a direct solution of the POMDP.

Sebastian Junges, Nils Jansen, Ralf Wimmer
and JoostPieter Katoen, Bernd Becker: Permissive Finitestate Controllers of POMDPs using Parameter Synthesis
Technical report.
pdffile, BibTeX
► Abstract
We study finitestate controllers (FSCs) for partially observable Markov decision
processes (POMDPs) that are provably correct with respect to given specifications.
The key insight is that computing (randomised) FSCs on POMDPs is equivalent to–and
computationally as hard as–synthesis for parametric Markov chains (pMCs).
This correspondence allows to use tools for parameter synthesis in pMCs to compute
correctbyconstruction FSCs on POMDPs for a variety of specifications.
Our experimental evaluation shows comparable performance to wellknown POMDP solvers.

Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Skolem Functions for DQBF
Proceedings of the 14^{th} International
Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 9938, pages 395–411, Springer, 2016
pdffile, BibTeX
, Original Publication
► Abstract
We consider the problem of computing Skolem functions for satisfied
dependency quantified Boolean formulas (DQBFs). We show how Skolem functions
can be obtained from an eliminationbased DQBF solver and how to take
preprocessing steps into account. The size of the Skolem functions is
optimized by don'tcare minimization using Craig interpolants and
rewriting techniques. Experiments with our DQBF solver HQS
show that we are able to effectively compute Skolem functions with
very little overhead compared to the mere solution of the formula.

Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker: Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
Informal Proceedings of the 25^{th} International Workshop on Logic & Synthesis (IWLS), pages 50–57, 2016
pdffile, BibTeX
► Abstract
We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization
of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural
calculus to exactly express the realizability problem of incomplete
combinational and sequential circuits with an arbitrary number of
(combinational or boundedmemory) black boxes.
In contrast to usual approaches for controller synthesis, restrictions to
the interfaces of missing circuit parts in distributed architectures are
strictly taken into account. We present a solution method for DQBFs
together with the extraction of Skolem functions for existential variables,
which can directly serve as implementations for the black boxes. First
experimental results are provided.

Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker: Dependency Schemes for DQBF
Proceedings of the 19^{th} International Conference on Theory
and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9710, pages 473–489, Springer, 2016
pdffile, BibTeX
, Original Publication
► Abstract
Dependency schemes allow to identify variable independencies
in QBFs or DQBFs. For QBF, several dependency schemes have been
proposed, which differ in the number of independencies they are able
to identify. In this paper, we analyze the spectrum of dependency
schemes that were proposed for QBF. It turns out that only some of
them are sound for DQBF. For the sound ones, we provide a
correctness proof, for the others counterexamples.
Experiments show that a significant number of dependencies can
either be added to or removed from a formula without changing
its truth value, but with significantly increasing the flexibility
for modifying the representation.

Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Skolem Functions for DQBF (extended version)
Technical report.
pdffile, BibTeX
, Original Publication
► Abstract
We consider the problem of computing Skolem functions for satisfied
dependency quantified Boolean formulas (DQBFs). We show how Skolem functions
can be obtained from an eliminationbased DQBF solver and how to take
preprocessing steps into account. The size of the Skolem functions is
optimized by don'tcare minimization using Craig interpolants and
rewriting techniques. Experiments with our DQBF solver HQS
show that we are able to effectively compute Skolem functions with
very little overhead compared to the mere solution of the formula.

Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker: Solving DQBF through Quantifier Elimination
Proceedings of the International Conference on Design, Automation & Test in Europe (DATE), pages 1617–1622, IEEE, 2015
pdffile, BibTeX
, Original Publication
► Abstract
We show how to solve dependencyquantified Boolean formulas (DQBF) using
a quantifier elimination strategy which yields an equivalent QBF
that can be decided using any standard QBF solver. The elimination is
accompanied by a number of optimizations which help reduce memory
consumption and computation time.
We apply our solver HQS to problems from the domain of
verification of incomplete combinational circuits to demonstrate the
effectiveness of the proposed algorithm. The results show enormous
improvements both in the number of solved instances and in the
computation times compared to existing work on validating DQBF.

Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám
and JoostPieter Katoen, Bernd Becker: Counterexamples for Expected Rewards
Proceedings of the 20^{th} International Symposium on Formal Methods (FM), Lecture Notes in Computer Science, vol. 9109, pages 435–452, Springer, 2015
pdffile, BibTeX
, Original Publication
► Abstract
The computation of counterexamples for probabilistic systems
has gained a lot of attention during the last few years. All of the
proposed methods focus on the situation when the probabilities of certain
events are too high. In this paper we investigate how counterexamples for
properties concerning expected costs (or, equivalently, expected rewards)
of events can be computed. We propose methods to extract a minimal
subsystem which already leads to costs beyond the allowed bound. Besides
these exact methods, we present heuristic approaches based on path
search and on bestfirst search, which are applicable to very large systems
when deriving a minimum subsystem becomes infeasible due to the
system size. Experiments show that we can compute counterexamples
for systems with millions of states.

Ralf Wimmer, Nils Jansen, Erika Ábrahám, JoostPieter Katoen: Highlevel Counterexamples for Probabilistic Automata
Logical Methods in Computer Science, 11(1:15), pages 123, 2015
pdffile, BibTeX
, Original Publication
► Abstract
Providing compact and understandable counterexamples for violated
system properties is an essential task in model checking. Existing
works on counterexamples for probabilistic systems so far computed
either a large set of system runs or a subset of the system's
states, both of which are of limited use in manual debugging. Many
probabilistic systems are described in a guarded command language
like the one used by the popular model checker PRISM. In this
paper we describe how a smallest possible subset of the commands can be
identified which together make the system erroneous. We
additionally show how the selected commands can be further
simplified to obtain a wellunderstandable counterexample.

Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker: Towards Verification of Artificial Neural Networks
Proceedings of the 18^{th} GI/ITG/GMMWorkshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 30–40, Technische Universität Chemnitz, Germany, 2015
pdffile, BibTeX
► Abstract
We consider the safety verification of controllers obtained via
machine learning. This is an important problem as the employed
machine learning techniques work well in practice, but cannot guarantee
safety of the produced controller, which is typically represented as
an artificial neural network. Nevertheless, such methods are used
in safetycritical environments.\
In this paper we take a typical control problem, namely the Cart Pole System
(a.k.a. inverted pendulum),
and a model of its physical environment and study safety verification of
this system. To do so, we use bounded model checking (BMC). The created
formulas are solved with the SMTsolver iSAT3. We examine the problems
that occur during solving these formulas and show that
extending the solver by special deduction routines can reduce
both memory consumption and computation time on such instances significantly.
This constitutes a first step towards verification of machinelearned controllers,
but a lot of challenges remain.

Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker: Preprocessing for DQBF
Proceedings of the 18^{th} International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9340, pages 173–190, Springer, 2015
pdffile, BibTeX
, Original Publication
► Abstract
For SAT and QBF formulas many techniques are applied in order to reduce/modify
the number of variables and clauses of the formula, before the formula is
passed to the actual solving algorithm. It is well known that these
preprocessing techniques often reduce the computation time of the solver
by orders of magnitude. In this paper we generalize different preprocessing
techniques for SAT and QBF problems to dependency quantified Boolean formulas
(DQBF) and describe how they need to be adapted to work with a DQBF solver core. We
demonstrate their effectiveness both for CNF and nonCNFbased DQBF algorithms.

Hassan Hatefi, Bettina Braitling, Ralf Wimmer, Luis María Ferrer Fioriti, Holger Hermanns, Bernd Becker: Cost vs. Time in Stochastic Games and Markov Automata
Proceedings of the 1^{st} International Symposium on Dependable Software Engineering: Theory, Tools and Applications (SETTA), Lecture Notes in Computer Science, vol. 9409, pages 19–34, Springer, 2015
pdffile, BibTeX
, Original Publication
► Abstract
Costs and rewards are important tools for analysing quantitative
aspects of models like energy consumption and costs of maintenance
and repair. Under the assumption of transient costs, this
paper considers the computation of expected costbounded
rewards and costbounded reachability for Markov automata and
stochastic games. We give a transformation of this class of
properties to expected timebounded rewards and timebounded
reachability, which can be computed by available algorithms. We
prove the correctness of the transformation and show its
effectiveness on a number of case studies.

Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer: Modeling Unknown Values in Test and Verification
Formal Modeling and Verification of CyberPhysical Systems (Proceedings of the 1^{st} International Summer School on Methods and Tools for the Design of Digital Systems), pages 122–150, Springer, 2015
pdffile, BibTeX
, Original Publication
► Abstract
With increasing complexities and a componentbased design
style the handling of unkown values (e. g., at the interface of components)
becomes more and more important in electronic design automation (EDA)
and production processes. Tools are required that allow an accurate
modeling of unkowns in combination with algorithms balancing exactness
of representation and efficiency of calculation. In the following, stateoftheart
approaches are described that enable an efficient and successful
handling of unknown values using formal techniques in the areas of Test
and Verification.

Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker: Solving DQBF Through Quantifier Elimination
Technical report.
pdffile, BibTeX
► Abstract
We show how to solve dependency quantified Boolean formulas (DQBF) using
a quantifier elimination strategy which yields an equivalent QBF
that can be decided using any standard QBF solver. The elimination is
accompanied by a number of optimizations which help reduce memory
consumption and computation time.
We apply our solver HQS to problems from the domain of
verification of incomplete combinational circuits and demonstrate the
effectiveness of the proposed algorithm. The results show enormous
improvements both in the number of solved instances and in the
computation times compared to existing work on validating DQBF.

Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker: Preprocessing for DQBF
Technical report.
pdffile, BibTeX
► Abstract
For SAT and QBF formulas many techniques are applied in order to reduce/modify
the number of variables and clauses of the formula, before the formula is
passed to the actual solving algorithm. It is well known that these
preprocessing techniques often reduce the computation time of the solver
by orders of magnitude. In this paper we generalize different preprocessing
techniques for SAT and QBF problems to dependency quantified Boolean formulas
(DQBF) and describe how they need to be adapted to work with a DQBF solver core. We
demonstrate their effectiveness both for CNF and nonCNFbased DQBF algorithms.

Hassan Hatefi, Bettina Braitling, Ralf Wimmer, Luis María Ferrer Fioriti, Holger Hermanns, Bernd Becker: Cost vs. Time in Stochastic Games and Markov Automata
Technical report.
pdffile, BibTeX
► Abstract
Costs and rewards are important tools for analysing quantitative
aspects of models like energy consumption and costs of maintenance
and repair. Under the assumption of transient costs, this
paper considers the computation of expected costbounded
rewards and costbounded reachability for Markov automata and
stochastic games. We give a transformation of this class of
properties to expected timebounded rewards and timebounded
reachability, which can be computed by available algorithms. We
prove the correctness of the transformation and show its
effectiveness on a number of case studies.

Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd Becker: Transient Reward Approximation for ContinuousTime Markov Chains
IEEE Transactions on Reliability, 64(4), pages 1254–1275, 2015
pdffile, BibTeX
, Original Publication
► Abstract
We are interested in the analysis of very large continuoustime
Markov chains (CTMCs) with many distinct rates. Such models arise
naturally in the context of the reliability analysis, e. g.,
of computer networks performability analysis, of power grids,
of computer virus vulnerability, and in the study of
crowd dynamics. We use abstraction techniques together with novel
algorithms for the computation of bounds on the expected final and
accumulated rewards in continuoustime Markov decision processes
(CTMDPs). These ingredients are combined in a partly symbolic and
partly explicit (symblicit) analysis approach. In particular, we
circumvent the use of multiterminal decision diagrams, because the
latter do not work well if facing a large number of different
rates. We demonstrate the practical applicability and efficiency of
the approach on two case studies.

Bettina Braitling, Luis María Ferrer Fioriti
and Hassan Hatefi, Ralf Wimmer
and Holger Hermanns, Bernd Becker: Abstractionbased Computation of Reward Measures for Markov Automata
Proceedings of the 16^{th} International Conference
on Verification, Model Checking, and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, vol. 8931, pages 172–189, Springer, 2015
pdffile, BibTeX
, Original Publication
► Abstract
Markov automata allow us to model a wide range of complex reallife systems by
combining continuous stochastic timing with probabilistic transitions and
nondeterministic choices. By adding a reward function it is possible
to model costs like the energy consumption of a system as well.
However, models of reallife systems tend to be large, and the analysis methods
for such powerful models like Markov (reward) automata do not scale well, which limits
their applicability. To solve this problem we present an abstraction technique for
Markov reward automata, based on stochastic games, together with automatic refinement
methods for the computation of timebounded accumulated reward properties. Experiments
show a significant speedup and reduction in system size compared to direct analysis
methods.

Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, JoostPieter Katoen: Fast Debugging of PRISM Models
Proceedings of the 12^{th} International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 8837, pages 146–162, Springer, 2014
pdffile, BibTeX
, Original Publication
► Abstract
In addition to rigorously checking whether a system
conforms to a specification, model checking can provide valuable
feedback in the form of succinct and understandable
counterexamples. In the context of probabilistic systems, path and
subsystembased counterexamples at the statespace level can be of
limited use in debugging. As many probabilistic systems are
described in a guarded command language like the one used by the
popular model checker Prism, a technique identifying a subset of
critical commands has recently been proposed. Based on repeatedly
solving MAXSAT~instances, our novel approach to computing a minimal
critical command set achieves a speedup of up to five orders of
magnitude over the previously existing technique.

Ralf Wimmer, Erika Ábrahám: Maybe or Maybe Not – Contributions to Stochastic Verification
Aspekte der Technischen Informatik: Festschrift zum 60. Geburtstag von Bernd Becker, pages 119–127, Monsenstein und Vannerdat, 2014
► Abstract
We summarize the contributions of the Chair for Computer
Architecture at AlbertLudwigsUniversit\"at Freiburg
to the field of verification for stochastic
systems. The contributions are twofold: on the one hand, there
are methods for symbolic state space minimization, on the
other hand efficient algorithms for counterexample generation.

Sreedhar Saseendran Kumar, Jan Wülfing and
Joschka Boedecker, Ralf Wimmer, Martin Riedmiller
and Bernd Becker, Ulrich Egert: Autonomous Control of Network Activity
Proceedings of the 9^{th} International Meeting on SubstrateIntegrated Microelectrode Arrays (MEA), 2014
pdffile, BibTeX
► Abstract
Electrical stimulation of the brain is used to treat
neurological disorders. Yet it is unknown how to find stimulation
patterns that produce desired results with the least interference.
Towards this goal, we tested a generic closedloop paradigm that
autonomously optimizes stimulation settings. We used neuronal networks
coupled to a reinforcement learning based controller to maximize response lengths.

Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns: MeGARA: Menubased Game Abstraction Refinement for Markov Automata
Proceedings of the 12^{th} International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), Electronic Proceedings in Theoretical Computer Science, vol. 154, pages 48–63, Open Publishing Association, 2014
pdffile, BibTeX
, Original Publication
► Abstract
Markov automata combine continuous time, probabilistic
transitions, and nondeterminism in a single model. They represent
an important and powerful way to model a wide range of complex reallife
systems. However, such models tend to be large and difficult to handle,
making abstraction and abstraction refinement necessary. In this paper
we present an abstraction and abstraction refinement technique for
Markov automata, based on the gamebased and menubased abstraction of
probabilistic automata. First experiments show that a significant
reduction in size is possible using abstraction.

Nils Jansen, Florian Corzilius, Matthias Volk
and Ralf Wimmer, Erika Ábrahám
and JoostPieter Katoen, Bernd Becker: Accelerating Parametric Probabilistic Verification
Proceedings of the 11^{th} International
Conference on Quantitative Evaluation of Systems (QEST), Lecture Notes in Computer Science, vol. 8657, pages 404–420, Springer, 2014
pdffile, BibTeX
, Original Publication
► Abstract
We present a novel method for computing reachability probabilities of parametric
discretetime Markov chains whose transition probabilities are fractions of
polynomials over a set of parameters. Our algorithm is based on two key
ingredients: a graph decomposition into strongly connected subgraphs combined
with a novel factorization strategy for polynomials. Experimental evaluations
show that these approaches can lead to a speedup of up to several
orders of magnitude in comparison to existing approaches.

Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, JoostPieter Katoen, Ralf Wimmer: Counterexample Generation for DiscreteTime Markov Models: An Introductory Survey
14^{th} International School on Formal Methods for the
Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures, Lecture Notes in Computer Science, vol. 8483, pages 65–121, Springer, 2014
pdffile, BibTeX
, Original Publication
► Abstract
This paper is an introductory survey of available methods for
the computation and representation of probabilistic counterexamples
for discretetime Markov chains and probabilistic automata. In
contrast to traditional model checking, probabilistic
counterexamples are sets of finite paths with a critical probability
mass. Such counterexamples are not obtained as a byproduct of model
checking, but by dedicated algorithms. We define what probabilistic
counterexamples are and present approaches how they can be
generated. We discuss methods based on path enumeration, the computation of critical
subsystems, and the generation of critical command sets, both, using
explicit and symbolic techniques.

Nils Jansen, Ralf Wimmer, Erika Ábrahám
and Barna Zajzon, JoostPieter Katoen, Bernd Becker
and Johann Schuster: Symbolic Counterexample Generation for Large DiscreteTime
Markov Chains
Science of Computer Programming, 91(A), pages 90–114, 2014
pdffile, BibTeX
, Original Publication
► Abstract
This paper presents several symbolic counterexample generation
algorithms for discretetime Markov chains (DTMCs) violating a PCTL
formula. A counterexample is (a symbolic representation of) a subDTMC
that is incrementally generated. The crux to this incremental approach
is the symbolic generation of paths that belong to the
counterexample. We consider two approaches. First, we extend bounded
model checking and develop a simple heuristic to generate highly probable
paths first. We then complement the SATbased approach by a fully
(multiterminal) BDDbased technique. All symbolic approaches are
implemented, and our experimental results show a substantially better
scalability than existing explicit techniques. In particular, our
BDDbased approach using a method called fragment search allows for
counterexample generation for DTMCs with billions of states
(up to $10^15$).

Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi
and Ralf Wimmer, Bernd Becker, Holger Hermanns: Abstractionbased Computation of Reward Measures for Markov Automata (extended version)
Technical report.
pdffile, BibTeX
► Abstract
Markov automata allow us to model a wide range of complex reallife systems by
combining continuous stochastic timing with probabilistic transitions and
nondeterministic choices. By adding a reward function it is possible
to model costs like the energy consumption of a system as well.
However, models of reallife systems tend to be large, and the analysis methods
for such powerful models like Markov (reward) automata do not scale well, which limits
their applicability. To solve this problem we present an abstraction technique for
Markov reward automata, based on stochastic games, together with automatic refinement
methods for the computation of timebounded accumulated reward properties. Experiments
show a significant speedup and reduction in system size compared to direct analysis
methods.

Ralf Wimmer, Nils Jansen, Erika Ábrahám
and JoostPieter Katoen, Bernd Becker: Minimal Counterexamples for LinearTime Probabilistic Verification
Theoretical Computer Science, 549, pages 61–100, 2014
pdffile, BibTeX
, Original Publication
► Abstract
Counterexamples for property violations have a number of important
applications like supporting the debugging of erroneous systems and
verifying large systems via counter\exampleguided abstraction
refinement. In this paper, we propose the usage of minimal critical
subsystems of discretetime Markov chains and Markov decision
processes as counterexamples for violated ωregular properties.
Minimality can thereby be defined in terms of the number of states or
transitions. This problem is known to be NPcomplete for Markov decision
processes. We show how to compute such subsystems using mixed
integer linear programming and evaluate the practical applicability
in a number of experiments. They show that our method yields substantially
smaller counterexample than using existing techniques.

Karina Gitina, Sven Reimer, Matthias Sauer
and Ralf Wimmer, Christoph Scholl, Bernd Becker: Equivalence Checking of Partial Designs Using Dependency
Quantified Boolean Formulae
Proceedings of the 31^{st} IEEE International
Conference on Computer Design, pages 396–403, IEEE Computer Society Press, 2013
pdffile, BibTeX
, Original Publication
► Abstract
We consider the partial equivalence checking problem (PEC), i. e.,
checking whether a given partial implementation of a combinational
circuit can (still) be extended to a complete design that is
equivalent to a given full specification. To solve PEC, we give a
linear transformation from PEC to the question whether a dependency
quantified Boolean formula (DQBF) is satisfied.
Our novel algorithm to solve DQBF based on quantifier elimination can
therefore be applied to solve PEC. We also present first experimental
results showing the feasibility of our approach and the inaccuracy of
QBF approximations, which are usually used for deciding the PEC so far.

Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám: Stochastic Bounded Model Checking: Bounded Rewards and Compositionality
Proceedings of the 16^{th} GI/ITG/GMMWorkshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 243–254, Universität Rostock, ITMZ, 2013
pdffile, BibTeX
► Abstract
We extend the available SAT/SMTbased methods for generating
counterexamples of probabilistic systems in two ways: First, we
propose bounded rewards, which are appropriate, e. g., to model the
energy consumption of autonomous embedded systems, and show how to
extend the SMTbased counterexample generation to handle such
models. Second, we describe a compositional SAT encoding of the transition
relation of Markov models, which exploits the system structure to
obtain a more compact formula, which in turn can be solved more
efficiently. Preliminary experiments show promising results in both
cases.

Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Equivalence Checking for Partial Implementations Revisited
Proceedings of the 16^{th} GI/ITG/GMMWork\shop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 61–70, Universität Rostock, ITMZ, 2013
pdffile, BibTeX
► Abstract
In this paper we consider the problem of checking whether a partial
implementation can (still) be extended to a complete design which is equivalent
to a given full specification.
In particular, we investigate the relationship between the
equivalence checking problem for partial implementations (PEC) and
the validity problem for quantified boolean formulae (QBF) with
socalled Henkin quantifiers.
Our analysis leads us to a sound and complete algorithmic solution to the
PEC problem as well as to an exact complexity theoretical classification of the problem.

Ralf Wimmer, Nils Jansen, Andreas Vorpahl
and Erika Ábrahám, JoostPieter Katoen
and Bernd Becker: Highlevel Counterexamples for Probabilistic Automata
Proceedings of the 10^{th}
International Conference on Quantitative Evaluation of Systems (QEST), Lecture Notes in Computer Science, vol. 8054, pages 18–33, Springer, 2013
pdffile, BibTeX
, Original Publication
► Abstract
Providing compact and understandable counterexamples for violated
system properties is an essential task in model checking. Existing
works on counterexamples for probabilistic systems so far computed
either a large set of system runs or a subset of the system's
states, both of which are of limited use in manual debugging. Many
probabilistic systems are described in a guarded command language
like the one used by the popular model checker \textttPRISM. In this
paper we describe how a minimal subset of the commands can be
identified which together already make the system erroneous. We
additionally show how the selected commands can be further
simplified to obtain a wellunderstandable counterexample.

Ralf Wimmer, Nils Jansen, Andreas Vorpahl
and Erika Ábrahám, JoostPieter Katoen
and Bernd Becker: Highlevel Counterexamples for Probabilistic Automata
Technical report.
pdffile, BibTeX
► Abstract
Providing compact and understandable counterexamples for violated
system properties is an essential task in model checking. Existing
works on counterexamples for probabilistic systems so far computed
either a large set of system runs or a subset of the system's
states, both of which are of limited use in manual debugging. Many
probabilistic systems are described in a guarded command language
like the one used by the popular model checker \textttPRISM. In this
paper we describe how a minimal subset of the commands can be
identified which together already make the system erroneous. We
additionally show how the selected commands can be further
simplified to obtain a wellunderstandable counterexample.

Nils Jansen, Florian Corzilius, Matthias Volk
and Ralf Wimmer
and Erika Ábrahám, JoostPieter Katoen
and Bernd Becker: Accelerating Parametric Probabilistic Verification
Technical report.
pdffile, BibTeX
► Abstract
We present a novel method for computing reachability
probabilities of parametric discretetime Markov chains whose
transition probabilities are fractions of polynomials over a
set of parameters. Our algorithm is based on two key ingredients:
a graph decomposition into strongly connected subgraphs combined
with a novel factorization strategy for polynomials. Experimental
evaluations show that combining these approaches leads to a
speedup of up to several orders of magnitude in comparison to existing approaches.

Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, JoostPieter Katoen, Bernd Becker: The COMICS Tool – Computing Minimal Counterexamples for DTMCs
Proceedings of the 10^{th} International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 7561, pages 349–353, Springer, 2012
pdffile, BibTeX
, Original Publication
► Abstract
This paper presents the tool COMICS~1.0,
which performs model checking and generates counterexamples for DTMCs.
For an input DTMC, COMICS computes an
abstract system that carries the model checking information and uses
this result to compute a critical subsystem, which induces a
counterexample. This abstract subsystem can be refined and concretized
hierarchically. The tool comes with a command line version as
well as a graphical user interface that allows the user to
interactively influence the refinement process of the counterexample.

Nils Jansen and
Erika Ábrahám and
Barna Zajzon and
Ralf Wimmer and
Johann Schuster and
JoostPieter Katoen and
Bernd Becker: Symbolic Counterexample Generation for Discretetime Markov Chains
Proceedings of the 9^{th} International Symposium on Formal Aspects of Component Software (FACS), Lecture Notes in Computer Science, vol. 7684, pages 134–151, Springer, 2012
pdffile, BibTeX
, Original Publication
► Abstract
In this paper we investigate the generation of counterexamples
for discretetime Markov chains (DTMCs) and PCTL properties. Whereas
most available methods use explicit representations for at least some
intermediate results, our aim is to develop fully symbolic
algorithms. As in most related work, our counterexample computations are based on
path search. We first adapt bounded model checking as a
path search algorithm and extend it with a novel SATsolving
heuristics to prefer paths with higher probabilities. As a second
approach, we use symbolic graph algorithms to find
counterexamples. Experiments show that our approaches, in contrast to
other existing techniques, are applicable to very large systems
with millions of states.

Ralf Wimmer: Symbolische Methoden für die probabilistische Verifikation –
Zustands\raum\reduktion und Gegenbeispiele
Ausgezeichnete Informatikdissertationen 2011, Lecture Notes in Informatics (LNI), vol. D12, pages 271–280, Gesellschaft für Informatik, 2012
pdffile, BibTeX
► Abstract
Ein bekanntes Hindernis f\"ur die formale Verifikation von Systemen
bildet die potentiell stark anwachsende Gr\"o\sse des Zustandsraums, genannt
„Zustandsraumexplosion”. Dieses Problem konnte f\"ur digitale
Schaltungen durch den Einsatz symbolischer Methoden zufriedenstellend
gel\"ost oder zumindest entscheidend entsch\"arft werden. F\"ur
probabilistische Systeme, die als MarkowKette oder
MarkowEntscheidungsprozess modelliert sind, brachte die direkte
\"Ubertragung dieser symbolischen Methoden bisher keinen Durchbruch.
In dieser Arbeit stellen wir zwei neue Ans\"atze vor, mit denen
MarkowModelle mit sehr gro\ssen Zustandsr\"aumen verifiziert werden
k\"onnen. Die erste Methode ist ein symbolisches Verfahren zur
Vorverarbeitung: Zu jedem MarkowModell berechnen wir mit rein
symbolischen Verfahren das kleinste Modell, das in den
interessierenden Eigenschaften mit dem OriginalModell \"ubereinstimmt.
Die Verifikation kann danach auf dem minimierten Modell durchgef\"uhrt
werden. Das zweite offene Problem, das in der Dissertation gel\"ost
wird, ist die symbolische Berechnung von Gegenbeispielen, wenn
Sicherheitseigenschaften von MarkowKetten mit diskreter Zeit verletzt
sind. Anhand von Experimenten wird gezeigt, dass die neu entwickelten
Verfahren den bisher verf\"ugbaren Verfahren hinsichtlich der
Laufzeit bzw. der Gr\"o\sse der handhabbaren Systeme deutlich \"uberlegen sind.

Ralf Wimmer, Bernd Becker,
Nils Jansen, Erika Ábrahám and
JoostPieter Katoen: Minimal Critical Subsystems as Counterexamples
for ωRegular DTMC Properties
Proceedings of the 15^{th} GI/\allowbreak ITG/\allowbreak GMMWorkshop
„Methoden und Beschreibungssprachen zur Modellierung
und Verifikation von Schaltungen und Systemen” (MBMV), pages 169–180, Verlag Dr. Kova\v c, 2012
pdffile, BibTeX
► Abstract
We propose a new approach to compute
counterexamples for violated ωregular properties of
discretetime Markov chains. Whereas most approaches compute a set
of system paths as a counterexample, we determine a critical
subsystem that already violates the given property. In earlier
work methods have been introduced to compute such subsystems for safety
properties, based on a search for shortest paths. In this paper
we use mixed integer linear programming to determine
minimal critical subsystems for arbitrary ωregular properties.

Ralf Wimmer, Bernd Becker,
Nils Jansen, Erika Ábrahám,
JoostPieter Katoen: Minimal Critical Subsystems for DiscreteTime Markov Models
Proceedings of the 18^{th} International
Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 7214, pages 299–314, Springer, 2012
pdffile, BibTeX
, Original Publication
► Abstract
We propose a new approach to compute counterexamples for
violated ωregular properties of discretetime Markov chains
and Markov decision processes. Whereas most approaches compute a set
of system paths as a counterexample, we determine a critical
subsystem that already violates the given property. In earlier work
we introduced methods to compute such subsystems based on a search for
shortest paths. In this paper we use SMT solvers and mixed integer
linear programming to determine minimal critical subsystems.

Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, JoostPieter Katoen, Bernd Becker: The COMICS Tool – Computing Minimal Counterexamples for DTMCs
Technical report.
pdffile, BibTeX
► Abstract
This report presents the tool COMICS, which performs
model checking and generates counterexamples for DTMCs. For an input
DTMC, COMICS computes an abstract system that carries the model
checking information and uses this result to compute a critical
subsystem, which induces a counterexample. This abstract subsystem
can be refined and concretized hierarchically. The tool comes with a
commandline version as well as a graphical user interface that
allows the user to interactively influence the refinement process of
the counterexample.

Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd Becker: Transient Reward Approximation for ContinuousTime Markov Chains
Technical report.
pdffile, BibTeX
► Abstract
We are interested in the analysis of very large continuoustime
Markov chains (CTMCs) with many distinct rates. Such models arise naturally
in the context of reliability analysis, e.g., of computer network performability
analysis, of power grids, of computer virus vulnerability, and in the study
of crowd dynamics. We use abstraction techniques together with novel algorithms
for the computation of bounds on the expected final and accumulated rewards
in continuoustime Markov decision processes (CTMDPs). These ingredients
are combined in a partly symbolic and partly explicit (symblicit) analysis
approach. In particular, we circumvent the use of multiterminal decision
diagrams, because the latter do not work well if facing a large number of
different rates. We demonstrate the practical applicability and efficiency
of the approach on two case studies.

Ralf Wimmer, Nils Jansen, Erika Ábrahám, JoostPieter Katoen, Bernd Becker: Minimal Counterexamples for Refuting ωRegular Properties of Markov Decision Processes
Technical report.
pdffile, BibTeX
► Abstract
Counterexamples for property violations have a number of important
applications like supporting the debugging of erroneous systems and
verifying large systems via counter\exampleguided abstraction
refinement. In this paper, we propose the usage of minimal critical
subsystems of discretetime Markov chains and Markov decision
processes as counterexamples for violated ωregular properties.
Minimality can thereby be defined in terms of the number of states or
transitions. This problem is known to be NPcomplete for Markov decision
processes. We show how to compute such subsystems using mixed
integer linear programming and evaluate the practical applicability
in a number of experiments. They show that our method yields substantially
smaller counterexample than using existing techniques.

Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns
and Abhishek Dhama, Oliver Theel
and Ralf Wimmer, Bettina Braitling, Bernd Becker: Bounded Fairness for Probabilistic Distributed Algorithms
Proceedings of the 11^{th} International
Conference on Application of Concurrency to System Design (ACSD), pages 89–97, IEEE Computer Society, 2011
pdffile, BibTeX
, Original Publication
► Abstract
This paper investigates quantitative dependability metrics
for distributed algorithms operating in the presence of sporadic or
frequently occurring faults. In particular, we investigate necessary
revisions of traditional fairness assumptions in order to arrive at
useful metrics, without adding hidden assumptions that may obfuscate
their validity. We formulate faulty distributed algorithms as Markov
decision processes to incorporate both probabilistic faults and
nondeterminism arising from concurrent execution. We lift the notion
of bounded fairness to the setting of Markov decision processes.
Bounded fairness is particularly suited for
distributed algorithms running on nearly symmetric infrastructure, as
it is common for sensor network applications.
Finally, we apply this fairness notion in the quantitative
modelchecking of several case studies.

Nils Jansen, Erika Ábrahám, Jens Katelaan
and Ralf Wimmer, JoostPieter Katoen, Bernd Becker: Hierarchical Counterexamples for DiscreteTime Markov Chains
Proceedings of the 9^{th} International Symposium on
Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 6996, pages 443–452, Springer, 2011
pdffile, BibTeX
, Original Publication
► Abstract
This paper introduces a novel \emphcounterexample generation
approach for the verification of discretetime Markov chains (DTMCs)
with two main advantages: (1) We generate \emphabstract
counterexamples which can be refined in a \emphhierarchical manner.
(2) We aim at minimizing the number of states involved in the
counterexamples, and compute a \emphcritical subsystem of the DTMC
whose paths form a counterexample. Experiments show that with our
approach we can reduce the size of counterexamples and the number of
computation steps by several orders of magnitude.

Bettina Braitling, Ralf Wimmer, Bernd Becker
and Nils Jansen, Erika Ábrahám: Counterexample Generation for Markov Chains using
SMTbased Bounded Model Checking
Proceedings of the 13^{th} IFIP International Conference on
Formal Methods for Open Objectbased Distributed Systems
(FMOODS) / 31^{st} IFIP International Conference on FORmal
TEchniques for Networked and Distributed Systems (FORTE), Lecture Notes in Computer Science, vol. 6722, pages 75–89, Springer, 2011
pdffile, BibTeX
, Original Publication
► Abstract
Generation of counterexamples is a highly important task
in the model checking process. In contrast to, e. g., digital
circuits where counterexamples typically consist of a single path
leading to a critical state of the system, in the probabilistic
setting counterexamples may consist of a large number of paths. In
order to be able to handle large systems and to use the capabilities
of modern SATsolvers, bounded model checking (BMC) for discretetime
Markov chains was established.
In this paper we introduce the usage of SMTsolving over linear real
arithmetic for the BMC procedure. SMTsolving, extending SAT with
theories in this context on the one hand leads to a convenient way to
express conditions on the probability of certain paths and on the
other hand allows to handle Markov reward models. We use the former to
find paths with high probability first. This leads to more compact
counterexamples. We report on some experiments, which show promising
results.

Bettina Braitling, Ralf Wimmer, Bernd Becker
and Nils Jansen, Erika Ábrahám: SMTbased Counterexample Generation for Markov Chains
Proceedings of the 14^{th} GI/ITG/GMMWorkshop „Methoden und
Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen” (MBMV), pages 19–28, Offis Oldenburg, 2011
pdffile, BibTeX
► Abstract
Counterexamples are a highly important feature of the
model checking process. In contrast to, e. g., digital circuits where
counterexamples typically consist of a single path leading to a
critical state of the system, in the probabilistic setting,
counterexamples may consist of a large number of paths. In order to
be able to handle large systems and to use the capabilities of modern
SATsolvers, bounded model checking (BMC) for discretetime Markov
chains was established.
In this paper we introduce the usage of SMTsolving over the reals
for the BMC procedure. SMTsolving, extending SAT with theories, leads
in this context on the one hand to a convenient way to express
conditions on the probability of certain paths and on the other hand
to handle Markov Reward models. The former can be used to find paths with
high probability first. This leads to more compact counterexamples.
We report on some experiments, which show promising results.

Ralf Wimmer,
Ernst Moritz Hahn,
Holger Hermanns,
Bernd Becker: Reachability Analysis for Incomplete Networks
of Markov Decision Processes
Proceedings of the ACM/IEEE
9^{th} International Conference on
Formal Methods and Models for Codesign (MEMOCODE), pages 151–160, IEEE Computer Society Press, 2011
pdffile, BibTeX
, Original Publication
► Abstract
Assume we have a network of discretetime Markov decision processes
(MDPs) which synchronize via common actions. We investigate how to
compute probability measures in case the structure of some of the
component MDPs (socalled blackbox MDPs) is not known. We then
extend this computation to work on networks of MDPs that share
integer data variables of finite domain. We use a protocol which
spreads information within a network as a case study to show the
feasibility and effectiveness of our approach.

Nils Jansen, Erika Ábrahám, Jens Katelaan
and Ralf Wimmer, JoostPieter Katoen, Bernd Becker: Hierarchical Counterexamples for DiscreteTime Markov Chains
Technical report.
pdffile, BibTeX
► Abstract
In this paper we introduce a novel \emphcounterexample generation
approach for discretetime Markov chains (DTMCs) with two main
advantages: (1) We generate \emphabstract counterexamples, which
can be refined in a \emphhierarchical manner. (2) We aim at
minimizing the number of states involved in the counterexamples, and
compute a \emphcritical subsystem of the DTMC, whose paths form a
counterexample. Experiments show that with our approach we can
reduce the size of counterexamples and the number of computation
steps by orders of magnitude.

Marco Bozzano, Alessandro Cimatti, JoostPieter Katoen
and Viet Yen Nguyen, Thomas Noll, Marco Roveri and
Ralf Wimmer: A Model Checker for AADL
Proceedings of the 22^{nd} International
Conference on ComputerAided Verification (CAV), Lecture Notes in Computer Science, vol. 6174, pages 562–565, Springer, 2010
pdffile, BibTeX
, Original Publication
► Abstract
We present a graphical toolset for verifying AADL models, which are
gaining widespread acceptance in aerospace, automobile and avionics
industries for comprehensively specifying safetycritical systems by
capturing functional, probabilistic and hybrid aspects. Analyses
are implemented on top of mature model checking tools and range from
requirements validation to functional verification, safety assessment
via automatic derivation of FMEA tables and dynamic fault trees,
to performability evaluation, and diagnosability analysis. The toolset is
currently being applied to several case studies by a major industrial
developer of aerospace systems.

Natalia Kalinnik, Erika \'Abrah\'am
and Tobias Schubert, Ralf Wimmer
and Bernd Becker: Exploiting Different Strategies for the Parallelization
of an SMT Solver
Proceedings of the 13^{th} GI/ITG/GMMWorkshop
„Methoden und Beschreibungssprachen
zur Modellierung und Verifikation von Schaltungen
und Systemen” (MBMV), pages 97–106, FraunhoferVerlag, 2010
pdffile, BibTeX
► Abstract
In this paper we present two different parallelization
schemes for the SMT solver iSAT, based on (1) the distribution of
work by dividing the search space into disjoint parts and exploring
them in parallel, thereby exchanging learnt information, and (2) a
portfolio approach, where the entire benchmark instance is
explored in parallel by several copies of the same solver but using
different heuristics to guide the search. We also combine both
approaches such that solvers examine disjoint parts of the search
space using different heuristics. The main contribution of the
paper is to study the performances of different techniques for
parallelizing iSAT.

Ralf Wimmer, Bernd Becker: Correctness Issues of Symbolic Bisimulation Computation for Markov Chains
Proceedings of the 15^{th} International GI/ITG Conference on
„Measurement, Modelling and Evaluation of Computing Systems” (MMB) and
„Dependability and Fault Tolerance” (DFT), Lecture Notes in Computer Science, vol. 5987, pages 287–301, Springer, 2010
pdffile, BibTeX
, Original Publication
► Abstract
Bisimulation reduction is a classical means to
fight the infamous state space explosion problem, which limits the
applicability of automated methods for verification like model
checking. A signaturebased method, originally developed by Blom and
Orzan for labeled transition systems and adapted for Markov chains by
Derisavi, has proved to be very efficient. It is possible to implement it
symbolically using binary decision diagrams such that it is able to
handle very large state spaces efficiently. We will show, however,
that for Markov chains this algorithm suffers from numerical
instabilities, which often result in too large quotient systems. We
will present and experimentally evaluate two different approaches to
avoid these problems: first the usage of rational arithmetic, and
second an approach not only to represent the system structure but also
the transition rates symbolically. In addition, this allows us to
modify their actual values after the quotient computation.

Erika Ábrahám, Ulrich Loup, Ralf Wimmer, JoostPieter Katoen: On the Minimization of Hybrid Automata
Proceedings of the 22^{nd} Nordic Workshop on Programming Theory (NWPT), 2010
► Abstract
Minimization is a widely used technique for the abstraction of
systems with large or infinite state spaces. The result of the
minimization is a finite partitioning of the concrete state space
and an induced abstract transition system with the partitions as
abstract states. This final abstract transition system is bisimilar
to the concrete system with respect to the reachable states and the
observable actions.
In this work we discuss the minimization of hybrid systems and
introduce a modified minimization algorithm. It computes an
abstraction that is in general not bisimilar to the concrete system,
but it provides enough information for reachability analysis.
Furthermore, besides the wellknown forward approach for
minimization, we discuss as an alternative a backward minimization
method.

Ralf Wimmer, Salem Derisavi, Holger Hermanns: Symbolic Partition Refinement with Automatic Balancing of
Time and Space
Performance Evaluation, 67(9), pages 815–835, 2010
pdffile, BibTeX
, Original Publication
► Abstract
State space lumping is one of the classical means to fight
the state space explosion problem in statebased performance
evaluation and verification. Particularly when numerical algorithms
are applied to analyze a Markov model, one often observes that those
algorithms do not scale beyond systems of moderate size. To alleviate
this problem, symbolic lumping algorithms have been devised to
effectively reduce very large–but symbolically represented–Markov
models to moderate size explicit representations. This lumping
step partitions the Markov model in such a way that any numerical
analysis carried out on the lumped model is guaranteed to produce
exact results for the original system. But even this lumping
preprocessing may fail due to time or memory limitations. This paper
discusses the two main approaches to symbolic lumping, and combines
them to improve on their respective limitations. The algorithm
automatically converts between known symbolic partition
representations in order to provide a tradeoff between memory
consumption and runtime. We show how to apply this algorithm for the
lumping of Markov chains, but the same techniques can be adapted in a
straightforward way to other models like Markov reward models, labeled
transition systems, or interactive Markov chains.

Ralf Wimmer, Bettina Braitling, Bernd Becker
and Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns
and Abhishek Dhama, Oliver Theel: Symblicit Calculation of LongRun Averages for
Concurrent Probabilistic Systems
Proceedings of the 7^{th}
International Conference on Quantitative
Evaluation of Systems (QEST), pages 27–36, IEEE Computer Society Press, 2010
pdffile, BibTeX
, Original Publication
► Abstract
Model checkers for concurrent probabilistic systems have
become very popular within the last decade. The study of longrun
average behavior has however received only scant attention in this
area, at least from the implementation perspective. This paper
studies the problem of how to efficiently realize an algorithm for
computing optimal longrun average reward values for concurrent
probabilistic systems. At its core is a variation of Howard and
Veinott's algorithm for Markov decision processes, where symbolic
and nonsymbolic representations are intertwined in an effective
manner: the state space is represented using binary decision
diagrams, while the linear equation systems which have to be solved
for the induced Markov chains to improve the current scheduler are
solved using an explicit state representation. In order to keep the
latter small, we apply a symbolic bisimulation minimization
algorithm to the induced Markov chain. The scheduler improvement
step itself is again performed on symbolic data structures.
Practical evidence shows that the implementation is effective, and
sometimes uses considerably less memory than a fully explicit
implementation.

Erika Ábrahám , Nils Jansen
and Ralf Wimmer, JoostPieter Katoen, Bernd Becker: DTMC Model Checking by SCC Reduction
Proceedings of the 7^{th}
International Conference on Quantitative
Evaluation of Systems (QEST), pages 37–46, IEEE Computer Society Press, 2010
pdffile, BibTeX
, Original Publication
► Abstract
DiscreteTime Markov Chains (DTMCs) are a widelyused
formalism to model probabilistic systems. On the one hand, available
tools like Prism or Mrmc offer efficient \emphmodel
checking algorithms and thus support the verification of DTMCs.
However, these algorithms do not provide any diagnostic information
in the form of \emphcounterexamples, which are
highly important for the correction of erroneous systems. On the other
hand, there exist several approaches to generate counterexamples for
DTMCs, but all these approaches require the model checking result for
completeness.
In this paper we introduce a model checking algorithm for DTMCs that
also supports the generation of counterexamples. Our algorithm,
based on the detection and abstraction of strongly connected
components, offers \emphabstract counterexamples, which can be
interactively refined by the user.

Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns
and Abhishek Dhama, Oliver Theel
and Ralf Wimmer, Bettina Braitling, Bernd Becker: Bounded Fairness for Probabilistic Distributed Algorithms
Technical report.
pdffile, BibTeX
► Abstract
This paper investigates quantitative dependability metrics
for distributed algorithms operating in the presence of sporadic or
frequently occurring faults. In particular, we investigate necessary
revisions of traditional fairness assumptions in order to arrive at
useful metrics, without adding hidden assumptions that may obfuscate
their validity. We formulate distributed algorithms as Markov decision
processes to incorporate both probabilistic faults and nondeterminism
arising from the distributed setting. We especially discuss the
notions of bounded fairness and nearroundrobin schedulers,
which appear particularly suited for distributed algorithms running on
nearly symmetric infrastructure, as it is common for sensor network
applications. We further develop methods to incorporate this fairness
notion in the quantitative model checking of distributed algorithms.
Finally, we apply our methodology to several case studies to provide a
first experimental insight into its applicability.

Natalia Kalinnik,
Tobias Schubert and
Erika Ábrahám and
Ralf Wimmer and
Bernd Becker: Picoso – A Parallel Interval Constraint Solver
Proceedings of the International Conference
on Parallel and Distributed Processing Techniques
and Applications (PDPTA), pages 473–479, CSREA Press, 2009
pdffile, BibTeX
► Abstract
This paper describes the \underlineparallel \underlineinterval
\underlineconstraint \underlinesolver Picoso, which can decide
(a subclass of) boolean combinations of linear and nonlinear
constraints. Picoso follows a master/client model based on message
passing, making it suitable for any kind of workstation cluster as
well as for multiprocessor machines. To run several clients in
parallel, an efficient work stealing mechanism has been integrated,
dividing the overall search space into disjoint parts. Additionally,
to prevent the clients from running into identical conflicts,
information about conflicts in form of conflict clauses is exchanged
among the clients. Performance measurements, using four clients to
solve a number of benchmark problems, show that Picoso yields linear
speedup compared to the sequential interval constraint solver
iSAT, on which the clients of Picoso are based.

Abhishek Dhama, Oliver Theel and
Pepijn Crouzen, Holger Hermanns and
Ralf Wimmer, Bernd Becker: Dependability Engineering of Silent SelfStabilizing Systems
Proceedings of the 11^{th}
International Symposium on Stabilization,
Safety, and Security of Distributed Systems (SSS), Lecture Notes in Computer Science, vol. 5873, pages 238–253, Springer, 2009
pdffile, BibTeX
, Original Publication
► Abstract
Selfstabilization is an elegant way of realizing nonmasking
faulttolerant systems. Sustained research over last decades
has produced multiple selfstabilizing algorithms for many problems in
distributed computing. In this paper, we present a framework to
evaluate multiple selfstabilizing solutions under a fault model that
allows intermittent transient faults. To that end, metrics to quantify
the dependability of selfstabilizing systems are defined. It is also
shown how to derive models that are suitable for probabilistic model
checking in order to determine those dependability metrics. A
heuristicsbased method is presented to analyze counterexamples
returned by a probabilistic model checker in case the system under
investigation does not exhibit the desired degree of
dependability. Based on the analysis, the selfstabilizing algorithm
is subsequently refined.

Eckard Böde,
Marc Herbstritt and
Holger Hermanns and
Sven Johr and
Thomas Peikenkamp,
Reza Pulungan and
JanHendrik Rakow and
Ralf Wimmer and
Bernd Becker: Compositional Dependability Evaluation for Statemate
IEEE Transactions on Software Engineering, 35(2), pages 274–292, 2009
pdffile, BibTeX
, Original Publication
► Abstract
Software and system dependability is getting ever more
important in embedded system design. Current industrial practice of
modelbased analysis is supported by statetransition diagrammatic
notations such as Statecharts. Stateoftheart modelling tools like
Statemate support safety and failureeffect analysis at
design time, but restricted to qualitative properties. This paper
reports on a (plugin) extension of Statemate enabling the
evaluation of quantitative dependability properties at design time.
The extension is compositional in the way the model is augmented
with probabilistic timing information. This fact is exploited in the
construction of the underlying mathematical model, a uniform
continuoustime Markov decision process, on which we are able to
check requirements of the form: \emph„The probability to hit a
safetycritical system configuration within a mission time of 3
hours is at most 0.01.” We give a detailed explanation of the
construction and evaluation steps making this possible, and report
on a nontrivial case study of a highspeed train signalling system
where the tool has been applied successfully.

Ralf Wimmer, Bettina Braitling, Bernd Becker: Counterexample Generation for Discretetime
Markov Chains using Bounded Model Checking
Proceedings of the 10^{th} International
Conference on Verification, Model Checking, and
Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, pages 366–380, Springer, 2009
pdffile, BibTeX
, Original Publication
► Abstract
Since its introduction in 1999, bounded model checking
has gained industrial relevance for detecting errors
in digital and hybrid systems. One of the main reasons
for this is that it always provides a counterexample
when an erroneous execution trace is found. Such a
counterexample can guide the designer while debugging
the system.
In this paper we are investigating how bounded model
checking can be applied to generate counterexamples
for a different kind of model–namely discretetime
Markov chains. Since in this case counterexamples in general
do not consist of a single path to a safetycritical
state, but of a potentially large set of paths,
novel optimization techniques like loopdetection
are applied not only to speedup the counterexample
computation, but also to reduce the size of the
counterexamples significantly. We report on some
experiments which demonstrate the practical applicability
of our method.

Ralf Wimmer and
Alexander Kortus and
Marc Herbstritt and
Bernd Becker: Probabilistic Model Checking and
Reliability of Results
Proceedings of the 11^{th} IEEE International
Workshop on Design & Diagnostics of
Electronic Circuits & Systems (DDECS), pages 207–212, IEEE Computer Society Press, 2008
pdffile, BibTeX
, Original Publication
► Abstract
In formal verification, reliable results are of utmost
importance. In model checking of digital systems, mainly
incorrect implementations of the model checking algorithms
due to logical errors are the source of wrong results.
In probabilistic model checking, however,
numerical instabilities are an additional source for
inconsistent results.
We motivate our investigations with an example, for which
several stateoftheart probabilistic model checking tools
give completely wrong results due to inexact computations.
We then analyze, at which points inaccuracies are introduced
during the model checking process.
We discuss first ideas how, in spite of these inaccuracies,
reliable results can be obtained or at least the user be
warned about potential correctness problems:
(1) usage of exact (rational) arithmetic,
(2) usage of interval arithmetic to obtain safe approximations
of the actual probabilities, (3) provision of certificates
which testify that the result is correct, and (4) integration of
a „degree of belief” for each subformula into existing model
checking tools.

Bernd Becker
and Marc Herbstritt
and Natalia Kalinnik
and Matthew Lewis
and Juri Lichtner
and Tobias Nopper
and Ralf Wimmer: Propositional Approximations for Bounded
Model Checking of Partial Circuit Designs
Proceedings of the 26^{th} IEEE International Conference
on Computer Design (ICCD), pages 52–59, IEEE Computer Society Press, 2008
pdffile, BibTeX
, Original Publication
► Abstract
Bounded model checking of partial circuit designs enables
the detection of errors even when the implementation of the
design is not finished. The behavior of the missing parts
can be modeled by a conservative extension of propositional
logic, called 01Xlogic. Then the transitions of the
underlying (incomplete) sequential circuit under verification
have to be represented adequately. In this work, we investigate
the difference between a relationoriented and a functionoriented
approach for this issue. Experimental results on a large
set of examples show that the functionoriented representation
is most often superior w. r. t. (1) CPU runtime and (2)
accuracy regarding the ability to find a counterexample, such that
by using the functionoriented approach an increase of
accuracy up to 210\% and a speedup of the CPU runtime up to
390\% compared to the relationoriented approach are achieved. But
there are also relevant examples, e. g. a VLIWALU, for which the
relationoriented approach outperforms the functionoriented one
by 300\% in terms of CPUtime,
showing that both approaches are efficient for different scenarios.

Ralf Wimmer, Alexander Kortus
and Marc Herbstritt, Bernd Becker: The Demand for Reliability in Probabilistic Verification
Proceedings of the 11^{th} GI/ITG/GMMWorkshop
„Methoden und Beschreibungssprachen zur Modellierung
und Verifikation von Schaltungen und Systemen” (MBMV), pages 99–108, ShakerVerlag, 2008
pdffile, BibTeX
► Abstract
For formal verification,
reliable results are of utmost importance.
In model checking of digital systems, mainly
incorrect implementations due to logical errors are the source
of wrong results. In probabilistic model checking, however, numerical
instabilities are an additional source for inconsistent
results.
First we present an example, for which several stateoftheart
probabilistic model checking tools give completely wrong
results due to inexact computations. This motivates the
investigation at which points inaccuracies are introduced
during the model checking process. We then give ideas how,
in spite of these inaccuracies, reliable results can be obtained or
at least the user be warned about potential problems:
(1) to introduce a „degree of belief” for each subformula,
(2) to use exact (rational) arithmetic,
(3) to use interval arithmetic to obtain safe approximations
of the actual probabilities, and (4) to provide certificates
which testify that the result is correct.

Ralf Wimmer,
Salem Derisavi,
Holger Hermanns: Symbolic Partition Refinement with Dynamic Balancing of Time and Space
Proceedings of the 5^{th} International Conference
on Quantitative Evaluation of Systems (QEST), pages 65–74, IEEE Computer Society Press, 2008
pdffile, BibTeX
, Original Publication
► Abstract
Bisimulation minimization is one of the classical means to fight the
infamous state space explosion problem in verification. Particularly
in stochastic verification, numerical algorithms are applied, which
do not scale beyond systems of moderate size. To alleviate this
problem, symbolic bisimulation minimization has been used
effectively to reduce very large symbolically represented state
spaces to moderate size explicit representations. But even this
minimization may fail due to time or memory limitations. This paper
presents a symbolic algorithm which relies on a hybrid symbolic
partition representation. It dynamically converts between two known
representations in order to provide a tradeoff between
memory consumption and runtime. The conversion itself is logarithmic
in the partition size. We show how to apply it for the
minimization of Markov chains, but the same techniques can be
adapted in a straightforward way to other models like labeled
transition systems or interactive Markov chains.

Ralf Wimmer, Marc Herbstritt, Bernd Becker: Optimization Techniques for BDDbased Bisimulation Minimization
Proceedings of the 17^{th} ACM Great Lakes Symposium on VLSI (GLSVLSI), pages 405–410, ACM Press, 2007
pdffile, BibTeX
, Original Publication
► Abstract
In this paper we report on optimizations for
a BDDbased algorithm for the computation
of bisimulations. The underlying algorithmic
principle is an iterative refinement of a
partition of the state space. The proposed
optimizations demonstrate that both, taking
into account the algorithmic structure of the
problem and the exploitation of the BDDbased
representation, are essential to finally obtain
an efficient symbolic algorithm for realworld
problems.
The contributions of this paper are (1) block
forwarding to update block refinement as soon as
possible, (2) splitdriven refinement that
overapproximates the set of blocks that must
definitely be refined, and (3) block ordering
to fix the order of the blocks for the refinement
in a clever way.
We provide substantial experimental results on
examples from different applications and compare
them to alternative approaches when possible.
The experiments clearly show that the proposed
optimization techniques result in a significant
performance speedup compared to the basic algorithm
as well as to alternative approaches.

Ralf Wimmer, Marc Herbstritt, Bernd Becker: Forwarding, Splitting, and Block Ordering to Optimize
BDDbased Bisimulation Computation
Proceedings of the 10^{th} GI/ITG/GMMWorkshop
„Methoden und Beschreibungssprachen zur Modellierung
und Verifikation von Schaltungen und Systemen” (MBMV), pages 203–212, ShakerVerlag, 2007
pdffile, BibTeX
► Abstract
In this paper we present optimizations
for a BDDbased algorithm for the computation of several
types of bisimulations which play an important role
for minimisation of large systems thus enabling their verification.
The basic principle of the algorithm is partition refinement.
Our proposed optimizations take this refinementstructure as well
as the usage of BDDs for the representation of the system into
account: (1) \emphblock forwarding updates insitu newly refined
blocks of the partition, (2) \emphsplitdriven refinement
approximates the blocks that may be refined, and (3) \emphblock ordering
heuristically suggests a good order in which the blocks will be refined.
We provide substantial experimental results on examples
from different applications and compare them to alternative
approaches. The experiments clearly show that the proposed optimization
techniques result in a significant performance speedup compared to the
basic algorithm as well as to alternative approaches.

Ralf Wimmer, Holger Hermanns
and Marc Herbstritt
and Bernd Becker: Towards Symbolic Stochastic Aggregation
Technical report.
pdffile, BibTeX
► Abstract
Bisimulations are one of the classical means to fight
the state explosion problem. Especially in combination
with symbolic methods, like BDDbased data representation
and algorithms that exploit the compact BDD representation,
they enable the minimization of very large state spaces without
losing relevant properties.
In this report, we show how a symbolic algorithm,
that was originally developed for nonstochastic
systems, can be extended to compute strong and
branching bisimulations on interactive Markov chains (IMCs).
An IMC is a very general model that combines the stochastic
behavior of traditional Markov chains with actionlabeled
transition systems. To the best of our knowledge,
our suggested algorithm is the first symbolic algorithm for
both stochastic \emphstrong bisimulation and stochastic
\emphbranching bisimulation on IMCs.

Ralf Wimmer, Alexander Kortus
and Marc Herbstritt
and Bernd Becker: Symbolic Model Checking for DTMCs with Exact and Inexact Arithmetic
Technical report.
pdffile, BibTeX
► Abstract
In formal verification, \emphreliable results are of utmost
importance. In model checking of digital systems, mainly
incorrect implementations due to logical errors are the source
of wrong results. In probabilistic model checking, numerical
instabilities are an additional source for inconsistent
results.
In this report, we experimentally analyze the impact
of inexact floatingpoint arithmetic on the correctness of the
result in the context of probabilistic model checking of
discretetime Markov chains. Inexact arithmetic performs
implicitly \emphrounding of values that are generated during the
model checking process.
To enable a direct comparison to the state of the art, which relies on
inexact floatingpoint arithmetic, we have implemented a prototypical
probabilistic model checker that provides standard floatingpoint
arithmetic as well as exact arithmetic.
During our experimental evaluation, we found practical examples where
the use of inexact arithmetic produces unacceptable results. Two reasons
for these problems are:
(1) Rounding can change the structure of the system, and
(2) rounding can change the truthvalue of subformulae.
Both issues can result in probabilities that are far away
from the correct ones.
As a summary, this work reveals the demand for investigating reliable
numerical methods within probabilistic model checking.

Ralf Wimmer,
Marc Herbstritt,
Holger Hermanns,
Kelley Strampp,
Bernd Becker: Sigref – A Symbolic Bisimulation Tool Box
Proceedings of the 4^{th} International Symposium on Automated
Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 4218, pages 477–492, Springer, 2006
pdffile, BibTeX
, Original Publication
► Abstract
We present a uniform signaturebased approach to
compute the most popular bisimulations. Our approach is implemented
symbolically using BDDs, which enables the handling of very large
transition systems. Signatures for the bisimulations
are built up from a few generic building blocks, which naturally
correspond to efficient BDD operations. Thus, the definition
of an appropriate signature is the key for a rapid development of
algorithms for other types of bisimulation.
We provide experimental evidence of the viability of this approach
by presenting computational results for many bisimulations on
realworld instances. The experiments show cases where our framework
can handle state spaces efficiently that are far too large to handle
for any tool that requires an explicit state space description.

Ralf Wimmer, Marc Herbstritt, Bernd Becker: Minimization of Large State Spaces
using Symbolic Branching Bisimulation
Proceedings of the 9^{th} IEEE International Workshop on Design &
Diagnostics of Electronic Circuits & Systems (DDECS), pages 9–14, IEEE Computer Society Press, 2006
pdffile, BibTeX
, Original Publication
► Abstract
Bisimulations in general are a powerful concept to minimize large
finite state systems regarding some welldefined observational behavior.
In contrast to strong bisimulation, for branching bisimulation there are
only tools available that work on an explicit state space representation.
In this work we present for the first time a symbolic approach for branching
bisimulation that uses BDDs as basic data structure and that is based on
the concept of signature refinement. First experimental results for problem
instances derived from process algebraic system descriptions show the
feasibility and the robustness of our approach.

Ralf Wimmer, Tobias Nopper, Marc Herbstritt
and Christoph Löffler, Bernd Becker: Collaborative Exercise Management
Proceedings of the 11^{th} World Conference on ELearning in Corporate,
Government, Health Care, & Higher Education (ELearn), pages 3127–3134, Association for the Advancement of Computers in Education (AACE), 2006
pdffile, BibTeX
► Abstract
In this work, we report on a novel tool for managing exercises
used in a collaborative course organization environment at university.
Our approach focuses on the separation of the content of the exercises
and its layout. The latter is based on the typesetting system \LaTeX.
Content management of the exercises is established by a webbased interface.
As a whole, our tool provides a timesaving and unambiguous workflow
for collaborative, time and placeindependent exercise organization.

Eckard Böde, Marc Herbstritt, Holger Hermanns,
Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker: Compositional Performability Evaluation for Statemate
Proceedings of the 3^{rd} International Conference on Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press, 2006
pdffile, BibTeX
, Original Publication
► Abstract
This paper reports on our efforts to link an industrial stateoftheart
modelling tool to academic stateoftheart analysis algorithms. In a
nutshell, we enable timed reachability analysis of uniform
continuoustime Markov decision processes, which are generated from Statemate
models. We give a detailed explanation of several
construction, transformation, reduction, and analysis steps required to
make this possible. The entire tool flow has been implemented, and it is
applied to a nontrivial example.

Marc Herbstritt,
Ralf Wimmer,
Thomas Peikenkamp,
Eckard Böde,
Michael Adelaide,
Sven Johr,
Holger Hermanns,
Bernd Becker: Analysis of Large SafetyCritical Systems: A quantitative Approach
Technical report.
pdffile, BibTeX
► Abstract
The ever increasing complexity of systems requires combined efforts
with respect to analysis and verification to close the socalled
verification gap. On the modeling side, to face this problem, expressive
highlevel methodologies are used to manage system complexity. From the
analysis side it is therefore essential to also start at this level. Due to
powerful symbolic tools – often based on BDDs – consistent highlevel
representations can be generated. The bottleneck for subsequent
system analysis, however, is still the incredible state space of
such representations. This fact gains even more importance when the
intended analysis is bound to explicit tools, e.g.,~for a quantitative
analysis using stochastic model checking.
In this work, we are bridging the gaps between highlevel system descriptions
of safetycritical systems and corresponding explicit state space
representations that can be handled by explicit quantitative analysis tools.
In a first step, our approach safely integrates failure behavior of
safetycritical systems into their highlevel description. Then, structural
reductions are applied. Manageable explicit representations are finally
obtained by a novel BDDbased symbolic branching bisimulation algorithm.
We provide experimental data demonstrating the efficiency of our methods:
safetycritical systems whose size seems to be prohibitive for any explicit
analysis tool at the beginning are reduced by orders of magnitude,
thus paving the way to quantitative analysis without losing relevant
information.