http://www.dagstuhl.de/10031

17. – 22. Januar 2010, Dagstuhl Seminar 10031

Quantitative Models: Expressiveness and Analysis

Organisatoren

Christel Baier (TU Dresden, DE)
Manfred Droste (Universität Leipzig, DE)
Paul Gastin (ENS – Cachan, FR)
Kim Guldstrand Larsen (Aalborg University, DK)


Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Dagstuhl Seminar Proceedings DROPS
Teilnehmerliste
Gemeinsame Dokumente

Summary

Quantitative models and quantitative analysis in Computer Science are receiving increased attention in order to meet the challenges from application areas such as Performance Analysis, Operational Research and Embedded Systems. What is aimed at is a revision of the foundation of Computer Science where boolean models and analyses are replaced by quantitative models and analyses in order that more detailed and practically useful answers can be provided.

The purpose of this seminar was to bring together researchers from different communities with their central interest in quantitative models and analysis. The goal was to address three fundamental topics which are closely related: quantitative analysis of real-time and hybrid systems; probabilistic analysis and stochastic automata; weighted automata. These three areas of research have mainly evolved independently so far and the relationship between them has emerged only recently. The seminar brought together leading researchers of the three areas, with the goal of future highly productive cross-fertilizations.

The model of timed automata introduced by Alur and Dill in 1989 has by now established itself as a universal formalism for describing real-time systems. The notion of priced (or weighted) timed automata was introduced independently by Alur et al and Larsen et al in 2001, with the surprising result that cost optimal reachability is decidable. Since these initial results, efficient tools have been developed and a number of more challenging questions have been considered including multi-priced timed automata, optimal infinite scheduling (both with respect to mean pay-off and discounting), priced timed games and model checking for priced timed automata.

Stochastic models have a long tradition in Mathematics, starting with the work by Markov in the early 20th century and by Bellman around 1950 who introduced the basic principles of Markov chains and Markov decision processes, respectively. Later, distributed randomized systems were modeled by finite-state automata with discrete transition probabilities, and automata- and graph-based algorithms were developed to determine the probabilities of given linear-time properties. However, the concept of ``dense time'' in most stochastic models is different from that of timed automata. Continuous-time stochastic models support reasoning about time-dependent distributions for the delay of transitions. The seminar discussed methods for the quantitative analysis where the concepts of timed and probabilistic automata have been combined.

In the seminar, 45 researchers from 13 countries discussed their recent research results and developments for quantitative models and their analysis. Four survey lectures and 28 talks were organized in eight sessions with centralized themes. From the beginning, all lectures and talks raised questions of members from the other fields, and lively discussions followed. In particular, the surveys presented the fields of weighted automata, priced timed automata and games, stochastic model checking, and reconciliations between weighted and probabilistic logics. The lectures and talks dealt with, e.g., quantitative modeling formalisms and their semantics, expressiveness of models including quantitative measures for infinite behavior (like discounting, mean payoff, long-run averages), and composition and components of different models, to name only a few topics.

There are a number of open problems concerning the interplay between these fields. For instance, there are many interesting open questions about the combination of real-time and probabilism. Also, weighted automata and probabilistic automata bear similarities but also differences, and one should investigate how known techniques can be transferred in either direction. The interplay between priced timed automata and weighted automata also demands further investigation. Due to these open challenges, several researchers decided to meet again later in the year, e.g. during the workshop in Leipzig on ``Weighted Automata: Theory and Applications (WATA 2010)''.

During the seminar, there was very much interaction between the participants. It was expressed that a future research collaboration between the different present groups should be highly fruitful and would therefore be very desirable. A Dagstuhl seminar would provide an ideal and unique opportunity for this. The successful collaboration in the present seminar was felt to be due in particular to the superb facilities and excellent organization provided by the Dagstuhl center and its team.

Related Dagstuhl Seminar

Classification

  • Modelling/simulation
  • Semantics/formal Methods
  • Verification/logics

Keywords

  • Quantitative models
  • Quantitative analysis
  • Timed and hybrid systems
  • Probabilistic systems
  • Weighted automata

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im 1. Obergeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.