MoRe 2019

2nd International Workshop on Multi-objective Reasoning in Verification and Synthesis

This event is a LICS 2019 workshop, held on June 22, 2019, in Vancouver, Canada.

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:

  • games (and related models) with multiple qualitative and quantitative objectives;
  • multi-criteria reasoning in probabilistic models (e.g., percentile queries, quantiles, trade-off between worst-case and average-case performance);
  • extensions of timed automata including probabilistic or weighted aspects;
  • stochastic hybrid systems;
  • temporal logics enabling quantitative reasoning;
  • probabilistic programs;
  • practical applications involving multi-objective challenges;
  • any related attempt to tackle trade-offs between multiple criteria in formal models for verification and synthesis.
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

  • Stéphane Le Roux, Arno Pauly and Mickael Randour, Extending finite-memory determinacy by Boolean combination of winning conditions.
  • Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj and Mickael Randour, Life is Random, Time is Not: Markov Decision Processes with Window Objectives.
  • Véronique Bruyère, Guillermo Perez, Jean-François Raskin and Clément Tamines, Solving generalized parity games via safety games.
  • Petr Jancar, EXPSPACE-Complete Variant of Countdown Games, with an Application.
  • Rodica Condurache, Youssouf Oualhadj and Nicolas Troquard, Energy sensitive rational synthesis.
  • Krishnendu Chatterjee and Laurent Doyen, Stochastic Games with Generalized Mean-Payoff Objectives.

Programme

Saturday, June 22

08:30-09:00 Welcome.
09:00-10:00 Invited talk: Michael Blondin - Automatic analysis of population protocols.
10:00-10:30 Coffee break.
10:30-11:00 Clément Tamines - Solving generalized parity games via safety games.
11:00-11:30 Mickael Randour - Extending finite-memory determinacy by Boolean combination of winning conditions.
11:30-12:00 Petr Jancar - EXPSPACE-Complete Variant of Countdown Games, with an Application.
12:00-12:30 Youssouf Oualhadj - Energy sensitive rational synthesis.
12:30-14:00 Lunch.
14:00-15:00 Invited talk: David Parker - Multi-objective Reasoning with Probabilistic Model Checking.
15:00-15:30 Florent Delgrange - Life is Random, Time is Not: Markov Decision Processes with Window Objectives.
15:30-16:00 Coffee break.
16:00-16:30 Laurent Doyen - Stochastic Games with Generalized Mean-Payoff Objectives.
16:30-17:00 Discussion.

Venue

MoRe 2019 is co-located with LICS 2019, in Vancouver, Canada. Further information will be announced when available.

Past events

  • MoRe 2018, 1st International Workshop on Multi-objective Reasoning in Verification and Synthesis, FLoC 2018 workshop, Oxford, UK, July 13, 2018.

MoRe 2019 is supported by Complexys, the UMONS research institute for complex systems.