Research Reports

• Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization", in AVACS Technical Report, (2016), Vol. 103, pp. 93 p.
Citation
Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization", in AVACS Technical Report, (2016), Vol. 103, pp. 93 p.
Abstract
This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can -- in contrast to purely functional controller models -- not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states.
Export
• Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata", in AVACS Technical Report, (2011), Vol. 70, pp. 31 p.
Citation
Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata", in AVACS Technical Report, (2011), Vol. 70, pp. 31 p.
Abstract
This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of convex safety properties with exhaustive entry states can be verified in polynomial time and time-bounded reachability can be decided in nondeterministic polynomial time for non-parametric verification and in exponential time for parametric verification. Properties with exhaustive entry states are restricted to runs originating in a (specified) inner envelope of some mode-invariant. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.
Export
• Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems", in AVACS Technical Report, (2011), Vol. 76.
Citation
Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems", in AVACS Technical Report, (2011), Vol. 76.
Abstract
We describe an approach to integrate incremental ow pipe computation into a fully symbolic backward model checker for hybrid systems. Our method combines the advantages of symbolic state set representation, such as the ability to deal with large numbers of boolean variables, with an effcient way to handle continuous ows dened by linear differential equations, possibly including bounded disturbances.
Export
• Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Towards Verification of the Pastry Protocol using TLA+", in Research Report, (2011), pp. 51 p.
Citation
Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Towards Verification of the Pastry Protocol using TLA+", in Research Report, (2011), pp. 51 p.
Abstract
Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verication. We have modeled Pastry's core routing algorithms and communication protocol in the specication language TLA+. In order to validate the model and to search for bugs we employed the TLA+ model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA+. A rst result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.
Export
• Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies", in AVACS Technical Report, (2010), Vol. 66, pp. 40 p.
Citation
Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies", in AVACS Technical Report, (2010), Vol. 66, pp. 40 p.
Abstract
The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. \begin{itemize} \item For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. \item At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. \item At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. \end{itemize} We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
Export
• Carsten Ihlemann and Viorica Sofronie-Stokkermans, "On Hierarchical Reasoning in Combinations of Theories", in AVACS Technical Report, (2010), Vol. 60, pp. 26 p.
Citation
Carsten Ihlemann and Viorica Sofronie-Stokkermans, "On Hierarchical Reasoning in Combinations of Theories", in AVACS Technical Report, (2010), Vol. 60, pp. 26 p.
Abstract
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.
Export
• Carsten Ihlemann and Viorica Sofronie-Stokkermans, "System Description: H-PILoT (Version 1.9)", in AVACS Technical Report, (2010), Vol. 61, pp. 45 p.
Citation
Carsten Ihlemann and Viorica Sofronie-Stokkermans, "System Description: H-PILoT (Version 1.9)", in AVACS Technical Report, (2010), Vol. 61, pp. 45 p.
Abstract
This system description provides an overview of H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories. H-PILoT reduces deduction problems in the theory extension to deduction problems in the base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability of the formulae obtained after the reduction. For a certain type of theory extension (namely for {\em local theory extensions}) this hierarchical reduction is sound and complete and -- if the formulae obtained this way belong to a fragment decidable in the base theory -- H-PILoT provides a decision procedure for testing satisfiability of ground formulae, and can also be used for model generation.
Export
• Martin Suda, Christoph Weidenbach, and Patrick Wischnewski, "On the saturation of YAGO", in Research Report, (2010), pp. 50 p.
Citation
Martin Suda, Christoph Weidenbach, and Patrick Wischnewski, "On the saturation of YAGO", in Research Report, (2010), pp. 50 p.
Export
• Matthias Horbach and Christoph Weidenbach, "Decidability Results for Saturation-based Model Building", in Research Report, (2009), pp. 38 p.
Citation
Matthias Horbach and Christoph Weidenbach, "Decidability Results for Saturation-based Model Building", in Research Report, (2009), pp. 38 p.
Abstract
Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. Based on an extension of our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting, we describe models given by ARM (Atomic Representations of term Models) or DIG (Disjunctions of Implicit Generalizations) representations as minimal models of finite saturated clause sets. This allows us to present several new decidability results for validity in such models. These results extend in particular the known decidability results for ARM and DIG representations.
Export
• Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains", in Research Report, (2009), pp. 49 p.
Citation
Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains", in Research Report, (2009), pp. 49 p.
Abstract
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and refutationally complete in the limit for a first-order fixed domain semantics. For saturated Horn theories and classes of positive formulas, we can even employ the calculus to prove properties of the minimal model itself, going beyond the scope of known superposition-based approaches.
Export
• Matthias Horbach and Christoph Weidenbach, "Deciding the Inductive Validity of Forall Exists* Queries", (2009).
Citation
Matthias Horbach and Christoph Weidenbach, "Deciding the Inductive Validity of Forall Exists* Queries", (2009).
Abstract
We present a new saturation-based decidability result for inductive validity. Let $\Sigma$ be a finite signature in which all function symbols are at most unary and let $N$ be a satisfiable Horn clause set without equality in which all positive literals are linear. If $N\cup\{A_1,\ldots,A_n\rightarrow\}$ belongs to a finitely saturating clause class, then it is decidable whether a sentence of the form $\forall\exists^* (A_1\wedge\ldots\wedge A_n)$ is valid in the minimal model of $N$.
Export
• Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation", (2009).
Citation
Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation", (2009).
Export
• Christoph Weidenbach and Patrick Wischnewski, "Contextual Rewriting", (2009).
Citation
Christoph Weidenbach and Patrick Wischnewski, "Contextual Rewriting", (2009).
Export
• Arnaud Luc Fietzke and Christoph Weidenbach, "Labelled splitting", in Research Report, (2008), pp. 45 p.
Citation
Arnaud Luc Fietzke and Christoph Weidenbach, "Labelled splitting", in Research Report, (2008), pp. 45 p.
Abstract
We define a superposition calculus with explicit splitting and an explicit, new backtracking rule on the basis of labelled clauses. For the first time we show a superposition calculus with explicit backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from SPASS. An experimental evaluation of an implementation of the new rule shows that it improves considerably the previous SPASS splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.
Export
• Viorica Sofronie-Stokkermans, "Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems", in AVACS Technical Report, (2008), Vol. 46.
Citation
Viorica Sofronie-Stokkermans, "Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems", in AVACS Technical Report, (2008), Vol. 46.
Abstract
In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space (where the topology expresses how the interacting systems share the information). This allows us to use results from categorical logic (and in particular geometric logic) to describe which type of properties are transferred, if valid locally in all component systems, also at a global level, to the system obtained by interconnecting the individual systems. The main area of application is to modular verification of complex systems. We illustrate the ideas by means of an example involving a family of interacting controllers for trains on a rail track.
Export
• Viorica Sofronie-Stokkermans, "Efficient Hierarchical Reasoning about Functions over Numerical Domains", in AVACS Technical Report, (2008), Vol. 45, pp. 17 p.
Citation
Viorica Sofronie-Stokkermans, "Efficient Hierarchical Reasoning about Functions over Numerical Domains", in AVACS Technical Report, (2008), Vol. 45, pp. 17 p.
Abstract
We show that many properties studied in mathematical analysis (monotonicity, boundedness, inverse, Lipschitz properties, possibly combined with continuity or derivability) are expressible by formulae in a class for which sound and complete hierarchical proof methods for testing satisfiability of sets of ground clauses exist. The results are useful for automated reasoning in mathematical analysis and for the verification of hybrid systems.
Export
• Thomas Hillenbrand and Christoph Weidenbach, "Superposition for Finite Domains", in Max-Planck-Institut für Informatik / Research Report, (2007), pp. 25 p.
Citation
Thomas Hillenbrand and Christoph Weidenbach, "Superposition for Finite Domains", in Max-Planck-Institut für Informatik / Research Report, (2007), pp. 25 p.
Export
• Viorica Sofronie-Stokkermans, "Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators", in Research Report / Max-Planck-Institut für Informatik, (2001), pp. 41 p.
Citation
Viorica Sofronie-Stokkermans, "Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators", in Research Report / Max-Planck-Institut für Informatik, (2001), pp. 41 p.
Abstract
In this paper we establish a link between satisfiability of universal sentences with respect to classes of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal (Horn) sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal (Horn) theory of some such classes. In particular, we obtain exponential decision procedures for the universal Horn theory of (i) the class of all bounded distributive lattices with operators, (ii) for the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, and a doubly-exponential decision procedure for the universal Horn theory of the class of all Heyting algebras.
Export
• Uwe Waldmann, "Superposition and chaining for totally ordered divisible abelian groups", in Research Report / Max-Planck-Institut für Informatik, (2001), pp. 40 p.
Citation
Uwe Waldmann, "Superposition and chaining for totally ordered divisible abelian groups", in Research Report / Max-Planck-Institut für Informatik, (2001), pp. 40 p.
Abstract
We present a calculus for first-order theorem proving in the presence of the axioms of totally ordered divisible abelian groups. The calculus extends previous superposition or chaining calculi for divisible torsion-free abelian groups and dense total orderings without endpoints. As its predecessors, it is refutationally complete and requires neither explicit inferences with the theory axioms nor variable overlaps. It offers thus an efficient way of treating equalities and inequalities between additive terms over, e.g., the rational numbers within a first-order theorem prover.
Export
• Uwe Waldmann, "Cancellative superposition decides the theory of divisible torsion-free abelian groups", in Research Report / Max-Planck-Institut für Informatik, (1999), pp. 23 p.
Citation
Uwe Waldmann, "Cancellative superposition decides the theory of divisible torsion-free abelian groups", in Research Report / Max-Planck-Institut für Informatik, (1999), pp. 23 p.
Abstract
In divisible torsion-free abelian groups, the efficiency of the cancellative superposition calculus can be greatly increased by combining it with a variable elimination algorithm that transforms every clause into an equivalent clause without unshielded variables. We show that the resulting calculus is a decision procedure for the theory of divisible torsion-free abelian groups.
Export
• Viorica Sofronie-Stokkermans, "Resolution-based Theorem Proving for SHn-Logics", (Technische Universität Wien, Vienna, Austria, 1998).
Citation
Viorica Sofronie-Stokkermans, "Resolution-based Theorem Proving for SHn-Logics", (Technische Universität Wien, Vienna, Austria, 1998).
Abstract
In this paper we illustrate by means of an example, namely SHn-logics, a method for translation to clause form and automated theorem proving for first-order many-valued logics based on distributive lattices with operators.
Export
• Reiner Hähnle, Manfred Kerber, and Christoph Weidenbach, "Common Syntax of the DFG-Schwerpunktprogramm ''Deduktion''", (Universität Karlsruhe, Karlsruhe, 1996).
Citation
Reiner Hähnle, Manfred Kerber, and Christoph Weidenbach, "Common Syntax of the DFG-Schwerpunktprogramm ''Deduktion''", (Universität Karlsruhe, Karlsruhe, 1996).
Export
• Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder, "Basic paramodulation", in Research Report / Max-Planck-Institut für Informatik, (1993), pp. 36 p.
Citation
Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder, "Basic paramodulation", in Research Report / Max-Planck-Institut für Informatik, (1993), pp. 36 p.
Abstract
We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the {\em basic\/} strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.
Export
• Peter Baumgartner and Uwe Waldmann, "Hierarchic Superposition with Weak Abstraction", in Research Report, (2013), pp. 45 p.
Citation
Peter Baumgartner and Uwe Waldmann, "Hierarchic Superposition with Weak Abstraction", in Research Report, (2013), pp. 45 p.
Abstract
Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide a new completeness result for the fragment where all background-sorted terms are ground.
Export
• Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in AVACS Technical Report, (2015), Vol. 111, pp. 52 p.
Citation
Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in AVACS Technical Report, (2015), Vol. 111, pp. 52 p.
Export
• Arnaud Fietzke, Evgeny Kruglov, and Christoph Weidenbach, "Automatic Generation of Invariants for Circular Derivations in SUP(LA) 1", in Research Report, (2012), pp. 26 p.
Citation
Arnaud Fietzke, Evgeny Kruglov, and Christoph Weidenbach, "Automatic Generation of Invariants for Circular Derivations in SUP(LA) 1", in Research Report, (2012), pp. 26 p.
Abstract
The hierarchic combination of linear arithmetic and firstorder logic with free function symbols, FOL(LA), results in a strictly more expressive logic than its two parts. The SUP(LA) calculus can be turned into a decision procedure for interesting fragments of FOL(LA). For example, reachability problems for timed automata can be decided by SUP(LA) using an appropriate translation into FOL(LA). In this paper, we extend the SUP(LA) calculus with an additional inference rule, automatically generating inductive invariants from partial SUP(LA) derivations. The rule enables decidability of more expressive fragments, including reachability for timed automata with unbounded integer variables. We have implemented the rule in the SPASS(LA) theorem prover with promising results, showing that it can considerably speed up proof search and enable termination of saturation for practically relevant problems.
Export
• Matthias Horbach and Viorica Sofronie-Stokkermans, "Obtaining Finite Local Theory Axiomatizations via Saturation", in AVACS Technical Report, (2014), Vol. 93, pp. 26 p.
Citation
Matthias Horbach and Viorica Sofronie-Stokkermans, "Obtaining Finite Local Theory Axiomatizations via Saturation", in AVACS Technical Report, (2014), Vol. 93, pp. 26 p.
Abstract
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.
Export
• Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in eScholar, (2015), pp. 22 p.
Citation
Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in eScholar, (2015), pp. 22 p.
Export
• Martin Suda and Christoph Weidenbach, "Labelled Superposition for PLTL", in Research Reports, (2012), pp. 42 p.
Citation
Martin Suda and Christoph Weidenbach, "Labelled Superposition for PLTL", in Research Reports, (2012), pp. 42 p.
Abstract
This paper introduces a new decision procedure for PLTL based on labelled superposition. Its main idea is to treat temporal formulas as infinite sets of purely propositional clauses over an extended signature. These infinite sets are then represented by finite sets of labelled propositional clauses. The new representation enables the replacement of the complex temporal resolution rule, suggested by existing resolution calculi for PLTL, by a fine grained repetition check of finitely saturated labelled clause sets followed by a simple inference. The completeness argument is based on the standard model building idea from superposition. It inherently justifies ordering restrictions, redundancy elimination and effective partial model building. The latter can be directly used to effectively generate counterexamples of non-valid PLTL conjectures out of saturated labelled clause sets in a straightforward way.
Export