LICS on Thursday

Detailed program
Thursday July 25th, 2002
See also the unified by-slot program

All sessions take place in auditorium 1.

Session 14

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.

Session 15

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.

Session 16

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.

Session 17

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