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