Compositionality for Quantitative Specifications

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2015
Type Article in Proceedings
Conference The 11th International Symposium on Formal Aspects of Component Software - FACS 2014
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-15317-9_19
Field Informatics
Keywords modal transition systems; compositional design; robust systems; logic
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.