Author name cluster

Ralf Wimmer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

TCS Journal 2022 Journal Article

Solving dependency quantified Boolean formulas using quantifier localization

Aile Ge-Ernst
Christoph Scholl
Juraj Síč
Ralf Wimmer

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), while non-prenex DQBFs have almost not been studied in the literature. In this paper, we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks, including all instances from the QBFEVAL'18–'20 competitions, clearly show that quantifier localization pays off in this context.

Details DOI

AAAI Conference 2019 Conference Paper

A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving

Christoph Scholl
Jie-Hong Roland Jiang
Ralf Wimmer
Aile Ge-Ernst

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 ΣP 3 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 state-of-the-art DQBF solvers on a number of benchmarks, including the 2018 DQBF evaluation benchmarks.

PDF Details

IJCAI Conference 2019 Conference Paper

Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks

Steven Carr
Nils Jansen
Ralf Wimmer
Alexandru Serban
Bernd Becker
Ufuk Topcu

We study strategy synthesis for partially observable Markov decision processes (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 recurrent neural network (RNN) to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory 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.

PDF Details

TCS Journal 2014 Journal Article

Minimal counterexamples for linear-time probabilistic verification

Ralf Wimmer
Nils Jansen
Erika Ábrahám
Joost-Pieter Katoen
Bernd Becker

Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time 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 NP-complete 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.

Details DOI