Compositionality for Quantitative Specifications

Abstract : We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.
Type de document :
Communication dans un congrès
FACS, Sep 2014, Bertinoro, Italy. 2014
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087320
Contributeur : Uli Fahrenberg <>
Soumis le : mardi 25 novembre 2014 - 17:38:52
Dernière modification le : mercredi 11 avril 2018 - 02:01:25
Document(s) archivé(s) le : jeudi 26 février 2015 - 12:25:44

Fichier

1408.1256v1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01087320, version 1

Citation

Uli Fahrenberg, Jan Křetínský, Axel Legay, Louis-Marie Traonouez. Compositionality for Quantitative Specifications. FACS, Sep 2014, Bertinoro, Italy. 2014. 〈hal-01087320〉

Partager

Métriques

Consultations de la notice

446

Téléchargements de fichiers

57