Compositionality for Quantitative Specifications

TL;DR

This paper introduces a compositional framework for designing and verifying systems with quantitative data, enabling refinement and analysis of actions with rewards, time, or energy, using disjunctive modal transition systems.

Contribution

It presents a novel approach to quantitative system design, including the first computation method for the quotient operation in this context.

Findings

Provides a framework for compositional quantitative system verification

Introduces computation of the quotient operation for quantitative systems

Establishes connections to modal nu-calculus and distance-based system notions

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.