Quantitative Modal Logics  
     Adequacy, Expressiveness, Compositionality and Decidability

	      Kim G. Larsen (Aalborg University, Denmark)


In this talk we present a number of quantitative extensions of
so-called Hennessy-Milner Logic - as well as modal mu-calculus -
tailored for real-time, weighted and probabilistic reactive systems.
Hennessy-Milner logic has been demonstrated to enjoy a number of
extremely useful properties: in particular, the equivalence between
systems induced by the logic is that of bisimularity; in fact for each
finite-state process its bisimulation equivalence class may be
characterized by a single formula, thus reducing equivalence checking
to a model-checking problem, an approach originally pursued by Anna
Ingolfsdottir.  Also, the logic allows for compositional verification,
has validity being axiomatizable and satisfiability being
decidable. In the talk we shall investigate to what extent the
quantitative extensions of Hennessy-Milner logic enjoys the same
properties.

Bio sketch

Kim G. Larsen received the Danish Citation Laureates Award (Thomson
Scientific) as the most cited Danish Computer Scientist in the period
1990-2004, the 2013 CAV Award for his work on UPPAAL “the foremost
model checker for real-time systems” and an ERC Advanced Grant for the
project LASSO (Learning, Analysis, Synthesis and Optimization of
Cyber-Physical Systems), which started in November 2015. Kim has
published over 300 scientific papers, has received over 21,500
citations to his scientific work and his h-index is 71 according to
Google Scholar.