Dagstuhl Seminar 14041
Quantitative Models: Expressiveness, Analysis, and New Applications
( Jan 19 – Jan 24, 2014 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/14041
Organizers
- Manfred Droste (Universität Leipzig, DE)
- Paul Gastin (ENS - Cachan, FR)
- Kim Guldstrand Larsen (Aalborg University, DK)
- Axel Legay (INRIA Rennes - Bretagne Atlantique, FR)
Contact
- Susanne Bach-Bernhard (for administrative matters)
Quantitative models and quantitative analysis in Computer Science is receiving increased attention in order to meet the challenges from application areas such as Cyber Physical 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.
In 2010, Dagstuhl Seminar 10031, we brought together researchers from different communities whose central interest is in quantitative models and analysis. In particular our objective was to link those researchers working on so called model checking approaches with those coming from the formal language theory. Our action was motivated by the observation that both communities were pursuing quantitative extensions but using different terminologies and techniques for analyzing such models. The workshop was a success and created various interactions between and beyond the participants from the two areas of quantitative model checking and weighted automata. Since then, the theme of quantitative analysis has expanded to become one of the hottest topic in the formal methods area. A large number of new models, toolsets, and new application domains have emerged since our last workshop. The theory of weighted automata has also developed, introducing extensions of the models which are motivated by the quantitative analysis of systems. It is time for the quantitative model checking and weighted automata communities to meet again with the objective of discussing the latest developments in those areas.
Aside from continuing the interactions initiated during Dagstuhl Seminar 10031, one of the main objectives of this workshop will be to create interaction with researchers working in areas where we do believe that our models and techniques may have potential applications. Particularly, we will invite major players in the following areas (we plan to have one tutorial per day to generate discussions):
- Systems biology, an area where quantitative models have recently been used to represent and analyse biological phenomena. Here the challenge is not only to find mathematical models for such phenomena, but also to define new efficient quantitative analysis techniques capable of coping with very large size complex systems. Two promising applications are 1) using SMC-based techniques to monitor complex properties that cannot be expressed in classical temporal logic (e.g., oscillation properties), and 2) using interface theories as a formal characterization of phenomena in the area of synthetic biology.
- Smart Building: the challenge of Smart Building is to balance energy consumption with dynamic changes. Quantitative models such as energy automata and analysis are emerging as potential key techniques.
- Energy Grid: the challenge of smart electricity grids is to balance the behavior of all participants (suppliers and consumers) to improve efficiency and stability. Again, quantitative models such as energy automata and analysis are emerging as potential key techniques.
- Multicore Platform: the growing omnipresence of multicore platforms calls for renewed efforts into techniques for mapping application onto the corresponding execution platform with predictable (perhaps even optimal) quantitative behavior (guaranteed fulfillment of deadlines, minimal energy consumption).
Quantitative models and quantitative analysis in Computer Science is receiving increased attention in order to meet the challenges from application areas such as Cyber Physical 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. Recently, a large number of new models, toolsets, and new application domains have emerged. The theory of weighted automata has also developed, introducing extensions of the models which are motivated by the quantitative analysis of systems.
The first objective of the seminar was to bring the quantitative model checking and weighted automata communities together with the goal of discussing the latest developments in those areas. The second objective of this workshop was to go one major step further. In fact, it has been recently observed an increasing usage (and demand) of quantitative models in a wide range of new application domains. This includes, e.g., systems biology and energy grid. However, these different communities are often not aware of each other. This seminar had the major objective to put those various communities in contact with the hope of creating fruitful long term collaborations.
Quantitative model checking covers extended automata-based models that permit to reason on quantities. 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 zone has led to a number of tools -- e.g. BIP, Kronos, UPPAAL -- which support efficient analysis (reachability and model checking) of timed automata. Later the more expressive formalism of hybrid automata was introduced and popularized by Henzinger et al and the introduction of the tool HyTech provided a semi-decision algorithm for analyzing so-called linear hybrid systems. Whereas in timed automata the continuous part of a model is restricted to be clocks (which always evolve with rate 1), linear hybrid automata allow more general continuous variables with evolution rates in arbitrary intervals. 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 were 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.
Driven by new needs in areas such as cyber physical systems, a series of recent work have tried to combine real-time with stochastic aspects, leading to new models such as timed stochastic automata. One of the main objectives of the seminar was to study those new models and put them in perspective with similar results in weighted automata. The new notion of energy automata (Larsen, Markey, Bouyer, ...) that extends price timed automata and permits to reason on energy problems was also discussed and put in perspective with similar work done at the weighted automata level.
Weighted automata on finite words were already investigated in seminal work of Schützenberger (1961) and Chomsky and Schützenberger (1963). They consist of classical finite automata in which the transitions carry weights which may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. This concept soon developed a flourishing theory. Recently, motivated by practical examples of energy consumption, new quantitative automata models have been introduced and investigated in which the weights of finite or infinite paths are computed e.g. by the average weights or by the accumulation points of the average weights of their transitions. Colcombet (2009) studied regular cost functions which permit a quantitative extension of classical equivalence results relating automata, expressions, algebraic recognizability, and variants of monadic second-order logic. Gastin et al (2010) introduced weighted pebble automata in order to capture the expressive power of weighted extensions of Xpath for XML documents, or temporal logics for linear behaviors. All these concepts provide totally new models for which weighted automata-theoretic methods can often be applied successfully. It was very profitable therefore to bring these different communities together.
Another main theme of the seminar was to create interaction with researchers working in areas where the theoretical models and techniques may have potential applications. In systems biology, the challenge is not only to find mathematical models, but also to define new efficient quantitative analysis techniques capable of coping with very large size complex systems. Two promising applications are 1) using SMC-based techniques to monitor complex properties that cannot be expressed in classical temporal logic (e.g., oscillation properties), and 2) using interface theories as a formal characterization of phenomena in the area of synthetic biology. As another application area, the challenge of smart electricity grids is to balance the behavior of all participants (suppliers and consumers) to improve efficiency and stability. Again, quantitative models such as energy automata and analysis are emerging as potential key techniques.
In the seminar, 40 researchers from 13 countries discussed their recent research results and developments for quantitative models and their analysis. Five survey lectures, including two lectures covering the application domains, and 32 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, formal model checking and simulation methods adopted by industry, programmable single-cell biocomputers, models for smart grid balancing, and asymptotic analysis of weighted automata. The lectures and talks dealt with, e.g., quantitative logics and their semantics, expressiveness of models including quantitative measures for infinite behavior (like discounting, mean payoff, long-run averages), and statistical model checking of stochastic hybrid systems, 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 connection between energy automata, energy functions and weighted automata, on weighted specification languages used in more algebraic settings, on energy games, and on the combination of real-time and probabilism. 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 international workshop in Leipzig on "Weighted Automata: Theory and Applications (WATA 2014)".
During the seminar, there was very much interaction between the participants. In particular, the seminar was successful in attracting academic researchers with contacts to industry; this was felt very positive and should definitely be continued. Generally, 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.
Creative Commons BY 3.0 Unported license
Manfred Droste, Paul Gastin, Kim Guldstrand Larsen, and Axel Legay
- Giorgio Bacci (Aalborg University, DK) [dblp]
- Giovanni Bacci (Aalborg University, DK) [dblp]
- Benedikt Bollig (ENS - Cachan, FR) [dblp]
- Miroslav Ciric (University of Nis - Serbia, RS) [dblp]
- Thomas Colcombet (CNRS / University Paris-Diderot, FR) [dblp]
- Julie De Pril (University of Mons, BE) [dblp]
- Laurent Doyen (ENS - Cachan, FR) [dblp]
- Manfred Droste (Universität Leipzig, DE) [dblp]
- Zoltan Esik (University of Szeged, HU) [dblp]
- Javier Esparza (TU München, DE) [dblp]
- Ulrich Fahrenberg (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Emmanuel Filiot (Free University of Brussels, BE) [dblp]
- Paul Gastin (ENS - Cachan, FR) [dblp]
- Daniel Gebler (VU University Amsterdam, NL) [dblp]
- Cyrille Jegourel (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Heinz Koeppl (ETH Zürich, CH) [dblp]
- Jan Kretinsky (TU München, DE) [dblp]
- Antonin Kucera (Masaryk University - Brno, CZ) [dblp]
- Dietrich Kuske (TU Ilmenau, DE) [dblp]
- Kai Lampka (Uppsala University, SE) [dblp]
- Kim Guldstrand Larsen (Aalborg University, DK) [dblp]
- Axel Legay (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Björn Lisper (Mälardalen University - Västerås, SE) [dblp]
- Sylvain Lombardy (University of Bordeaux, FR) [dblp]
- Jan Madsen (Technical University of Denmark - Lyngby, DK) [dblp]
- Nicolas Markey (ENS - Cachan, FR) [dblp]
- Benjamin Monmege (Free University of Brussels, BE) [dblp]
- Vitaly Perevoshchikov (Universität Leipzig, DE) [dblp]
- Tatjana Petrov (IST Austria - Klosterneuburg, AT) [dblp]
- Karin Quaas (Universität Leipzig, DE) [dblp]
- Christian Reidys (University of Southern Denmark - Odense, DK) [dblp]
- Martin Riedl (Universität der Bundeswehr - München, DE) [dblp]
- Cristian Riveros (Pontificia Universidad Catolica de Chile, CL) [dblp]
- Jacques Sakarovitch (ENST - Paris, FR) [dblp]
- Sean Sedwards (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Gerard J. M. Smit (University of Twente, NL) [dblp]
- Jeremy Sproston (University of Turin, IT) [dblp]
- Bart Theelen (Embedded Systems Institute - Eindhoven, NL) [dblp]
- Thomas Weidner (Universität Leipzig, DE) [dblp]
- Rafael Wisniewski (Aalborg University, DK) [dblp]
Related Seminars
- Dagstuhl Seminar 10031: Quantitative Models: Expressiveness and Analysis (2010-01-17 - 2010-01-22) (Details)
Classification
- modelling / simulation
- semantics / formal methods
- verification / logic
Keywords
- quantitative model checking
- weighted automata
- systems biology
- energy grid
- smart buildings
- multicore platforms
