Author name cluster

Helmut Veith

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.

14 papers

2 author rows

I&C Journal 2017 Journal Article

On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability

Igor Konnov
Helmut Veith
Josef Widder

Counter abstraction is a powerful tool for parameterized model checking, if the number of local states of the concurrent processes is relatively small. In recent work, we introduced parametric interval counter abstraction that allowed us to verify the safety and liveness of threshold-based fault-tolerant distributed algorithms (FTDA). Due to state space explosion, applying this technique to distributed algorithms with hundreds of local states is challenging for state-of-the-art model checkers. In this paper, we demonstrate that reachability properties of FTDAs can be verified by bounded model checking. To ensure completeness, we need an upper bound on the distance between states. We show that the diameters of accelerated counter systems of FTDAs, and of their counter abstractions, have a quadratic upper bound in the number of local transitions. Our experiments show that the resulting bounds are sufficiently small to use bounded model checking for parameterized verification of reachability properties of several FTDAs, some of which have not been automatically verified before.

Details DOI

CSL Conference 2016 Conference Paper

Monadic Second Order Finite Satisfiability and Unbounded Tree-Width

Tomer Kotek
Helmut Veith
Florian Zuleger

The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese. We prove that the following problem is decidable: Input: (i) A monadic second order logic sentence alpha, and (ii) a sentence beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of alpha and beta may intersect. Output: Is there a finite structure which satisfies alpha and beta such that the restriction of the structure to the vocabulary of alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic MS^{exists card} extending monadic second order logic with linear cardinality constraints of the form |X_{1}|+. .. +|X_{r}| < |Y_{1}|+. .. +|Y_{s}| on the variables X_i, Y_j of the outer-most quantifier block. We prove the decidability of a similar extension of WS1S.

Details

TCS Journal 2015 Journal Article

Closure properties and complexity of rational sets of regular languages

Andreas Holzer
Christian Schallhart
Michael Tautschnig
Helmut Veith

The test specification language FQL describes relevant test goals as regular expressions over program locations, such that each matching test case has an execution path matching this expression. To specify not only test goals but entire suites, FQL describes families of related test goals by regular expressions over extended alphabets: Herein, each symbol corresponds to a regular expression over program locations, and thus, a word in an FQL expression corresponds to a regular expression describing a single test goal. In this paper we provide a systematic foundation for FQL test specifications, which are in fact rational sets of regular languages (RSRLs). To address practically relevant problems like query optimization, we tackle open questions about RSRLs: We settle closure properties of general and finite RSRLs under common set theoretic operations. We also prove complexity results for checking equivalence and inclusion of star-free RSRLs, and for deciding whether a regular language is a member of a general or star-free RSRL.

Details DOI

SAT Conference 2009 Conference Paper

Encoding Treewidth into SAT

Marko Samer
Helmut Veith

Abstract One of the most important structural parameters of graphs is treewidth, a measure for the “tree-likeness” and thus in many cases an indicator for the hardness of problem instances. The smaller the treewidth, the closer the graph is to a tree and the more efficiently the underlying instance often can be solved. However, computing the treewidth of a graph is NP -hard in general. In this paper we propose an encoding of the decision problem whether the treewidth of a given graph is at most k into the propositional satisfiability problem. The resulting SAT instance can then be fed to a SAT solver. In this way we are able to improve the known bounds on the treewidth of several benchmark graphs from the literature.

Details

LPAR Conference 2007 Conference Paper

On the Notion of Vacuous Truth

Marko Samer
Helmut Veith

Abstract The model checking community has proposed numerous definitions of vacuous satisfaction, i. e. , formal criteria which tell whether a temporal logic specification holds true on a system model for the intended reason. In this paper we attempt to study the notion of vacuous satisfaction from first principles. We show that despite the apparently vague formulation of the vacuity problem, most proposed notions of vacuity for temporal logic can be cast into a uniform and simple framework, and compare previous approaches to vacuity detection from this unified point of view.

Details

TIME Conference 2005 Conference Paper

Deterministic CTL Query Solving

Marko Samer
Helmut Veith

Temporal logic queries provide a natural framework to extend the realm of model checking from mere verification of engineers' specifications to computing previously unknown temporal properties of a system. Formally, temporal logic queries are patterns of temporal logic specifications which contain placeholders for subformulas; a solution to a temporal logic query is an instantiation which renders the specification true. In this paper, we investigate temporal logic queries that can be solved deterministically, i. e. , solving such queries can be reduced in a deterministic manner to solving their subqueries at appropriate system states. We show that this kind of determinism is intimately related to the notion of intermediate collecting queries studied by the authors in previous work. We describe a large class of deterministically solvable CTL queries and devise a BDD-based symbolic algorithm for this class.

Details

CSL Conference 2003 Conference Paper

Friends or Foes? Communities in Software Verification (Invited Lecture)

Helmut Veith

Abstract In contrast to hardware which is finite-state and based on relatively few ample principles, software systems generally give rise to infinite state spaces, and are described in terms of programming languages involving rich semantical concepts. The challenges of software verification can be addressed only by a combined effort of different communities including, most notably, model checking, theorem proving, symbolic computation, static analysis, compilers, and abstract interpretation. We focus on a recent family of tools which use predicate abstraction and theorem proving to extract a finite state system amenable to model checking.

Details

SAT Conference 2003 Conference Paper

SAT Based Predicate Abstraction for Hardware Verification

Edmund M. Clarke
Muralidhar Talupur
Helmut Veith
Dong Wang

Abstract Predicate abstraction is an important technique for extracting compact finite state models from large or infinite state systems. Predicate abstraction uses decision procedures to compute a model which is amenable to model checking, and has been used successfully for software verification. Little work however has been done on applying predicate abstraction to large scale finite state systems, most notably, hardware, where the decision procedures are SAT solvers. We consider predicate abstraction for hardware in the framework of Counterexample-Guided Abstraction Refinement where in the course of verification, the abstract model has to be repeatedly refined. The goal of the refinement is to eliminate spurious behavior in the abstract model which is not present in the original model, and gives rise to false negatives (spurious counterexamples). In this paper, we present two efficient SAT-based algorithms to refine abstract hardware models which deal with spurious transitions and spurious counterexamples respectively. Both algorithms make use of the conflict graphs generated by SAT solvers. The first algorithm extracts constraints from the conflict graphs which are used to make the abstract model more accurate. Once an abstract transition is determined to be spurious, our algorithm does not need to make any additional calls to SAT solver. Our second algorithm generates a compact predicate which eliminates a spurious counterexample. This algorithm uses the conflict graphs to identify the important concrete variables that render the counterexample spurious, creates an additional predicate over these concrete variables, and adds it to the abstract model. Experiments over hardware designs with several thousands of registers demonstrate the effectiveness of our methods.

Details

CSL Conference 2003 Conference Paper

Validity of CTL Queries Revisited

Marko Samer
Helmut Veith

Abstract We systematically investigate temporal logic queries in model checking, adding to the seminal paper by William Chan at CAV 2000. Chan’s temporal logic queries are CTL specifications where one unspecified subformula is to be filled in by the model checker in such a way that the specification becomes true. Chan defined a fragment of CTL queries called \(\mbox{CTL}^{v}\) which guarantees the existence of a unique strongest solution. The starting point of our paper is a counterexample to this claim. We then show how the research agenda of Chan can be realized by modifying his fragment appropriately. To this aim, we investigate the criteria required by Chan, and define two new fragments \(\mbox{CTL}^{v}_{new}\) and \(\mbox{CTL}^{d}\) where the first is the one originally intended; the latter fragment also provides unique strongest solutions where possible but admits also cases where the set of solutions is empty.

Details

TCS Journal 2002 Journal Article

On the complexity of data disjunctions

Thomas Eiter
Helmut Veith

We study the complexity of data disjunctions in disjunctive deductive databases (DDDBs). A data disjunction is a disjunctive ground clause R( c ̄ 1)⋯R( c ̄ k), k⩾2, which is derived from the database such that all atoms in the clause involve the same predicate R. We consider the complexity of deciding existence and uniqueness of a minimal data disjunction, as well as actually computing one, both for propositional (data) and nonground (program) complexity of the database. Our results extend and complement previous results on the complexity of disjunctive databases, and provide newly developed tools for the analysis of the complexity of function computation.

Details DOI

CSL Conference 1999 Conference Paper

Quantifier Elimination in Fuzzy Logic

Matthias Baaz
Helmut Veith

Abstract We investigate quantifier elimination of first order logic over fuzzy algebras. Fuzzy algebras are defined from continuous t-norms over the unit interval, and subsume Łukasiewicz [28, 29], Gödel [16, 12] and Product [19] Logic as most prominent examples. We show that a fuzzy algebra has quantifier elimination iff it is one of the abovementioned logics. Moreover, we show quantifier elimination for various extensions of these logics, and observe other model-theoretic properties of fuzzy algebras. Further considerations are devoted to approximation of fuzzy logics by finite-valued logics.

Details

MFCS Conference 1998 Conference Paper

Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics

Matthias Baaz
Agata Ciabattoni
Christian G. Fermüller
Helmut Veith

Abstract We investigate the proof theory of Urquhart's C and other logics underlying the most prominent fuzzy logics, such as Gödel, Product, and łukasiewicz logic. All these logics share the property that their truth values are linearly ordered. We define hypersequent calculi for such logics, and show the following results: (1) Contraction-free counterparts of intuitionistic logic and Gödel logic (including C ) admit cut-elimination. (2) Validity in these logics is decidable. (3) Hajek's basic fuzzy logic BL properly extends the contraction-free Gödel logic; the axiom for commutativity of the minimum is independent from the other axioms of BL. (4) All abovementioned logics are distinct from each other.

Details

I&C Journal 1998 Journal Article

Succinct Representation, Leaf Languages, and Projection Reductions

Helmut Veith

In this article, the following results are shown: 1. For succinctly encoded problemss(A), completeness under polynomial time reductions is equivalent to completeness under projection reductions, an extremely weak reduction defined by a quantifier-free projective formula. 2. The succinct versions(Aof a computational problemAis complete under projection reductions for the class of problems characterizable with leaf languageA, but not complete undermonotoneprojections. 3. A strong conversion lemma: IfAis reducible toBin polylogarithmic time, then the succinct version ofAis monotone projection reducible to the succinct version ofB. This result strengthens previous results by Papadimitriou and Yannakakis, and Balcázar and Lozano. It allows iterated application for multiple succinct problems. 4. For all syntactic complexity classes there exist complete problems undermonotoneprojection reductions. This positively answers a question by Stewart for a large number of complexity classes.

Details DOI

MFCS Conference 1995 Invited Paper

Second Order Logic and the Weak Exponential Hierarchies

Georg Gottlob
Nicola Leone
Helmut Veith

Abstract Second order logic over finite structures is well-known to capture the levels of the polynomial hierarchy PH. Recently, it has been shown that Θ 1 k — the first order closure of second order Σ 1 m — captures the class Θ P k = \(L^{\Sigma _k^P }\), a natural intermediate class of the polynomial hierarchy [12]. In this paper we show that with respect to expression complexity, second order logic characterizes the levels of the weak exponential hierarchy EH. Moreover, we extend these results to intermediate classes EΘ P k in EH which correspond to the Θ P k classes in PH. To this end, in extending previous results, we show completeness under projection translations of certain quantified propositional formula languages for Θ P k. Those, as well as quantified Boolean formulas are applied to improved complexity upgrade techniques based on the ”succinct input” paradigm. Thus, we obtain a uniform treatment for obtaining expression complexity results for a large number of natural languages. We exhibit examples from database theory and nonmonotonic reasoning. In particular, we investigate the expression complexity of first order logic with Henkin quantifiers and default logic.

Details