WPHS-ATVA 2015 - 2015 Workshop on Probabilistic and Hybrid Systems

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.