This research line regards model checking approaches where:

  • systems have quantitative aspects
  • system properties are specified by means of logics that either involve quantitative aspects in their operators or evaluate over quantitative domains
  • verification algorithms deal with quantitative nature of models and their specification

More details on this topic can be found in the following documents and the references therein:

  • Modelling and analyzing adaptive self-assembling strategies with Maude
     Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
    International Workshop on Rewriting Logic and its Applications (WRLA’12)
  • Quantitative mu-calculus and CTL defined over constraint semirings
    Alberto Lluch Lafuente, Ugo Montanari,TCS special issue on quantitative aspects of programming languages, Volume 346, Issue 1, November 2005. bib
  • A Logic for Application Level QoS
    Dan Hirsch, Alberto Lluch-Lafuente, Emilio Tuosto, Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages, Elsevier Electronic Notes on Theoretical Computer Science, 2006. bib
  • Cost-Algebraic Heuristic Search
    Stefan Edelkamp, Shahid Jabbar, Alberto Lluch Lafuente, Twentieth National Conference on Artificial Intelligence (AAAI-05), July 2005.
    abstract bib
  • A logic for graphs with QoS
    Gianluigi Ferrari, Alberto Lluch Lafuente, 1st Workshop on Views On Designing Complex Architectures, September 2004.
    abstract bib