CAP 2017: First Workshop on Composition, Abstraction, and Parametrization for the Verification of Probabilistic and Hybrid Systems

Technical Information

 

Quantitative verification strives to answer questions which go beyond the classical yes/no answers of traditional verification techniques: What is the probability that a safety-critical state is entered within 10 hours of operation? How large is the expected power consumption in the worst case? Because the size of the state space is typically exponential in the number of system components (the infamous “state space explosion problem”), scalability is of major concern for applying quantitative verification techniques to real-world systems. The fact that numerical computations need to be performed, makes this issue even more serious. This is similar to the verification of hybrid systems, whose state space contains both discrete and continuous components and is therefore uncountably infinite. They are essential for analyzing embedded systems which typically measure real-valued quantities like temperature, voltages, or velocity, use digital circuits to process them and to operate actors like engines, heatings etc. which act upon the measured quantities in a closed loop. Both, probabilities and hybrid state spaces, can be combined in order to analyze systems for which both continuous quantities and probabilities play a role.

Many techniques have been devised to cope with very large or even infinite state spaces. Examples are exploiting compositionality, abstraction, and parametrization. Compositionality refers to the fact that large systems are typically constructed from simpler components, and verification can exploit this structure to reduce the size of the state space that needs to be analyzed. Abstraction is a fundamental principle in computer science, based on omitting irrelevant details. In verification, abstraction is used in various ways for reducing the size of state spaces and simplifying verification tasks. Finally, parametrization allows one to handle families of systems which only differ in the value of one more more parameters.

The workshop is rooted in the collaboration project CAP which is a joint project of the Institute of Software of the Chinese Academy of Sciences (ISCAS), Peking University, and Tsinghua University on the Chinese side and Saarland University, RWTH Aachen University and the Albert-Ludwigs-Universität Freiburg on the Germany side. It is funded by the Sino-German Center for the Advancement of Science (CDZ). The focus of the project is making quantitative verification techniques for probabilistic and hybrid systems scale to real-world applications.

The topic of the workshop – scalability of quantitative verification – is a central challenge for the whole verification community. While verification of digital circuits is more mature, applicable to circuits of industrial size, and has already gained acceptance in industry, the analysis of probabilistic and hybrid systems is currently a hot topic with an active research community. The workshop shall provide a forum where current trends and developments in probabilistic and hybrid system verification can be discussed. We want not only to transport results from the CAP project into the verification community, but also draw inspiration from ideas developed outside the project. Therefore the workshop is open for all interested participants. We expect that it is of great interest and a good complement for many people who are going to attend CAV.

Related workshops:
  • QAPL (Quantitative Aspects of Programming Languages, affiliated to ETAPS)

 

Organizational Information

 

Title: First Workshop on Composition, Abstraction, and Parametrization for the Verification of Probabilistic and Hybrid Systems (CAP 2017)

Workshop Organizers:
Ralf Wimmer (Chair)

Chair of Computer Architecture
Albert-Ludwigs-Universität Freiburg
Georges-Köhler-Allee 51
79110 Freiburg im Breisgau
Germany
Phone: +49 761 203 8179
Fax: +49 761 203 8142
E-Mail: wimmer@informatik.uni-freiburg.de
Web: http://www.informatik.uni-freiburg.de/~wimmer

Sun Meng (Co-chair)

Department of Information Science
School of Mathematical Sciences Peking University
Science Building No. 1, Room 1382E
Yiheyuan Road No. 5, Haidian District, Beijing, 10087
People’s Republic of China
Phone: +86 10 62768931
Fax: +86 10 62751801
E-Mail: sunmeng@math.pku.edu.cn
Web: http://www.math.pku.edu.cn/teachers/sunm/indexen.html

Previous experience in organizing workshops and conferences:

  • Ralf Wimmer has organized the 19 th GI/ITG/GMM-Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2016)” in March 2016 in Freiburg, Germany. See https://ira.informatik.uni-freiburg.de/mbmv2016/ for more information.

Main contact: Ralf Wimmer

Duration of the workshop: 2 days

Estimated number of participants: 30–40 (roughly 15–20 from the CAP project)

Proposed format and agenda: On each day, there will be one or two invited talks (1 hour) from a recognized researcher in quantitative verification. Apart from the invited talks, there will be talks of 30 min length (including discussion). We will take care to leave enough time for scientific discussions.

Potential invited speakers:

  • Christel Baier (TU Dresden, Dresden)
  • Dave Parker (University of Birmingham, UK)
  • Goran Frehse (Université Grenoble Alpes, Grenoble)
  • Yuxi Fu (Shanghai Jiao Tong University, Shanghai)
  • Xinxin Liu (Institute of Software, CAS)

Procedures for selecting papers and participants: People who want to give a talk during the workshop are expected to submit an extended abstract of two pages. A technical program committee consisting of about 10 experts in probabilistic and hybrid system verification will evaluate all submissions regarding their novelty and relevance to the scope of the workshop etc.
We encourage both the submission of work in progress and of results which have already been submitted elsewhere as long as they are central to the scope of the workshop. The workshop will have a guaranteed attendance of 15–20 people from the CAP project. We can fund the attendance of CAV and the CAP workshop for a number of people from the Chinese project partners. However, the workshop will be open for everyone who is interested in the topic.

Plans for dissemination: The extended abstracts of all workshop contributions will be distributed in printed form among the participants and published online in the workshop proceedings. This makes the contributions accessible for other researchers. The library of the Albert-Ludwigs-Universität Freiburg offers publishing papers free of charge for members of the university (we used this service also for MBMV). The proceedings get a document object identifier (DOI) and can therefore be cited in other publications.