10.30-11.30 | Registration open |
11.30-12.50 | Lunch |
12.50-13.00 | Opening |
| Paul Pettersson and Wang Yi |
13.00-14.00 | Invited Talk, session chair: Wang Yi |
| Lothar Thiele: Modular Performance Analysis of Distributed Embedded Systems |
14.00-15.30 | Session 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 |
15.30-16.00 | Coffee |
16.00-17.30 | Session 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 |
09.00-10.00 | Invited Talk, session chair: Oded Maler |
| Parosh Abdulla: Verification of Parameterised Timed Systems |
10.00-10.30 | Coffee |
10.30-12.00 | Session 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 |
12.00-13.30 | Lunch |
13.30-14.30 | Invited Talk, session chair: Kim G. Larsen |
| Karl-Erik Årzén: Timing Analysis and Simulation Tools for Real-Time Control |
14.30-16.00 | Session 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.00-16.30 | Coffee |
16.30-17.30 | Session 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 |
09.00-10.00 | Session 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.00-10.30 | Coffee |
10.30-12.00 | Session 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 |
12.00-13.30 | Lunch |
| End of FORMATS 2005 |
16.00 | Bus leaving from FORMATS to ARTIST2 Summer School |
17.00 | Bus leaving from Arlanda Airport (terminal 5 at the charter bus stop) to ARTIST2 Summer School |