Methods for Modalities 1
Institute for Logic, Language and Computation, University of Amsterdam, May 6-7, 1999
Invited Talks
Thursday, November 29, 09:30-10:45
Wolfgang Thomas, Model-Checking of Infinite State Systems

In this survey talk, we start by recalling the basic notions and constructions of the methodology of model-checking. A key point for the huge success of model-checking procedures in practice is the idea of symbolic computation, where one does not manipulate single states (elements of transition systems) but rather handles appropriate descriptions of sets of states. In "symbolic model-checking", ordered binary decision diagrams (OBDD's) serve as such descriptions.

In the second part of the talk we discuss how the method of model-checking can be generalized by referring to more general diagrams than OBDD's, namely ordinary finite automata. Here one considers infinite systems where states are represented by finite words of arbitrary length, where state properties are captured by regular sets of words, and where transition relations are described by word rewriting systems or transducers. The rich landscape of rewriting systems and transducers yields many types of infinite transition systems. We explain some basic types of infinite systems (given by prefix-recognizable, synchronized rational, and rational transition graphs) and outline known results on model-checking problems (reachability problems, model-checking of first-order and certain CTL*-properties).

(Copies of slides and a list of references will be distributed before the lecture.)

Thursday, November 29, 17:15-18:30
Joe Halpern, Causes and Explanations: A Structural-Model Approach

We propose new definitions of actual cause (causal) explanation, using structural equations to model counterfactuals. We show that these definitions yield a plausible and elegant account of causation and explanation that handles well examples which have caused problems for other definitions and resolves major difficulties in the traditional account. This is joint work with Judea Pearl.

Friday, November 30, 09:00-10:15
Marta Cialdea Mayer, Quantified Modal Logics and Tableau Methods

Quantification in modal logics can be given different semantical characterizations in the Kripke's style. The main differences concern the domains associated to each possible world, that can be either constant, or monotonically increasing or freely varying, and the designation of terms, that can either be required to be the same in each possible world (rigid designation) or not (non-rigid designation). The quantified modal logics (QMLs) considered in the talk belong to such a three-dimensional space of logics: each QML depends on its propositional kernel, the requirements on the object domains and the treatment of functional symbols.

Some QMLs are easy to be captured proof-theoretically, others are not always allowed a simple treatement. The talk introduces the main approaches to proof systems for QMLs, paying a particular attention to tableau methods. In particular, the talk presents a recent proposal unified treatment of QMLs with a propositional "analytical" basis (i.e. one of the systems K, D, T, K4, S4), by means of free variable tableaux.

Friday, November 30, 13:00-14:150
Ed Brinksma, Verification in Practice

In this talk we will give an overview of the evolution of the ideas behind software verification, and their application in practice. Interpreting the more recent developments in computer-aided verification we will argue that realistic software verification cannot be understood as a purely mathematical activity, as it must include empirical elements. Discussing a recent application case study we will identify areas where modal logics have a role to play, and point out some current developments.

Friday, November 30, 16:45-18:00
Enrico Franconi, (Description) Logics for Information Modelling and Access"

In this talk I'll describe how description logics are being used in information systems for the conceptual modelling and query management tasks. The emphasis will be in explaining why a proper logic is needed in those applications, and how these needs have an impact on the research in the modal and description logic communities. I will quickly survey the theoretical foundations of the tasks in a logical context. At the end, a demo of a real conceptual modelling tool driven by a description logics based inference engine will be given.

Methods for Modalities
Contact address

Henry Chinaski Productions 1999