Compositionality for quantitative specifications
From MaRDI portal
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 1693527 (Why is no real title available?)
- scientific article; zbMATH DE number 1351867 (Why is no real title available?)
- scientific article; zbMATH DE number 1104375 (Why is no real title available?)
- scientific article; zbMATH DE number 2017345 (Why is no real title available?)
- A behavioural pseudometric for probabilistic transition systems
- A spatial logic for concurrency. I
- Acceptance trees
- Automata, Languages and Programming
- Compositionality for quantitative specifications
- Consistency and refinement for interval Markov chains
- Constraint Markov chains
- Distances between processes: a pure algebraic approach
- Extending modal transition systems with structured labels
- Formal Modeling and Analysis of Timed Systems
- General quantitative specification theories with modal transition systems
- General quantitative specification theories with modalities
- Generalized quantitative analysis of metric transition systems
- Graphical versus logical specifications
- Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory
- Linear logic
- Merging partial behaviour models with different vocabularies
- Metrics for labelled Markov processes
- MoTraS: a tool for modal transition systems and their extensions
- Modal event-clock specifications for timed component-based design
- Modal specifications for the control theory of discrete event systems
- Modal transition systems: composition and LTL model checking
- Model checking discounted temporal properties
- Modular Markovian Logic
- On determinism in modal transition systems
- Probabilistic Modal μ-Calculus with Independent Product
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- Quantitative refinement for weighted modal transition systems
- Reactive Systems
- Refinement and difference for probabilistic automata
- Results on the propositional \(\mu\)-calculus
- Robust specification of real time components
- Robust synthesis for real-time systems
- Simulation distances
- Structural Refinement for the Modal nu-Calculus
- Structural operational semantics for stochastic and weighted transition systems
- Taking it to the limit: approximate reasoning for Markov processes
- The quantitative linear-time-branching-time spectrum
- The quantitative linear-time-branching-time spectrum
- Weighted modal transition systems
Cited in
(10)- General quantitative specification theories with modal transition systems
- Richer interface automata with optimistic and pessimistic compatibility
- Quotient of acceptance specifications under reachability constraints
- General quantitative specification theories with modalities
- Compositional branching-time measurements
- Composition of assumption-commitment specifications in a UNITY style
- Computing branching distances with quantitative games
- Constructive Specifications for Compositional Units
- Composition of default specifications
- Compositionality for quantitative specifications
This page was built for publication: Compositionality for quantitative specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1797783)
