19.01.14 - 24.01.14, Seminar 14041

Quantitative Models: Expressiveness, Analysis, and New Applications

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.

Motivation

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 de fine 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).