- 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
- 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
- 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.