Main conference
Workshops
A Deductive Proof System for CTL* Amir Pnueli  Weizmann Institute of Science (Israel)
The paper presents a sound and (relatively) complete deductive proof
system for the verification of CTL* properties over possibly
infinitestate reactive systems. The proof system is based on a set of
proof rules for the verification of basic CTL* formulas, namely
CTL* formulas with no embedded path quantifiers. We first present proof
rules for some of the most useful basic CTL* formulas, then present a
methodology for transforming an arbitrary basic formula into one of
these special cases. Finally, we present a rule for decomposing the
proof of a general (nonbasic) CTL* formula into proofs of basic CTL*
formulas. EventState Duality: The Enriched Case Vaughan Pratt  Stanford University (USA)
Enriched categories have been applied in the past to both eventoriented
true concurrency models and stateoriented information systems, with no
evident relationship between the two. Ordinary Chu spaces expose a
natural duality between partially ordered temporal spaces (pomsets,
event structures), and partially ordered information systems. Barr and
Chu's original definition of Chu spaces however was for the general
Venriched case, with ordinary Chu spaces arising for V = Set
(equivalently V = Poset at least for biextensional Chu spaces). We
extend timeinformation duality to the general enriched case, and apply
it to put on a common footing event structures, higherdimensional
automata (HDAs), a cancellationbased approach to branching time, and
other models treatable by enriching either event (temporal) space or
state (information) space. Refinement and Verification Applied to an InFlight Data Acquisition Unit Wan Fokkink  CWI (The Netherlands) Joint work with: Natalia Ioustinova, Ernst Kesseler, Jaco van de Pol, Yaroslav Usenko, and Yuri Yushtein
In order to optimise maintenance and increase security, The Royal
Netherlands Navy initiated the development of a multichannel onboard
dataacquisition system for its Lynx helicopters. This AIDA (Automatic
Inflight Data Acquisition) system records usage and loads data on main
rotor, engines and airframe. We used refinement in combination with
model checking to arrive at a formally verified implementation of the
AIDA system, starting from the functional requirements. Expressive Power of Temporal Logics Alexander Rabinovich  Tel Aviv University (Israel)
The objectives of this paper is to survey classical and recent
expressive completeness results and to provide some external yardsticks
by which the expressive power of temporal logics can be
measured. Types, or: Where's the Difference Between CCS and Pi? Davide Sangiorgi  INRIA (France)
The picalculus is the paradigmatic calculus of mobile processes. With
respect to previous formalisms for concurrency, most notably CCS, the
most novel aspect of picalculus is probably its rich theory of types.
We explain the importance of types in the picalculus on a concrete
example: the termination property.
A process M terminates if it cannot produce an infinite sequence of
reductions M > M_{1} > M_{2} ... Termination is
a useful property in concurrency. For instance, a terminating applet,
when loaded on a machine, will not run for ever, possibly absorbing all
computing resources (a `denial of service' attack). Similarly,
termination guarantees that queries to a given service originate only
finite computations.
We consider the problem of proving termination of nontrivial subsets of
CCS and picalculus. In CCS the proof is purely combinatorial, and is
very simple. In the picalculus, by contrast, combinatorial proofs
appear to be very hard. We show how to solve the problem by taking into
account type information.

concur02@fi.muni.cz 