International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'05)

FORMATS 2005 takes place at The ┼ngstr÷m Laboratory in room Polhem. The registration desk will be located just outside the room.

September 26

10.30-11.30Registration open
Paul Pettersson and Wang Yi
13.00-14.00Invited Talk, session chair: Wang Yi
Lothar Thiele: Modular Performance Analysis of Distributed Embedded Systems
14.00-15.30Session I: Logic and Specification, session chair: Eugene Asarin
Real-time Temporal Logic: Past, Present, Future
Oded Maler, Dejan Nickovic, Amir Pnueli
Translating Timed I/O Automata Specifications for Theorem Proving in PVS
Hongping Lim, Dilsun Kaynar, Nancy Lynch, Sayan Mitra
Specification and Refinement of Soft Real-time Requirements Using Sequence Diagrams
Atle Refsdal, Knut Husa, Ketil St°len
16.00-17.30Session II: Timed Games and Synthesis, session chair: Patricia Bouyer
On Optimal Timed Strategies
Thomas Brihaye, VÚronique BruyŔre, Jean-Franšois Raskin
Average Reward Timed Games
Bo Adler, Luca de Alfaro, Marco Faella
Beyond Liveness - Efficient Parameter Synthesis for Time Bounded Liveness
Gerd Behrmann, Kim Larsen, Jacob Rasmussen
18.00-Reception at MIC, room 1446

September 27

09.00-10.00Invited Talk, session chair: Oded Maler
Parosh Abdulla: Verification of Parameterised Timed Systems
10.30-12.00Session III: Model Checking, session chair: Paul Pettersson
Model Checking the Time to Reach Agreement
Martijn Hendriks
Diagonal Constraints in Timed Automata - Forward Analysis of Timed Systems
Patricia Bouyer, Franšois Laroussinie, Pierre-Alain Reynier
A New Verification Procedure for Partially Clairvoyant Scheduling
K. Subramani, D. Desovski
13.30-14.30Invited Talk, session chair: Kim G. Larsen
Karl-Erik ┼rzÚn: Timing Analysis and Simulation Tools for Real-Time Control
14.30-16.00Session IV: Hybrid Systems, session chair: Franck Cassez
Automatic Rectangular Refinement of Affine Hybrid Systems
Laurent Doyen, Thomas Henzinger, Jean-Franšois Raskin
Reachability Problems on Extended o-minimal Hybrid Automata
Raffaella Gentilini
Counterexamples for Timed Probabilistic Reachability
Husain Aljazzar, Holger Hermanns, Stefan Leue
16.30-17.30Session V: Petri Nets, session chair: Walter Vogler
Time Supervision of Concurrent Systems using Symbolic Unfoldings of Time Petri Nets
Thomas Chatain, Claude Jard
Comparison of the Expressiveness of Timed Automata and Time Petri Nets
Beatrice Berard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux
19.00-...FORMATS 2005 Dinner at Vńrmlands Nation

September 28

09.00-10.00Session VI: Semantics and Modelling, session chair: Jean-Francois Raskin
Implementation of Timed Automata: An Issue of Semantics or Modeling?
Karine Altisen, Stavros Tripakis
Timed Abstract Non-Interference
Roberto Giacobazzi, Isabella Mastroeni
10.30-12.00Session VII: Semantics, session chair: Stavros Tripakis
Quantifying Similarities Between Timed Systems
Thomas Henzinger, Rupak Majumdar, Vinayak Prabhu
Performance of Pipelined Asynchronous Systems
Flavio Corradini, Walter Vogler
Is Timed Branching Bisimilarity an Equivalence Indeed?
Wan Fokkink, Jun Pang, Anton Wijs
End of FORMATS 2005
16.00Bus leaving from FORMATS to ARTIST2 Summer School
17.00Bus leaving from Arlanda Airport (terminal 5 at the charter bus stop) to ARTIST2 Summer School