quantitative model checking
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:
- 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.
abstract pdf bib draft - 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.
abstract pdf bib - Cost-Algebraic Heuristic Search
Stefan Edelkamp, Shahid Jabbar, Alberto Lluch Lafuente, Twentieth National Conference on Artificial Intelligence (AAAI-05), July 2005.
abstract pdf bib slides - A logic for graphs with QoS
Gianluigi Ferrari, Alberto Lluch Lafuente, 1st Workshop on Views On Designing Complex Architectures, September 2004.
abstract pdf bib slides
