6. FORMATS 2008: Saint Malo, France

Invited Talks

• Joël Ouaknine, James Worrell:
  Some Recent Results in Metric Temporal Logic. 1-13
  
• Albert Benveniste:
  Composing Web Services in an Open World: Issues of Quality of Service. 14
  
• Jirí Srba:
  Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets. 15-32
  

Extensions of Timed Automata and Semantics

• Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Jirí Srba:
  Infinite Runs in Weighted Timed Automata with Energy Constraints. 33-47
  
• Marcin Jurdzinski, Ashutosh Trivedi:
  Concavely-Priced Timed Automata. 48-62
  
• Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski:
  Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets. 63-77
  
• P. Vijay Suman, Paritosh K. Pandya, Shankara Narayanan Krishna, Lakshmi Manasa:
  Timed Automata with Integer Resets: Language Inclusion and Expressiveness. 78-92
  

Timed Games and Logic

• Alexander Rabinovich:
  Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities. 93-108
  
• Carlo A. Furia, Matteo Rossi:
  MTL with Bounded Variability: Decidability and Complexity. 109-123
  
• Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu:
  Timed Parity Games: Complexity and Robustness. 124-140
  
• Aldric Degorre, Oded Maler:
  On Scheduling Policies for Streams of Structured Jobs. 141-154
  

Case Studies

• Frédéric Boniol, Pierre-Emmanuel Hladik, Claire Pagetti, Frédéric Aspro, Victor Jégu:
  A Framework for Distributing Real-Time Functions. 155-169
  
• Georgeta Igna, Venkatesh Kannan, Yang Yang, Twan Basten, Marc Geilen, Frits W. Vaandrager, Marc Voorhoeve, Sebastian de Smet, Lou J. Somers:
  Formal Modeling and Scheduling of Datapaths of Digital Document Printers. 170-187
  

Model-Checking of Probabilistic Systems

• Anne Remke, Boudewijn R. Haverkort:
  A Uniformization-Based Algorithm for Model Checking the CSL Until Operator on Labeled Queueing Networks. 188-202
  
• Joost-Pieter Katoen, Alexandru Mereacre:
  Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains. 203-217
  

Verification and Test

• K. Mani Chandy, Sayan Mitra, Concetta Pilotto:
  Convergence Verification: From Shared Memory to Partially Synchronous Systems. 218-232
  
• Jasper Berendsen, Frits W. Vaandrager:
  Compositional Abstraction in Real-Time Model Checking. 233-249
  
• Julien Schmaltz, Jan Tretmans:
  On Conformance Testing for Timed Systems. 250-264
  

Time Petri Nets

• Hanifa Boucheneb, Kamel Barkaoui:
  Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs. 265-279
  
• Louis-Marie Traonouez, Didier Lime, Olivier H. Roux:
  Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph. 280-294