 | |
All
sessions take place in auditorium 1.Chair:
Franz Baader | 09:00- | 10:00
| Maurizio Lenzerini, U Rome I (La Sapienza), Italy
Invited
tutorial: Description logics: Foundations for class-based knowledge
representation |
| 10:00- | 10:30
| Martin Otto, U Wales Swansea, UK
Modal
and guarded characterisation theorems over finite transition
systems
Characterisation
theorems for modal and guarded fragments of
first-order logic are explored over finite transition systems. We show that
the classical characterisations in terms of semantic invariance under the
appropriate forms of bisimulation equivalence can be recovered at the level
of finite model theory. The new, more constructive proofs naturally extend
to alternative proofs of the classical variants. A finite model theory
version of van Benthem's characterisation theorem for basic modal logic,
which similarly sheds new light on the classical version, is due to
E.Rosen. That proof is simplified and the result slightly strengthened in
terms of quantitative bounds with the new approach presented here. The main
thrust of the present paper, however, lies in a uniform treatment that
extends to incorporate universal and inverse modalities and guarded
quantification over transition systems (width two relational structures).
Apart from first-order locality (specific ramifications of Gaifman's
theorem for bisimulation invariant formulae) our treatment rests on a
natural construction of finite, locally acyclic covers for finite
transition systems. These covers can serve as finite analogues of tree
unravellings in providing local control over first-order logic in finite
bisimilar companion structures. |
Chair:
Doron Peled | 11:00- | 11:30
| François Laroussinie, ENS Cachan, France
Nicolas
Markey, ENS Cachan, France
Philippe
Schnoebelen, ENS Cachan, France
Temporal
logic with forgettable past
We
investigate NLTL, a linear-time temporal logic with
forgettable past. NLTL can be exponentially more succinct than LTL+Past
(which in turn can be more succinct than LTL). We study satisfiability and
model checking for NLTL and provide optimal automata-theoretic algorithms
for these EXPSPACE-complete problems. |
| 11:30- | 12:00
| Ian Hodkinson, Imperial College, UK
Frank
Wolter, U Leipzig, Germany
Michael
Zakharyaschev, King's College London, UK
Decidable
and undecidable fragments of first-order branching
temporal logics
In
this paper we analyze the decision problem for fragments of
first-order extensions of branching time temporal logics such as
computational tree logics CTL and CTL* or Prior's Ockhamist logic of
historical nnecessity. On the one hand, we show that the one-variable
fragments of logics like first-order CTL* - such as the product of
propositional CTL* with simple propositional modal logic S5, or even the
one-variable bundled first-order temporal logic with sole temporal operator
`some time in the future' - are undecidable. On the other hand, it is
proved that by restricting applications of first-order quantifiers to state
(i.e., path-independent) formulas, and applications of temporal operators
and path quantifiers to formulas with at most one free variable, we can
obtain decidable fragments. The same arguments show decidability of
`non-local' propositional CTL*, in which truth values of propositional
atoms depend on the history as well as the current time. The positive
decidability results can serve as a unifying framework for devising
expressive and effective time-dependent knowledge representation
formalisms, e.g., temporal description or spatio-temporal
logics. |
| 12:00- | 12:30
| Stephan Kreutzer, Aachen U of Techn., Germany
Expressive
equivalence of least and inflationary fixed-point
logic
We
study the relationship between least and inflationary
fixed-point logic. By results of Gurevich and Shelah from 1986, it has been
known that on finite structures both logics have the same expressive power.
On infinite structures however, the question whether there is a formula in
IFP not equivalent to any LFP-formula was still open. In this paper, we
settle the question by showing that both logics are equally expressive on
arbitrary structures. The proof will also establish the strictness of the
nesting-depth hierarchy for IFP on some infinite structures. Finally, we
show that the alternation hierarchy for IFP collapses to the first level on
all structures, i.e. the complement of an inflationary fixed-point is an
inflationary fixed-point itself. |
Chair:
Thomas Streicher | 14:00- | 14:30
| Josée Desharnais, Laval U, Canada
Vineet
Gupta, Stratify Inc., USA
Radha
Jagadeesan, Loyola U Chicago, USA
Prakash
Panangaden, McGill U, Canada
The
metric analogue of weak bisimulation for probabilistic
processes
We
observe that equivalence is not a robust concept in the
presence of numerical information - such as probabilities - in the model.
We develop a metric analogue of weak bisimulation in the spirit of our
earlier work on metric analogues for strong bisimulation. We give a fixed
point characterization of the metric. This makes available coinductive
reasoning principles and allows us to prove metric analogues of the usual
algebraic laws for process combinators. We also show that quantitative
properties of interest are continuous with respect to the metric, which
says that if two processes are close in the metric then observable
quantitative properties of interest are indeed close. As an important
example of this we show that nearby processes have nearby channel
capacities - a quantitative measure of their propensity to leak
information. |
| 14:30- | 15:00
| Daniel Hirschkoff, ENS Lyon,
France
Etienne
Lozes, ENS Lyon, France
Davide
Sangiorgi, INRIA Sophia-Antipolis, France
Separability,
expressiveness, and decidability in the ambient
logic
The
Ambient Logic (AL) has been proposed for expressing
properties of process mobility in the calculus of Mobile Ambients (MA), and
as a basis for query languages on semistructured data. We study some basic
questions concerning the descriptive and discriminating power of AL,
focusing on the equivalence on processes induced by the logic (=L). We
consider MA, and two Turing complete subsets of it, MA1 and MA2,
respectively defined by imposing a semantic and a syntactic constraint on
process prefixes. The main contributions include: coinductive and inductive
operational characterisations of =L; an axiomatisation of =L on MA2; the
construction of characteristic formulas for the processes in MA1 with
respect to =L; the decidability of =L on MA1 and on MA2, and its
undecidability on MA. |
| 15:00- | 15:30
| Mikkel Nygaard, U Aarhus, Denmark
Glynn
Winskel, U Cambridge, UK
Linearity
in process languages
The
meaning and mathematical consequences of linearity (managing
without a presumed ability to copy) are studied for a path-based model of
processes which is also a model of affine-linear logic. This connection
yields an affine-linear language for processes, automatically respecting
open-map bisimulation, in which a range of process operations can be
expressed. An operational semantics is provided for the tensor fragment of
the language. Different ways to make assemblies of processes lead to
different choices of exponential, some of which respect
bisimulation. |
Chair:
Robert Nieuwenhuis | 16:00- | 16:30
| Ashish Tiwari, SRI International, USA
Deciding
confluence of certain term rewriting systems in polynomial
time
We
present a polynomial time algorithm for deciding confluence of
ground term rewrite systems. We generalize the decision procedure to get a
polynomial time algorithm, assuming that the maximum arity of a symbol in
the signature is a constant, for deciding confluence of rewrite systems
where each rule contains a shallow linear term on one side and a ground
term on the other. The existence of a polynomial time algorithm for
deciding confluence of ground rewrite systems was open for a long time and
was independently solved only recently by Comon, Godoy, and Nieuwenhuis
[FoCS 2001]. Our decision procedure is based on the concepts of abstract
congruence closure and abstract rewrite closure, which have been described
by Bachmair and Tiwari [CADE 2000] and Tiwari [FSTTCS 2001],
respectively. |
| 16:30- | 16:40
| Henrik Björklund, Uppsala U, Sweden
Sergei
Vorobyov, Uppsala U, Sweden
Short
presentation: Two adversary lower bounds for parity games |
| 16:40- | 16:50
| Emmanuel Beffara, ENS Lyon, France
Sergei
Vorobyov, Uppsala U, Sweden
Short
presentation: Is randomized Gurvich-Karzanov-Khachiyan's algorithm for
parity
games polynomial? |
| 16:50- | 17:00
| Emanuele Covino, U Bari, Italy
Giovanni
Pani, U Bari, Italy
Short
presentation: Time-space computational complexity of imperative programming
languages |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
