Author name cluster

Leander Tentrup

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.

7 papers

2 author rows

SAT Conference 2019 Conference Paper

Clausal Abstraction for DQBF

Leander Tentrup
Markus N. Rabe

Abstract Dependency quantified Boolean formulas (DQBF) is a logic admitting existential quantification over Boolean functions, which allows us to elegantly state synthesis problems in verification such as the search for invariants, programs, or winning regions of games. In this paper, we lift the clausal abstraction algorithm for quantified Boolean formulas (QBF) to DQBF. Clausal abstraction for QBF is an abstraction refinement algorithm that operates on a sequence of abstractions that represent the different quantifier levels. For DQBF we need to generalize this principle to partial orders of abstractions. The two challenges to overcome are: (1) Clauses may contain literals with incomparable dependencies, which we address by the recently proposed proof rule called Fork Extension, and (2) existential variables may have spurious dependencies, which we prevent by tracking consistency requirements during the execution. Our implementation \(\textsc {dCAQE}\) solves significantly more formulas than the existing DQBF algorithms.

Details

GandALF Workshop 2018 Workshop Paper

Solving QBF by Abstraction

Jesko Hecking-Harbusch
Leander Tentrup

Many verification and synthesis approaches rely on solving techniques for quantified Boolean formulas (QBF). Consequently, solution witnesses, in the form of Boolean functions, become more and more important as they represent implementations or counterexamples. We present a recursive counterexample guided abstraction and refinement algorithm (CEGAR) for solving and certifying QBFs that exploits structural reasoning on the formula level. The algorithm decomposes the given QBF into one propositional formula for every block of quantifiers that abstracts from assignments of variables not bound by this quantifier block. Further, we show how to derive an efficient certification extraction method on top of the algorithm. We report on experimental evaluation of this algorithm in the solver QuAbS (Quantified Abstraction Solver) which won the most recent QBF competition (QBFEVAL'18). Further, we show the effectiveness of the certification approach using synthesis benchmarks and a case study for synthesizing winning strategies in Petri Games.

PDF Details DOI

GandALF Workshop 2016 Workshop Paper

Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time

Leander Tentrup
Alexander Weinert
Martin Zimmermann

We consider the optimization variant of the realizability problem for Prompt Linear Temporal Logic, an extension of Linear Temporal Logic (LTL) by the prompt eventually operator whose scope is bounded by some parameter. In the realizability optimization problem, one is interested in computing the minimal such bound that allows to realize a given specification. It is known that this problem is solvable in triply-exponential time, but not whether it can be done in doubly-exponential time, i. e. , whether it is just as hard as solving LTL realizability. We take a step towards resolving this problem by showing that the optimum can be approximated within a factor of two in doubly-exponential time. Also, we report on a proof-of-concept implementation of the algorithm based on bounded LTL synthesis, which computes the smallest implementation of a given specification. In our experiments, we observe a tradeoff between the size of the implementation and the bound it realizes. We investigate this tradeoff in the general case and prove upper bounds, which reduce the search space for the algorithm, and matching lower bounds.

PDF Details DOI

GandALF Workshop 2016 Workshop Paper

Distributed PROMPT-LTL Synthesis

Swen Jacobs
Leander Tentrup
Martin Zimmermann

We consider the synthesis of distributed implementations for specifications in Prompt Linear Temporal Logic (PROMPT-LTL), which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous systems, we show that, despite being more powerful, the distributed realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to consider an assume-guarantee synthesis problem, as we have to express scheduling assumptions. As asynchronous distributed synthesis is already undecidable for LTL, we give a semi-decision procedure for the PROMPT-LTL assume-guarantee synthesis problem based on bounded synthesis.

PDF Details DOI

SAT Conference 2016 Conference Paper

Non-prenex QBF Solving Using Abstraction

Leander Tentrup

Abstract In a recent work, we introduced an abstraction based algorithm for solving quantified Boolean formulas (QBF) in prenex negation normal form (PNNF) where quantifiers are only allowed in the formula’s prefix and negation appears only in front of variables. In this paper, we present a modified algorithm that lifts the restriction on prenex quantifiers. Instead of a linear quantifier prefix, the algorithm handles tree-shaped quantifier hierarchies where different branches can be solved independently. In our implementation, we exploit this property by solving independent branches in parallel. We report on an evaluation of our implementation on a recent case study regarding the synthesis of finite-state controllers from \(\omega \) -regular specifications.

Details

SAT Conference 2014 Conference Paper

Fast DQBF Refutation

Bernd Finkbeiner
Leander Tentrup

Abstract Dependency Quantified Boolean Formulas (DQBF) extend QBF with Henkin quantifiers, which allow for non-linear dependencies between the quantified variables. This extension is useful in verification problems for incomplete designs, such as the partial equivalence checking (PEC) problem, where a partial circuit, with some parts left open as “black boxes”, is compared against a full circuit. The PEC problem is to decide whether the black boxes in the partial circuit can be filled in such a way that the two circuits become equivalent, while respecting that each black box only observes the subset of the signals that are designated as its input. We present a new algorithm that efficiently refutes unsatisfiable DQBF formulas. The algorithm detects situations in which already a subset of the possible assignments of the universally quantified variables suffices to rule out a satisfying assignment of the existentially quantified variables. Our experimental evaluation on PEC benchmarks shows that the new algorithm is a significant improvement both over approximative QBF-based methods, where our results are much more accurate, and over precise methods based on variable elimination, where the new algorithm scales better in the number of Henkin quantifiers.

Details

Highlights Conference 2013 Conference Abstract

A compositional proof rule for Coordination Logic

Leander Tentrup

We present the first proof system for Coordination Logic (CL). CL provides a logical representation for the distributed realizability problem and extends the game-based temporal logics with quantification over strategies under incomplete information. The proof system is based on a reduction from CL to its decidable fragment. We propose a compositional proof rule which splits a given CL formula into two parts, a decidable CL formula and another, simplified, CL formula. Applying the rule repeatedly transforms the original CL formula into a collection of decidable CL formulas. Our proof system is a complete framework for the synthesis of distributed systems.

PDF Details