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
- 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
- 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?)
- Linear logic
- Merging partial behaviour models with different vocabularies
- Metrics for labelled Markov processes
- 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
- MoTraS: a tool for modal transition systems and their extensions
- 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 operational semantics for stochastic and weighted transition systems
- Structural Refinement for the Modal nu-Calculus
- 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)- Composition of assumption-commitment specifications in a UNITY style
- Compositionality for quantitative specifications
- Computing branching distances with quantitative games
- Richer interface automata with optimistic and pessimistic compatibility
- Composition of default specifications
- Quotient of acceptance specifications under reachability constraints
- General quantitative specification theories with modalities
- General quantitative specification theories with modal transition systems
- Compositional branching-time measurements
- Constructive Specifications for Compositional Units
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)
