Research Reports

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.

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.

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.

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.

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.

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.

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 dened by linear differential equations, possibly including

bounded disturbances.

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.