Topics

MoRe aims at bringing together researchers interested in multi-objective reasoning for verification and synthesis.

Traditionally, verification and synthesis techniques focus on a single qualitative or quantitative objective for the reactive system. In practice, it is often desired that systems satisfy a functional requirement expressed as a qualitative property, while optimising some quantitative dimension (e.g., reach a target state while minimising the energy consumption). Furthermore, there are numerous application contexts in which reasoning simultaneously about multiple, heterogeneous quantitative and qualitative characteristics is important. In many cases, the analysis of such systems may be complicated by the fact that there are trade-offs between objectives. Such trade-offs may also arise between several interpretations of the same quantitative dimension: for example, between the average-case and the worst-case performance of a system.

MoRe is a meeting place for researchers in the area of multi-objective reasoning for verification and synthesis, with topics of interest ranging from novel theoretical models to industrial challenges and practical applications. Typical topics of the workshop include, but are not limited to, formal approaches toward verification and synthesis in the following settings:

For any questions, please contact Mickael Randour at <firstname>.<lastname>@gmail.com

Program committee

Program committee chairs

Program committee

Invited speakers

David Parker, University of Birmingham, United Kingdom

Multi-objective Reasoning with Probabilistic Model Checking

Probabilistic model checking is a versatile technique for verifying quantitative properties of systems that exhibit stochastic behaviour. It can provide formal guarantees on a wide range of system properties, such as safety, reliability, energy efficiency or security. Often, it is important to consider trade-offs between such properties, either because they are inherently conflicting or because different components or agents have opposing goals. This talk will give an overview of the probabilistic model checking tools PRISM and PRISM-games, and describe some of the current advances being made in their development. This includes techniques for controller synthesis and multi-objective verification for models such as Markov decision processes and stochastic games. These will be illustrated with applications from various domains including robotics, energy management and task scheduling.

Michael Blondin, Université de Sherbrooke, Canada

Automatic analysis of population protocols

Population protocols are a model of distributed computing in which replicated mobile agents with limited computational power interact stochastically to achieve a common task. They provide a simple and elegant formalism to model, e.g., networks of passively mobile sensors and chemical reaction networks. Devising algorithms for the formal analysis of population protocols is particularly challenging as it involves inspecting an infinite number of input configurations, each giving rise to a finite Markov chain. In this talk, I will discuss some advances on the formal analysis of population protocols such as verifying their correctness and automatically deriving asymptotic bounds on their expected termination time.

Accepted contributions

Programme

Saturday, June 22

Past events