**************************************************************************
2nd International Workshop on
Multi-objective Reasoning in Verification and Synthesis
MoRe 2019
http://math.umons.ac.be/more2019/
Saturday 22nd June 2019, Vancouver, Canada
LICS 2019 workshop
**************************************************************************
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.
INVITED SPEAKERS:
David Parker, University of Birmingham, United Kingdom
"Multi-objective Reasoning with Probabilistic Model Checking"
Michael Blondin, Université de Sherbrooke, Canada
"Automatic analysis of population protocols"
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"
REGISTRATION:
Through the LICS registration web page: https://lics.siglog.org/lics19/
ORGANISATION:
Program committee chairs
- Mickael Randour, UMONS - Université de Mons, Belgium
- Jeremy Sproston, University of Turin, Italy
Program committee
- S. Akshay, IIT Bombay, India
- Christel Baier, Technische Universität Dresden, Germany
- Nathalie Bertrand, INRIA Rennes Bretagne-Atlantique, France
- Véronique Bruyère, UMONS - Université de Mons, Belgium
- Stefan Kiefer, University of Oxford, UK
- Jan Kretinsky, Technical University of Munich, Germany
- Benjamin Monmege, Aix-Marseille Université, France
- Ufuk Topcu, University of Texas at Austin, USA
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* 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.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************