Mathematische Logik und Anwendungen


Abstracts Keynote Talks of the Graduiertenkolleg Closing Session

Universitšt Freiburg, 11.-12. September 2008

Victor Vianu (U.C. Dan Diego): Verification of Data-Aware Web Services
Date: September 11, 10.30-11.30am

The talk describes models of Web services and their compositions, and results on their automatic verification. After a brief review of finite-state models of Web services, the talk focuses on infinite-state models and verification results taking into account the presence of data. Web services accessing an underlying database are modeled as transducers whose control is specified in first-order logic. Compositions of Web services are modeled by communicating transducers. The properties to be verified are expressed in an extended LTL where propositions are interpreted as FO formulas. The results establish under what conditions automatic verification of such properties is possible and provide the complexity of verification. This brings into play a mix of techniques from logic and model checking.

Much of the talk is based on joint work with Alin Deutsch, Liying Sui, and Dayou Zhou (UC San Diego).

Michael Huth (Imperial College London): Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis [ Slides Talk (.pdf) ]
Date: September 11, 2.30-3.30pm

It is difficult to develop and maintain large, multi-author access-control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for all desired policy compositions. We present a policy language PBel (pronounced "pebble") whose combinators are based on Belnap logic, a four-valued logic, in which truth values correspond to policy results of "grant", "deny", "conflict", and "undefined". To support policy analysis, we define a query language in which analysis questions for policies written in PBel can be phrased. Queries can be translated into a fragment of first-order logic for which satisfiability and validity checks are computable by SAT solvers or BDDs. We show how policy analysis for PBel can then be carried out through model checking, validity checking, and assume-guarantee reasoning over such translated queries. Sufficient syntactic criteria for gap and conflict freedom of policies written in Pbel are also presented. Finally, we establish expressiveness results, showing that exactly the data-independent policies can be expressed in our language.

Acknowledgments: This is joint work with Glenn Bruns at Alcatel-Lucent.

Thomas Eiter (TU Wien): Answer Set Programming in a Nutshell [ Slides Talk (.pdf) ]
Date: September 12, 12noon-1pm

In the last decade, Answer Set Programming (ASP) has emerged as a powerful paradigm for declarative problem solving, which is rooted in knowledge representation and non-monotonic logic programming. The basic idea is to encode, similar as in SAT solving, solutions to a problem in the models of a non-monotonic logic program, which can be efficiently computed by reasoning engines. By its many language extensions and special features, ASP is particularly well-suited for modeling and solving problems which involve common sense reasoning, and it has been fruitfully applied to a wide range of applications including data integration, configuration, diagnosis, text mining, Semantic Web, and reasoning about actions and change. This talk gives a brief introduction to ASP, covering the basic concepts, some of its properties and features, and addresses current ASP systems and selected applications. It also presents some research issues in ASP, which span from theory to practice and show the fruitful interaction of these aspects.

Alexander Prestel (U Konstanz): Ein Entscheidungsproblem für positive Polynome (in Dimension 2)
Date: September 12, 2.30-3.30pm

Abstract: PDF