Publications
A publication list for download can be found here.
2017

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
► 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.

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, Springer
pdffile, BibTeX
► 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, Karina Wimmer, Christoph Scholl, Bernd Becker: Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
Advanced Logic Synthesis, Springer
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, 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
pdffile, BibTeX
► 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
pdffile, BibTeX
► 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.

Bernd Becker, Christoph Scholl, Ralf Wimmer: Verification of Incomplete Designs
Formal System Verification – State of the Art and Future Trends, pages 37–72, Springer
pdffile, BibTeX
► 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?”).
2016

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
pdffile, BibTeX
► 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
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
pdffile, BibTeX
► 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)