Workshops:		EXPRESS'02 PDMC'02
18:00 - 19:00		Welcome Gathering

8:50 - 9:00		Opening of the Conference
9:00 - 10:00		Invited Talk (Chair: M. Vardi) Amir Pnueli: A Deductive Proof System for CTL*
10:00 - 10:30		Break
		Verification, Model Checking I (Chair: P. Jancar)
10:30 - 11:00		Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore Zuck: Network Invariants in Action
11:00 - 11:30		Parosh A. Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso: Regular Model Checking Made Simple and Efficient
11:30 - 12:00		Kousha Etessami: A Hierarchy of Polynomial-Time Computable Simulations for Automata
12:00 - 12:30		P. Madhusudan and P.S. Thiagarajan: A Decidable Class of Asynchronous Distributed Controllers
12:30 - 14:00		Lunch
14:00 - 15:00		Invited Talk (Chair: A. Kucera) Wan Fokkink: Refinement and Verification Applied to an In-Flight Data Acquisition Unit
15:00 - 15:20		Break
		Verification, Model Checking II (Chair: U. Nestmann)
15:20 - 15:50		Antti Valmari and Antti Kervinen: Alphabet-Based Synchronisation is Exponentially Cheaper
15:50 - 16:20		Markus Lohrey: Safe Realizability of High-Level Message Sequence Charts
16:20 - 16:50		Eugene Asarin and Gerardo Schneider: Widening the Boundary Between Decidable and Undecidable Hybrid Systems
16:50 - 17:00		Break
17:00 - 18:30		Tutorial (Chair: M. Kretinsky) Julian Bradfield: Introduction to Modal and Temporal Mu-Calculi

9:00 - 10:00		Invited Talk (Chair: K.G. Larsen) Alexander Rabinovich: Expressive Power of Temporal Logics
10:00 - 10:30		Break
		Logic (Chair: I. Walukiewicz)
10:30 - 11:00		Luis Caires and Luca Cardelli: A Spatial Logic for Concurrency (Part II)
11:00 - 11:30		B. Konikowska and W. Penczek: Reducing Model Checking from Multi-Valued CTL* to CTL*
11:30 - 12:00		Martin Lange: Local Model Checking Games for Fixed Point Logic with Chop
12:00 - 12:30		Maria Sorea: A Decidable Fixpoint Logic for Time-Outs
12:30 - 13:45		Lunch
13:45 - 19:00		Trip

9:00 - 10:00		Invited Talk (Chair: C. Palamidessi) Davide Sangiorgi: Types, or: Where's the Difference Between CCS and Pi?
10:00 - 10:30		Break
		Mobility (Chair: R. Amadio)
10:30 - 11:00		Jens Chr. Godskesen, Thomas Hildebrandt, and Vladimiro Sassone: A Calculus of Mobile Resources
11:00 - 11:30		David Teller, Pascal Zimmer, and Daniel Hirschkoff: Using Ambients to Control Resources
11:30 - 12:00		Massimo Merro and Vladimiro Sassone: Typing and Subtyping Mobility in Boxed Ambients
12:00 - 12:30		Roberto Bruni, Cosimo Laneve, and Ugo Montanari: Orchestrating Transactions in Join Calculus
12:30 - 14:00		Lunch
		Probabilistic Systems (Chair: E. Best)
14:00 - 14:30		Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn Haverkort: Simulation for Continuous-Time Markov Chains
14:30 - 15:00		Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden: Weak Bisimulation is Sound and Complete for PCTL*
15:00 - 15:30		Stefano Cattani and Roberto Segala: Decision Algorithms for Probabilistic Bisimulation
15:30 - 15:50		Break
		Models of Computation, Process Algebra I (Chair: P. Schnoebelen)
15:50 - 16:20		Gerald Luettgen and Michael Mendler: Axiomatizing an Algebra of Step Reactions for Synchronous Languages
16:20 - 16:50		Jean Fanchon and Remi Morin: Regular Sets of Pomsets with Autoconcurrency
16:50 - 17:00		Break
17:00 - 18:30		Tutorial (Chair: M. Kretinsky) Andrew Gordon: Types for Cryptographic Protocols
19:15		Departure for Conference Dinner

9:00 - 10:00		Invited Talk (Chair: P. Panangaden) Vaughan Pratt: Event-State Duality: The Enriched Case
10:00 - 10:30		Break
		Models of Computation, Process Algebra II (Chair: J. Bradfield)
10:30 - 11:00		Philippa Gardner, Cosimo Laneve, and Lucian Wischik: The Fusion Machine
11:00 - 11:30		Mikkel Nygaard and Glynn Winskel: HOPLA - A Higher-Order Process Language
11:30 - 12:00		Marzia Buscemi and Ugo Montanari: A First Order Coalgebraic Model of Pi-Calculus Early Observational Equivalence
12:00 - 12:30		Stephen Brookes: Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes
12:30 - 14:00		Lunch
		Security (Chair: A. Gordon)
14:00 - 14:30		Michele Boreale and Marzia Buscemi: A Framework for the Analysis of Security Protocols
14:30 - 15:00		Roberto Amadio and Witold Charatonik: On Name Generation and Set-Based Analysis in the Dolev-Yao Model
15:00 - 15:30		Ralf Kuesters: On the Decidability of Cryptographic Protocols with Open-Ended Data Structures
15:30 - 15:50		Break
		Petri Nets (Chair: P.S. Thiagarajan)
15:50 - 16:20		H.C.M. Kleijn and M. Koutny: Causality Semantics of Petri Nets with Weighted Inhibitor Arcs
16:20 - 16:50		Hagen Völzer: Refinement-Robust Fairness
16:50 - 17:10		Break
		Bisimulation (Chair: C. Stirling)
17:10 - 17:40		Slawomir Lasota: Decidability of Strong Bisimilarity for Timed BPP
17:40 - 18:10		Jiri Srba: Undecidability of Weak Bisimilarity for Pushdown Processes
18:10 - 18:40		Antonin Kucera and Richard Mayr: Why is Simulation Harder Than Bisimulation?
		End of the Conference

Workshops:

CMCIM'02 FATES'02 FOCLASA'02 INFINITY'02 MTCS'02 Tools Day