Workshop on Probabilistic and Hybrid Systems

(satellite event of ATVA 2015)


Workshop description
Call for participation
Important dates

Workshop description

The interplay of random phenomena with discrete-continuous dynamics deserves increased attention in many systems of growing importance. Their verification needs to consider both stochastic behaviour and hybrid dynamics. Probabilistic and Hybrid Systems are modeled in well studied mathematical frameworks that permit to check whether the modeled real world system respects the designed properties. This check is based on formal verification techniques, such as model checking, that have been successfully applied to complex systems such as operating system’s hardware drivers, airborne software and consumer electronic protocols. Usually the properties are specified in one of the proposed temporal logics, such as PCTL, PLTL, CSL, and so on.

These logics support the specification of quantitative properties: instead of considering only whether the modeled system satisfies a given property, we can ask what it is the probability that the system satisfies the property.

A quantitative property can be used to specify the requirements of a system exhibiting randomized choices, costs, time, and security aspect. These characteristics are the key ingredients for modeling and analyzing networked, embedded, biological and energy systems.

Several tools have been developed and used to automatically check the probabilistic and hybrid systems and there is a vast literature on how to solve the verification problem and enhance the verification techniques so that more complex real life case studies can be modeled and analyzed.

The main purpose of this workshop on Probabilistic and Hybrid Systems is to let people working on these topics meet and discuss their ideas and results.
For this, we solicits the submission of talk proposals covering any of the aspects of the formal verification of probabilistic and hybrid systems. Examples of these aspects are new algorithms for improving the verification, application of existing methods to emerging scenarios, and tool demonstrations.

Call for participation

We invite you to submit your talk proposal via EasyChair. The proposal has to be in English and formatted according to the LNCS style. The proposal should contain the title of your talk as well as an extended abstract describing the topic of the talk, taking no more than 2 pages (references excluded).

The talk has to be related to the main topics of the workshop, and it can be about both published and unpublished results. The workshop has no official proceedings; for participants’ convenience, a copy of the abstracts will be distributed.

Important dates

July 1, 2015 Talk proposal deadline
July 31, 2015 Talk acceptance notification
August 15, 2015 Talk proposal final version deadline
October 12-15, 2015 ATVA 2015 main conference and tutorials (WPHS exact date to be announced)

Program committee

Program co-chairs:

  • Ernst Moritz Hahn (Institute of Software, Chinese Academy of Sciences, Beijing, China)
  • Andrea Turrini (Institute of Software, Chinese Academy of Sciences, Beijing, China)

Program committee

  • Alessandro Abate (University of Oxford, Oxford, UK)
  • Erika Ábrahám (RWTH Aachen University, Aachen, Germany)
  • Lei Bu (Nanjing University, Nanjing, China)
  • Yuxin Deng (Shanghai Jiaotong University, Shanghai, China)
  • Tingting Han (Birkbeck University of London, London, UK)
  • Wanwei Liu (National University of Defence Technology, Changsha, China)
  • Zhikun She (Beihang University, Beijing, China)
  • Verena Wolf (Saarland University, Saarbrücken, Germany)
  • Nicolás Wolovick (Universidad Nacional de Córdoba, Córdoba, Argentina)
  • Naijun Zhan (Institute of Software, Chinese Academy of Sciences, Beijing, China)