TY - GEN
T1 - Compositionality for quantitative specifications
AU - Fahrenberg, Uli
AU - Křetínský, Jan
AU - Legay, Axel
AU - Traonouez, Louis Marie
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84922324349&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-15317-9_19
DO - 10.1007/978-3-319-15317-9_19
M3 - Conference contribution
AN - SCOPUS:84922324349
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 306
EP - 324
BT - Formal Aspects of Component Software - 11th International Symposium, FACS 2014, Revised Selected Papers
A2 - Lanese, Ivan
A2 - Madelaine, Eric
A2 - Lanese, Ivan
PB - Springer Verlag
T2 - 11th International Symposium on Formal Aspects of Component Software, FACS 2014
Y2 - 10 September 2014 through 12 September 2014
ER -