January 19 – 24 , 2014, Dagstuhl Seminar 14041
Quantitative Models: Expressiveness, Analysis, and New Applications
1 / 2 >
For support, please contact
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
Related Dagstuhl Seminar
- 10031: "Quantitative Models: Expressiveness and Analysis" (2010)
- Modelling / Simulation
- Semantics / Formal Methods
- Verification / Logic
- Quantitative model checking
- Weighted automata
- Systems biology
- Energy grid
- Smart buildings
- Multicore platforms