ABSTRACTS

Automating Interactive Protocol Verification

KI 2008: Advances in Artificial Intelligence, 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008. Proceedings

Showing the absence of security hazards in cryptographic protocols is of major interest in the area of protocol security analysis. Standard model checking techniques - despite their advantages of being both fast and automatic - serve as mere debuggers that allow the user at best to detect security risks if they exist at all. In general they are not able to guarantee that all such potential hazards can be found, though. A full verification usually involves induction and therefore can hardly be fully automatic. Therefore the definition and application of suitable heuristics has turned out to become a central necessity. This paper describes how we attack this problem with the help of the Verification Support Environment (VSE) and how we nevertheless arrive at a high degree of automation.

Available: BibTeX-Entry PDF available upon request

Computer Safety, Reliability, and Security, 26th International Conference, SAFECOMP 2007, Nuremberg, Germany, September 18-21, 2007

Safety and security guarantees for individual applications in almost all cases depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs running on these. In particular for formal approaches the problem is to formalize these assumptions without looking at the (formal) model of the operating system (including the machines that execute applications) in all detail. The work described in the paper proposes a modular approach which uses histories of observable events to specify runs of distributed instances of the system. The overall verification approach decomposes the given verification problem into local tasks along the lines of assume-guarantee reasoning. As an example the paper discusses the specification and implementation of the SMTP scenario. It shows in detail how this methodology is utilized within the Verification Support Environment (VSE) to verify the SMTP server part.

Available: BibTeX-Entry PDF available upon request

Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007

Safety and security guarantees for individual applications in general depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs that are executed on these platforms. The problem for formal approaches is to formalize these assumptions without having to look at the details of the (formal) model of the operating system (including the machines that execute applications). The work described in this paper presents a modular approach which uses histories of observable events to specify runs of distributed instances of the system. The overall verification approach decomposes the given verification problem into local tasks along the lines of assume-guarantee reasoning. In this paper we focus on this methodology and on its realization in the Verification Support Environment (VSE). We also illustrate the proposed approach with the help of a suitable example, namely the specification and verification of an SMTP server whose implementation makes extensive use of various system calls as e.g. fork and socket commands.

Available: BibTeX-Entry PDF

Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday

Formal software development turns out to become one of the key issues in software engineering. Today an enormous variety of methods and tools exist that serve as an aid for the software engineer to formally specify and verify large-scaled systems. This paper reviews some of the most important general notions in formal software engineering and, in particular, gives an overview on VSE (Verification Support Environment), a tool that supports both hierarchical specification and formal verification.

Available: BibTeX-Entry PDF available upon request

Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings

Today we are confronted with an enormous variety of formal software engineering approaches and tools. Among these are many that address the critical early stages of software development. However, only little attention has been paid to the integration of different specialised approaches and to the overall development process. In this paper we present a technique for formal requirements analysis (observer models) that deals with particular perspectives on a system rather than with particular aspects of it. A realistic gasburner example illustrates the overall approach.

Available: BibTeX-Entry PDF available upon request

Proceedings of the Verification Workshop VERIFY in conjunction with CADE-18 and FLoC 2002, Copenhagen, Denmark

Verification of non-linear hybrid systems is a challenging task. Unlike manyy other verification methods the deduction-based verification approach we investigate in this paper avoids approximations and operates directly on the original non-linear system specifications. This approach, however, requires the solution of non-trivial mathematical sub-tasks. We propose to model existing reasoning systems, such as computer algebra systems and constraint solvers, as mathematical services and to provide them in a network of mathematical tools in a way that they can reasonably support subtasks as they may occur in formal methods applications. The motivation is to make it simpler to implement and test verification approaches by out-sourcing complex but precisely identifiable mathematical subtasks for which specialised reasoners do already exist.

Available: BibTeX-Entry PDF

Proceedings of the ESA Workshop on On-Board Autonomy, Oct 2001

It is well known that in many cases severe errors occur in the early stages of the software development process. Following this insight, considerable emphasis was put on requirements engineering. Formal methods provide means for the abstract yet precise description of required system properties. However, specialized description techniques are needed to treat certain aspects adequately. Moreover, complex systems often make it necessary to cover several of these views. Among the most critical and most difficult (to describe) aspects of systems behaviors are realtime properties. A major problem in this area lies in the complexity of timing constraints and the variety of situations that can appear in such systems. It turned out that timed automata or (linear) hybrid automata serve as a comprehensive mean to express temporal behavior. Verification Support Environment (VSE) supports abstract system specifications, the formulation and proof of safety an security properties, and refinements. The formal development method of VSE is based on Abstract Data Types and Temporal Logic. The aim of the work presented here is to integrate hybrid automata as a means for comprehensively describing realtime properties into the VSE method where an abstract system specification serves as the starting point of a formal refinement process. Hybrid automata (translated into VSE) provide a realtime view on these systems. Additional requirements specifications representing different views of the behavior can be "linked" to the same specification.

Available: BibTeX-Entry PDF

Proceedings of the 4th Workshop on Tools for System Design and Verification, Universität Ulm, Ulmer Informatik-Berichte

Available: BibTeX-Entry

Eighth Workshop on Automated Reasoning - Bridging the Gap between Theory and Practice, University of York, March 22-23, 2001

Available: PS BibTeX-Entry

Proceedings of the Fourteenth International Florida Artificial Intelligence Research Society Conference, May 2001

In formally analyzing and developing industrial sized systems we are often confronted with the problem of expressing realtime properties. Especially in safety critical applications as, for example, in embedded systems or in control software, these properties are crucial for the right functioning of the systems. There are numerous suitable approaches that allow us to specify realtime properties: MTL, TLA or VSE-SL to name a few, and also there are various tools available to formally develop such systems. But in most cases the approaches are trimmed for their own highly specialized application area. We try to overcome this restriction by exploiting the advantages of a (fairly general) formal development tool like VSE-II and the rather specialized Hybrid Automata by combining these two approaches.

Available: BibTeX-Entry (gzipped) PS

Proceedings of the 3rd International Workshop: Hybrid Systems -- Computation and Control, March 2000

In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. Experiments show that this approach is particularly interesting in cases where a standard reachab lity analysis would require to travel often through some of the given system locations.

Available: BibTeX-Entry (gzipped) DVI (gzipped) PS

Handbook of Automated Reasoning

Available: BibTeX-Entry (gzipped) PS

Handbook of Automated Reasoning

Available: BibTeX-Entry (gzipped) PS

Proceedings of the 15th International Conference on Automated Deduction, CADE98

In this paper we focus on two powerful techniques to obtain compact clause normal forms: Renaming of formulae and refined Skolemization methods. We illustrate their effect on various examples. By an exhaustive experiment of all first-order TPTP problems, it shows that our clause normal form transformation yields fewer clauses and fewer literals than the methods known and used so far. This often allows for exponentially shorter proofs and, in some cases, it makes it even possible for a theorem prover to find a proof where it was unable to do so with more standard clause normal form transformations.

Available: BibTeX-Entry (gzipped) PS

Technical Report, Max-Planck-Institute for Computer Science, MPI-I-1999-2-006

In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. This is done by representing a given verification problem as a second-order predicate logic formula which is to be solved (proved valid) with the help of a second-order quantifier elimination method. In contrast to many ``standard'' model checking approaches the method as described in this paper does not perform a forward or backward reachability analysis. Experiments show that this approach is particularly interesting in cases where a standard reachability analysis would require to travel often through some of the given system locations. In addition, the approach offers possibilities to proceed where ``standard'' reachability analysis approaches do not terminate.

Available: BibTeX-Entry (gzipped) PS

Journal of the IGPL, vol. 6, nr. 6, pp. 875-899, 1998

In modal logics we are interested in classes of frames that characterize the logic under consideration. Such classes are usually distinguished by their respective frame properties. In general these characterizations are not unique and it is desirable to find a strongest possible. In this article an approach is presented which helps in this respect. It allows us to transform a given background theory into one which is more general and which modal logics cannot distinguish from the former because of their syntactic and semantic restrictions. The underlying technique is based on the idea to find conservative extensions of a given logic whose frame properties allow us to extract significantly stronger characterizations of the original logic.

Available: BibTeX-Entry (gzipped) PS

Proceedings of the First International Joint Conference on Qualitative and Quantitative Practical Reasoning, ECSQARU/FAPR'97, Bad Honnef, Germany, June 1997

Available: BibTeX-Entry

Technical Report, Max-Plamck-Institute for Computer Science, 1996

Available: BibTeX-Entry(gzipped) PS

Second--Order predicate logic formulae with existentially or universally quantified predicate variables occur in various applications, as for instance in default reasoning with circumscription or correspondence theory in non-classical logics. In the latter cases it is important to find an equivalent first--order formula for a given formula with predicate quantifiers. Following early approaches by Wilhelm Ackermann a number of algorithms have been developed which accept a formula with predicate quantifiers as input and compute an equivalent first--order formula as output. In this chapter we give an overview of these algorithms and some of their applications. At least one algorithm is implemented and publicly available.

Available: BibTeX-Entry (gzipped) PS

This paper is about automated techniques for second-order quantifier elimination and (modal logic) correspondence theory. Given a modal schema and a semantics based method of translating modal formulae into fist-order ones, we try to derive automatically a fixpoint formula characterizing precisely the class of frames validating this schema. We propose to consider fixpoint calculus as the underlying formalism rather than the classical first-order logic in order to be able to express more subtle correspondences. The technique we consider can, in many cases, be easily applied without any computer support.
Although we mainly concentrate on Kripke semantics, our fixpoint approach is much more general, as it is based on the elimination of second-order quantifiers from formulae. Thus it can be applied in second-order theorem proving as well. We show some application examples for the method which may serve as new, automated proofs of the respective correspondences.

Available: BibTeX-Entry (gzipped) PS

In this paper a technique is presented which provides us with a means to develop resolution-based calculi for (first-order) modal and temporal logics. The approach is based on three parts: A special translation technique from modal and temporal logic formulae into classical predicate logic, a certain kind of saturation technique which is to be applied to given background theories, and an extraction of either suitable ``simpler'' background theories or logic-specific inference rules. The former is interesting in case existing classical logic theorem provers are to be utilized; the latter gains importance if one is prepared to extend theorem provers that are already at hand.

Available: DVI BibTeX-Entry

In modal logics we are interested in classes of frames which determine the logic under consideration. Such classes are usually distinguished by their respective frame properties, often also called the modal logic's background theory. In general these characterizations are not unique and it is desireable (and that not only from a theorem prover's perspective) to find a strongest possible. In this paper an approach is presented which helps in this respect. It allows us to transform a given background theory into one which is more general and which modal logics cannot distinguish from the former because of their syntactic and semantic restrictions. The underlying technique is based on the idea to find conservative extensions (of a given logic) whose determining properties serve as a starting point from which it is possible to extract significantly stronger characterizations of the original logic.

Available: (gzipped) PS BibTeX-Entry

This paper is about automated techniques for (modal logic) correspondence theory. The theory we deal with concerns the problem of finding fixpoint characterizations of modal axiom schemata. Given a modal schema and a semantics based method of translating modal formulae into classical ones, we try to derive automatically a fixpoint formula characterizing precisely the class of frames validating this schema. The technique we consider can, in many cases, be easily applied without any computer support. Although we mainly concentrate on Kripke semantics, our fixpoint approach is much more general, as it is based on the elimination of second-order quan- tifiers from formulae. Thus it can be applied in second-order theorem proving as well. We show some application examples for the method which may serve as new, automated proofs of the respective correspondences.

Available: DVI BibTeX-Entry

Standard logic programming languages like Prolog lack thepossibility of dealing with modalities and/or sorts. A first idea how to overcome this problem (and that without changing anything on Prolog itself) would be to apply the well-known relational translation approaches from modal and sorted logic into first-order predicate logic and to feed this translation result into Prolog. This, however, leads into other problems: firstly, the transformed problem is usually of much bigger size (number of clauses) than the original one and, secondly, very often it is not even in Horn form anymore.
In this paper a translation approach is proposed which avoids both of these problems, i.e. the number of clauses after translation is exactly as big as it would have been if we simply ignored the modal operators and sort restrictions and, also, the result is in Horn form provided it was already before (modulo modal operators and sorts).

Available: DVI BibTeX-Entry

In this paper we focus on the application of description logics to natural language processing. In cooperation with the {\sc pracma} project we have been developing a suitably extended knowledge representation system, called {\sc motel}. In our approach to agent modelling and natural language processing we use an extension of the well-known description language $\cal ALC$. Our system {\sc motel}\ serves on one hand as a knowledge base for the natural language front-end, and on the other hand, it provides powerful {\em logical\/} representation and reasoning components. As our approach is logic based we hope that this enhances the overall capabilities of the natural language processing (NLP) system. We present a brief overview of {\sc motel} and the different extensions we are working on, i.e.\ modal extension of description logics, a cardinality-based approach to quantitative information, reason maintenance, probablistic, non-monotonic, and abductive reasoning.

Available: BibTeX-Entry

MOTEL is a logic-based knowledge representation languages of the KL-ONE family. It contains as a kernel the KRIS language which is a decidable sublanguage of first-order predicate logic (see Baader and Hollunder (1990)). Whereas KRIS is a single-agent knowledge representation system, i.e. KRIS is only able to represent general world knowledge or the knowledge of one agent about the world, MOTEL is a multi-agent knowledge representation system. The MOTEL language allows modal contexts and modal concept forming operators which allow to represent and reason about the believes and wishes of multiple agents. Furthermore it is possible to represent defaults and stereotypes. Beside the basic resoning facilities for consistency checking, classification, and realization, MOTEL provides an abductive inference mechanism. Furthermore it is able to give explanations for its inferences.

Available: (gzipped) PS BibTeX-Entry

We propose a translation approach from modal logics to first-order predicate logic which combines advantages from both, the (standard) relational translation and the (rather compact) functional translation method and avoids many of their respective disadvantages (exponential growth versus equality handling). In particular in the application to serial modal logics it allows considerable simplifications such that often even a simple unit clause suffices in order to express the accessibility relation properties. Although we restrict the approach here to first-order modal logic theorem proving it has been shown to be of wider interest, as e.g.\ sorted logic or terminological logic.

Available: DVI BibTeX-Entry

Many attempts have been started to combine logic programming and modal logics. Most of them however, do not use classical PROLOG, but extend the PROLOG idea in order to cope with modal logic formulae directly. These approaches have the disadvantage that for each logic new logic programming systems are to be developed and the knowledge and experience gathered from PROLOG can hardly be utilized. Modal logics based on Kripke-style relational semantics, however, allow a direct translation from modal logic into first-order predicate logic by a straightforward translation of the given relational semantics. Unfor- tunately such a translation turns out to be rather naive as the size of formulae increases exponentially during the translation. This paper now introduces a translation method which avoids such a rep- resentational overhead. Its basic idea relies on the fact that any binary re- lation can be replaced by equations and inequations which (under certain circumstances) can be eliminated later on by some further transformation. The overall approach thus works essentially for any modal logic having a Kripke-style possible world semantics and first-order describable frame properties. If at all, its application as a pre-processing for PROLOG is limited merely by the possibility of having frame properties which are not Horn or not even first-order describable.

Available: DVI BibTeX-Entry

Standard knowledge representation systems are supposed to be able to represent either common or individual knowledge about the world. In this paper we propose an extension to such knowledge representation systems which, in a uniform manner, allows to express beliefs of multiple agents as well as knowledge, desire, time and in fact any modality which has a first-order predicate logic possible world semantics.

Available: DVI BibTeX-Entry

A short introduction to term rewriting systems. This chapter is supposed to provide beginners in logic with the basics of term rewriting, the Knuth-Bendix completion algorithm and theorem proving by rewriting.

Available: BibTeX-Entry

In German

A short introduction to term rewriting systems. This chapter is supposed to provide beginners in logic with the basic ideas behind term rewriting systems, Knuth-Bendix-Completion, and theory proving based on rewriting.

Available: BibTeX-Entry

In German

A short introduction to modal and temporal logic. This chapter is supposed to provide beginners with the basic notions of modal and temporal logics, their syntax and semantics, frame topology and correspondence theory.

Available: BibTeX-Entry