| 8.50-9.00 | Welcome | |
| 9.00-9.30 | Gerwin Klein | Verified Lightweight Bytecode Verification |
| 9.30-10.00 | Barbara Koenig | A Logic for the Static Analysis of Graph Transformation Systems |
| 10.00-10.30 | Coffee break | |
| 10.30-11.00 | Stefan Berghofer | Executing Higher Order Logic Specifications |
| 11.00-12.00 | Jan Rutten, CWI Amsterdam | Elements of Stream Calculus and its Applications (Invited talk) |
| 12.00-14.00 | Lunch | |
| 14.00-14.30 | Franz Baader | A Comparison of Automata and Tableau Methods for Modal Satisfiability |
| 14.30-15.00 | Manfred Droste | Ein Automatenmodell für nebenläufige Prozesse |
| 15.00-15.30 | Jan Johannsen | Higher Type Recursion and Parallel Complexity |
| 15.30-16.00 | Coffee break | |
| 16.00-16.30 | Uwe Egly | An Embedding of Lax Logic into Intuitionistic Logic |
| 16.30-17.00 | Peter H. Schmitt | Iterate Logic |
| 17.00-18.00 | Frank Wolter | Axiomatisierbare und entscheidbare Fragmente Temporaler Praedikatenlogik (Invited talk) |
| 18.15 | Business Meeting (Fachgruppensitzung) |
A joint dinner is planned for the evening.
End of event
(no talks planned for Thursday)
Tableaux-based decision procedures for satisfiability of modal and description logics behave quite well in practice, but it is sometimes hard to obtain exact worst-case complexity results using these approaches, especially for EXPTIME-complete logics. In contrast, automata-based approaches often yield algorithms for which optimal worst-case complexity can easily be proved. However, the algorithms obtained this way are usually not only worst-case, but also best-case exponential: they first construct an automaton that is always exponential in the size of the input, and then apply the (polynomial) emptiness test to this large automaton. To overcome this problem, one must try to construct the automaton ``on-the-fly'' while performing the emptiness test. In this talk we will show that Voronkov's inverse method for the modal logic K can be seen as an on-the-fly realization of the emptiness test done by the automata approach for K. The benefits of this result are two-fold. First, it shows that Voronkov's implementation of the inverse method, which behaves quite well in practice, is an optimized on-the-fly implementation of the automata-based satisfiability procedure for K. Second, it can be used to give a simpler proof of the fact that Voronkov's optimizations do not destroy completeness of the procedure. We will also show that the inverse method can easily be extended to handle global axioms, and that the correspondence to the automata approach still holds in this setting. In particular, the inverse method yields an EXPTIME-algorithm for satisfiability in K w.r.t. global axioms.
Stefan Berghofer, TU München: Execting Higher Order Logic Specifications
Executing formal specifications has been a popular research topic for some decades, covering every known specification formalism. Executability is essential for validating complex specifications by runnig test cases and for generating code automatically ("rapid prototyping"). In the theorem proving community executability is no less of an issue. Two prominent examples are the Boyer-Moore system (and its successor ACL2) and constructive type theory, both of which contain a functional programming language.
We report on the design of a prototyping component for the theorem prover Isabelle/HOL. We give a precise definition of an executable subset of HOL and describe its compilation into a functional programming language. The executable subset contains datatypes and recursive functions as well as inductive relations. Inductive relations must be such that they can be executed in Prolog style but requiring only matching rather than unification. This restriction is enforced by a mode analysis. Datatypes and recursive functions compile directly into their programming language equivalents, and inductive relations are translated into functional programs using mode information and standard programming techniques for lazy lists.
Our aim has not been to reach or extend the limits of functional-logic programming but to design a lightweight and efficient execution mechanism for HOL specifications that requires only a functional programming language and is sufficient for typical applications like execution of programming language semantics or abstract machines.
Uwe Egly, TU Wien: An embedding of Lax logic into intuitionistic logic
Lax logic (LL) is obtained from intuitionistic logic (IL) by adding a single modality $\circ$\/ (lax modality) which captures properties of necessity and possibility. This modality was considered by Curry in two papers from 1952 and 1957 and rediscovered recently in different contexts like verification of circuits and the computational $\lambda$ calculus. We show that lax logic can be faithfully embeded into the nderlying intuitionistic logic and discuss (computational) properties of the embedding. A consequence of faithfulness of our embedding is that the lax modality is redundant.
Manfred Droste, TU Dresden: Ein Automatenmodell für nebenläufige Prozesse
Bei automatischen Verifikationsverfahren der Spezifikation nebenläufiger Systeme treten häufig riesige Zustandsräume auf, das bekannte "state space explosion problem". Verschiedene Autoren haben gezeigt, dass sich die Verifikationsverfahren durch das Aufspüren und Ausnutzen von Unabhängigkeiten zwischen den Transitionen nebenläufiger Programme wesentlich verbessern lassen. Wir werden ein Automatenmodell für derartige Situationen vorstellen. Wir zeigen, wie endliche oder unendliche nebenläufige Berechnungen durch teilweise Ordnungen dargestellt und wie verschiedene Logiken (Prädikatenlogik, temporale Logik) zur Spezifikation dieser Ordnungen und damit der Berechnungen verwandt werden können. Hierbei ergeben sich Zusammenhänge zur Theorie erkennbarer, aperiodischer oder sternfreier Sprachen. Dies verallgemeinert klassische Sätze von Kleene, Büchi, McNaughton und Papert sowie kürzliche Resultate aus der Spur-Theorie.
Jan Johannsen, LMU München: Higher Type Recursion and Parallel Complexity (with Klaus Aehlig, Helmut Schwichtenberg, Sebastiaan Terwijn)
A typed lambda calculus with recursion in all finite types is defined such that the first order terms exactly characterize the parallel complexity class NC. This is achieved by use of the appropriate forms of recursion (concatenation recursion and logarithmic recursion), a ramified type structure and imposing of a linearity constraint.
Gerwin Klein, TU München: Verified Lightweigt Bytecode Verification
Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one-pass verification of welltypedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness.
Barbara Koenig, TU München: A Logic for the Static Analysis of Graph Transformation Systems
An analysis technique for graph transformation systems is presented. We introduce an algorithm which, given a graph transformation system and a start graph, produces a finite structure consisting of a hypergraph decorated with transitions (Petri graph) which can be seen as an approximation of the unfolding of the graph transformation system.
Some formulas of second-order logic on graphs enjoy the property that their validity on the approximation implies their validity for all reachable graphs. We introduce a syntactic characterization of such properties. This classification can also be extended to formulas of temporal logics.
Jan Rutten, Centre for Mathematics and Computer Science (CWI) Amsterdam: Elements of Stream Calculus and its Applications (Invited talk)
As an extensive exercise in the use of coinductive techniques,
the set of all streams (here: infinite sequences of real numbers)
is turned into a calculus in two ways:
the operation of `tail' of a stream is taken as a formal
notion of stream derivative:
(s_0, s_1, s_2, ...) ' = (s_1, s_2, s_3, ...)
a set of operators on streams is defined, including convolution
product, shuffle product, and their inverse, and a number of
algebraic identities (laws) are proved.
In the stream calculus that is thus obtained, it is possible to solve so-called behavioural differential equations (equations for defining streams, formulated in terms of stream derivatives and the operators) in an algebraic fashion. In order to solve equations involving shuffle product, it is crucial to understand the combined occurrences of convolution product (and inverse), on the one hand, and shuffle product (and inverse), on the other hand. The most interesting laws will deal with what we have called `shuffle elimination' (from the shuffle product of rational expressions, for instance). The calculus will be applied to (giving at the same time a unified perspective on):
The present work builds on and extends:
J.J.M.M. Rutten.
Automata, power series, and coinduction: taking input derivatives
seriously (extended abstract).
Report SEN-R9901, CWI, 1999.
Available at URL: www.cwi.nl.
Also in the proceedings of ICALP '99,
LNCS 1644, 1999, pp. 645--654.
J.J.M.M. Rutten.
Behavioural differential equations: a coinductive calculus of
streams, automata, and power series.
Report SEN-R0023, CWI, 2000.
Available at URL: www.cwi.nl.
In addition, the application to analytical differential equations was insprired by and extends:
D. Pavlovi'c and M. Escard'o.
Calculus in coinductive form.
Proceedings of the 13th Annual IEEE Symposium on Logic in
Computer Science, pages 408--417. IEEE Computer Society Press, 1998.
Peter H. Schmitt, Univ. Karlsruhe: Iterate Logic
The topic of this talk evolved within the investigation into a formal semantics of the Unified Modeling Language (UML), in particular its text-based part, the Object Constraint Language (OCL). I will begin by a short review of what needs to been known from this area for the purpose of this talk. OCL looks at first very much like a notational variant of first-order logic. Closer inspection, however, reveals some interesting, non-first-order constructs. Among those figures most prominently the "iterate" construct. I will introduce "Iterate Logic", a new logic on finite structures extending classical first-order logic intended to isolate the principles of the iterate construct and study its logic properties "in vitro". I will present first results comparing "Iterate Logic" with other logics on finite structures.
Frank Wolter, Univ. Leipzig: Axiomatisierbare und entscheidbare Fragmente Temporaler Praedikatenlogik (Invited talk)
Aufgrund der Interaktion zwischen temporalen und first-order Quantoren sind selbst scheinbar schwache Fragmente der Temporalen Praedikatenlogik nicht axiomatisierbar. Interessante axiomatisierbare Fragmente waren bisher nicht bekannt. Im Vortrag werde ich das monodische (nicht monadische!) Fragment der Temporalen Praedikatenlogik einfuehren. Dieses ist noch sehr expressiv aber axiomatisierbar. Schraenkt man den praedikatenlogischen Teil des monodischen Fragments auf ein entscheidbares Fragment der Praedikatenlogik (etwa das monadische Fragment oder das 2-Variablen-Fragment) ein, so wird das monodische Fragment sogar entscheidbar. Anwendungen dieser Resultate fuer Temporale Beschreibungslogiken und Raum-Zeit-Logiken werden diskutiert.