12. Jahrestagung der GI-Fachgruppe Logik in der Informatik München, 19.-20. Mai 2005

Vorträge

Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme.
(This is joint work with Silvio Ghilardi.)

In recent work Baader has shown that a certain description logic with conjunction, existential quantification and with circular definitions has a polynomial time subsumption problem both under an interpretation of circular definitions as greatest fixpoints and under an interpretation as arbitrary fixpoints (introduced by Nebel). This was shown by translating definitions in the description logic (``TBoxes'') into a labelled transition system and by reducing subsumption to a question of the existence of certain simulations. In the case of subsumption under the descriptive semantics a new kind of simulation, called synchronised simulation, had to be introduced. In this paper, we also give polynomial-time decision procedures for these logics; this time by devising sound and complete proof systems for them and demonstrating that proof search is polynomial for these systems. We then use the proof-theoretic method to study the hitherto unknown complexity of description logic with universal quantification, conjunction, and GCI axioms. Finally, we extend the proof-theoretic method to negation and thus obtain a decision procedure for the description logic ALC with fixpoints. This last section is only sketched.

The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demonstrated by Christodorescu and Jha, however, classical detection software relies on static patterns, and is easily outsmarted. In this paper, we present a flexible method to detect malicious code patterns in executables by model checking. While model checking was originally developed to verify the correctness of systems against specifications, we argue that it lends itself equally well to the specification of malicious code patterns. To this end, we introduce the specification language CTPL (Computation Tree Predicate Logic) which extends the well-known logic CTL, and describe an efficient model checking algorithm. Our practical experiments demonstrate that we are able to detect a large number of worm variants with a single specification.

This work presents game-based model checking for abstract models with respect to specifications in $\mu$-calculus, interpreted over a 3-valued semantics. If the model checking result is indefinite (don't know), he abstract model is refined, based on an analysis of the cause for this result. For finite concrete models our abstraction-refinement is fully automatic and guaranteed to terminate with a definite result true or false.

Adding an explicit monad structure to a higher-order de Bruijn representation of lambda terms through nested data types, i. e., heterogeneous families of data types, yields a truly nested data type that is thus no more strictly positive and exceeds the direct expressive power of theorem proving environments such as Coq. On the other hand, full explicit substitution requires a second-order existential quantifier in the categorical data type definition but is strictly positive and hence easier to handle. Both approaches are compared with respect to the definition and reasoning principles they support. We also discuss the extent to which the impredicative variant of the sort Set in Coq is needed.

Non-effective cut elimination proof uses Koenig's lemma to obtain a non-closed branch of a proof-search tree (without cut) for a formula A, if A is not cut-free provable. A partial model (semi-valuation) corresponding to this branch and verifying ~A is extended to a total model for ~A using arithmetical comprehension. This contradicts soundness, if A is derivable with cut. The same argument works for Herbrand Theorem. We discuss algorithms of obtaining cut-free proofs corresponding to this schema and quite different from complete search through all possible proofs.

The advent of XML processing languages raises the question whether there are good logical foundations for XML querying tasks as they are established for the theory of relational databases. The talk gives a couple of examples of the application of logics to the theory of XML query languages and concludes with some recent results on two-variable logics with data comparisons.
Folien

Security protocols employing cryptographic primitives with algebraic properties are conveniently modeled using Horn clauses modulo equational theories. We consider clauses corresponding to the class H3 of Nielson, Nielson and Seidl. We show that modulo the theory ACU of an associative-commutative symbol with unit, as well as its variants like the theory XOR and the theory AG of Abelian groups, unsatisfiability is NP-complete. Also membership and intersection-non-emptiness problems for the closely related class of one-way as well as two-way tree automata modulo these equational theories are NP-complete. A key technical tool is a linear time construction of an existential Presburger formula corresponding to the Parikh image of a context-free language. Our algorithms require deterministic polynomial time using an oracle for existential Presburger formulas, suggesting efficient implementations are possible.