Compositionality for Quantitative Specifications

D 2015

Compositionality for Quantitative Specifications

FAHRENBERG, Uli, Jan KŘETÍNSKÝ, Axel LEGAY and Louis-Marie TRAONOUEZ

Basic information

Original name

Compositionality for Quantitative Specifications

Authors

FAHRENBERG, Uli (276 Germany), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution), Axel LEGAY (56 Belgium) and Louis-Marie TRAONOUEZ (250 France)

Edition

Heidelberg Dordrecht London New York, The 11th International Symposium on Formal Aspects of Component Software - FACS 2014, p. 306-324, 19 pp. 2015

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00080593

Organization unit

Faculty of Informatics

ISBN

978-3-319-15316-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-15317-9_19

Keywords in English

modal transition systems; compositional design; robust systems; logic

Abstract

V originále

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.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

MUNI/A/0855/2013, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)

Investor: Masaryk University, Category A

Citovat

FAHRENBERG, Uli, Jan KŘETÍNSKÝ, Axel LEGAY and Louis-Marie TRAONOUEZ. Compositionality for Quantitative Specifications. In The 11th International Symposium on Formal Aspects of Component Software - FACS 2014. Heidelberg Dordrecht London New York: Springer, 2015, p. 306-324. ISBN 978-3-319-15316-2. Available from: https://dx.doi.org/10.1007/978-3-319-15317-9_19.

@inproceedings{1194313,
   author = {Fahrenberg, Uli and Křetínský, Jan and Legay, Axel and Traonouez, LouisandMarie},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {The 11th International Symposium on Formal Aspects of Component Software - FACS 2014},
   doi = {http://dx.doi.org/10.1007/978-3-319-15317-9_19},
   keywords = {modal transition systems; compositional design; robust systems; logic},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg Dordrecht London New York},
   isbn = {978-3-319-15316-2},
   pages = {306-324},
   publisher = {Springer},
   title = {Compositionality for Quantitative Specifications},
   year = {2015}
}

TY  - JOUR
ID  - 1194313
AU  - Fahrenberg, Uli - Křetínský, Jan - Legay, Axel - Traonouez, Louis-Marie
PY  - 2015
TI  - Compositionality for Quantitative Specifications
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783319153162
KW  - modal transition systems
KW  - compositional design
KW  - robust systems
KW  - logic
N2  - 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.
ER  -

FAHRENBERG, Uli, Jan KŘETÍNSKÝ, Axel LEGAY and Louis-Marie TRAONOUEZ. Compositionality for Quantitative Specifications. In \textit{The 11th International Symposium on Formal Aspects of Component Software - FACS 2014}. Heidelberg Dordrecht London New York: Springer, 2015, p.~306-324. ISBN~978-3-319-15316-2. Available from: https://dx.doi.org/10.1007/978-3-319-15317-9\_{}19.

Detailed Information on Publication Record