Friday, May 25, 2018

[DMANET] 1st Workshop on Multi-objective Reasoning in Verification and Synthesis (MoRe 2018): call for participation

[Apologies for multiple copies]


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

MoRe 2018

Friday 13th July 2018, Oxford, United Kingdom
FLoC 2018 workshop, affiliated with LICS 2018



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
- multi-criteria reasoning in probabilistic models (e.g., percentile
queries, quantiles, trade-off between worst-case and average-case
- probabilistic programs;
- extensions of timed automata including probabilistic or weighted
- 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.


Christel Baier, Technische Universität Dresden, Germany
"Conditioning and quantiles in Markovian models"

Benjamin Monmege, Aix-Marseille Université, France
"A journey through negatively-weighted timed games: undecidability,
decidability, approximability"


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"


Through the FLoC registration web page:
Early registration deadline is 6 June.


Program committee chairs

- Mickael Randour, UMONS - Université de Mons, Belgium
- Jeremy Sproston, University of Turin, Italy

Program committee

- Shaull Almagor, University of Oxford, UK
- Nathalie Bertrand, INRIA Rennes Bretagne-Atlantique, France
- Véronique Bruyère, UMONS - Université de Mons, Belgium
- Krishnendu Chatterjee, IST Austria, Austria
- Joost-Pieter Katoen, RWTH Aachen, Germany
- Sadegh Soudjani, University of Newcastle, UK
- Ufuk Topcu, University of Texas at Austin, USA
- Ashutosh Trivedi, University of Colorado Boulder, USA

* Contributions to be spread via DMANET are submitted to
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.