HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Compositionality for Quantitative Specifications

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.
Complete list of metadata

Cited literature [58 references]  Display  Hide  Download

https://hal.inria.fr/hal-01088154
Contributor : Uli Fahrenberg Connect in order to contact the contributor
Submitted on : Thursday, November 27, 2014 - 2:50:42 PM
Last modification on : Thursday, January 20, 2022 - 5:33:11 PM
Long-term archiving on: : Friday, April 14, 2017 - 9:53:10 PM

File

dmts.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01088154, version 1

Citation

Uli Fahrenberg, Jan Křetínský, Axel Legay, Louis-Marie Traonouez. Compositionality for Quantitative Specifications. [Research Report] Inria Rennes. 2014. ⟨hal-01088154⟩

Share

Metrics

Record views

171

Files downloads

70