--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Uli foaf_name: Fahrenberg, Uli foaf_surname: Fahrenberg - foaf_Person: foaf_givenName: Jan foaf_name: Kretinsky, Jan foaf_surname: Kretinsky foaf_workInfoHomepage: http://www.librecat.org/personId=44CEF464-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-8122-2881 - foaf_Person: foaf_givenName: Axel foaf_name: Legay, Axel foaf_surname: Legay - foaf_Person: foaf_givenName: Louis foaf_name: Traonouez, Louis foaf_surname: Traonouez bibo_doi: 10.1007/978-3-319-15317-9_19 bibo_volume: 8997 dct_date: 2015^xs_gYear dct_language: eng dct_publisher: Springer@ dct_title: Compositionality for quantitative specifications@ ...