MoRe 2018

1st International Workshop on Multi-objective Reasoning in Verification and Synthesis

This event is a FLoC 2018 workshop, held on July 13, 2018, in Oxford, UK.


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);
  • probabilistic programs;
  • extensions of timed automata including probabilistic or weighted aspects;
  • stochastic hybrid systems;
  • temporal logics enabling quantitative reasoning;
  • 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>


May 15, 2018. Accepted contributions announced.
November 16, 2017. Program committee announced.
November 03, 2017. Invited speakers announced.
August 29, 2017. Website online.

Program committee

Program committee chairs

Program committee

Invited speakers

Christel Baier, Technische Universität Dresden, Germany

Conditioning and quantiles in Markovian models.

The classical multi-objective analysis of Markov decision processes (MDP) and other stochastic models with nondeterminism seeks for policies to resolve the nondeterministic choices that achieve Pareto-optimality or maximize/minimize a linear goal function, while satisfying a list of probability or expectation constraints. Other approaches to reason about the trade-off between multiple cost and reward functions rely on conditioning or quantiles. The former, for instance, can serve to synthesize policies that maximize the expected utility in energy-critical situations or to minimize the cost of repair mechanism in exceptional error scenarios. Quantiles can, e.g., be used to identify policies with a minimal cost bound for meeting a utility constraint with sufficiently high probability. While algorithms for conditional probabilities in MDPs can rely on a fairly simple model transformation, reasoning about conditional expected accumulated costs and quantiles is computationally more difficult. The talk presents an overview of recent results in these directions.

Benjamin Monmege, Aix-Marseille Université, France

A journey through negatively-weighted timed games: undecidability, decidability, approximability.

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers in real-time systems. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. However, for a few years now, we explored, and we continue to explore, the world of weighted timed games with negative weights too, in order to get a more useful modelling mechanism. This gave rise to stronger undecidability results, but we also discovered new decidable fragments. In this talk, I will survey these results: decidability when limiting the number of distinct weights in the game, using corner-point abstraction techniques; decidability for a large fragment of one-clock weighted timed games, and for the so-called divergent weighted timed games, using value iteration schemes; approximability in the case of the so-called almost-divergent weighted timed games.

Accepted contributions

  • Dimitri Scheftelowitsch, Multi-Scenario Uncertainty in Markov Decision Processes.
  • Thomas Brihaye, Mickael Randour and Cédric Rivière, Stochastic o-minimal hybrid systems.
  • Thomas Brihaye, Véronique Bruyère, Aline Goeminne and Jean-François Raskin, Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives.
  • Véronique Bruyère, Quentin Hautem and Jean-Francois Raskin, Parameterized complexity of games with monotonically ordered omega-regular objectives.
  • Adrien Le Coent, Kim Guldstrand Larsen, Marco Muniz and Jiri Srba, Comfort and Energy Optimization for Floor Heating Systems.
  • Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann, Multiple Objectives and Cost Bounds in MDP.
  • Gilles Geeraerts, Shibashis Guha and Jean-Francois Raskin, Safe and Optimal Scheduling of Hard and Soft Tasks.
  • Mohammadhosein Hasanbeig, Alessandro Abate and Daniel Kroening, Logically-Constrained Reinforcement Learning.


MoRe 2018 is co-located with FLoC 2018, in Oxford, UK. Further information will be announced when available.