Workshop on Fixpoints and First-Order Temporal
For a number of years, propositional linear and branching-time
temporal logics have been applied in areas such as formal methods,
theoretical computer science and artificial intelligence. A variety of
logics and sophisticated methods for reasoning with these logics have
been developed, and in many cases applied to real-world problems, such
as specification and verification of reactive systems, the development
of temporal query languages and implementation via executable logics.
With the advent of more complex applications, more expressive logics
are increasingly required, such as first-order temporal logics and
fixpoint temporal logics. Thus, there is considerable interest in
these logics concerning their computational properties, reasoning
methods, and their use in applications. In addition, results obtained
often penetrate other areas of computer science. For example, work on
fixpoint temporal logics has strong connections with logical semantics
of programming languages, while work on first-order temporal logics is
closely related to knowledge representation and reasoning.
This informal workshop aims to create a stimulating setting to bring
together researchers within the UK
interested in fixpoint or first-order temporal
logics to exchange recent results and ideas. Suggested topics include
(but are not restricted to) foundations, efficient proof methods
(game-theoretic, automata-theoretic, tableau, resolution-based etc),
and applications. It will also provide an important opportunity for
researchers working in related areas to gain an overview of the current
state of the art in the field.
This Workshop on Fixpoint and First-Order Temporal Logic is being
organised by the
Logic and Computation group of the
University of Liverpool
and will be held on 13th September 2001. The workshop will be a one day event
and will take place at the University of Liverpool.