SOS specifications for uniformly continuous operators
From MaRDI portal
Publication:1678172
DOI10.1016/j.jcss.2017.09.011zbMath1380.68296OpenAlexW2760914093MaRDI QIDQ1678172
Publication date: 14 November 2017
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2017.09.011
structural operational semanticsuniform continuitycompositional reasoningprobabilistic process algebrasSOS specification formats
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items
A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces ⋮ A framework to measure the robustness of programs in the unpredictable environment ⋮ Back to the format: a survey on SOS for probabilistic processes ⋮ The metric linear-time branching-time spectrum on nondeterministic probabilistic processes ⋮ Probabilistic divide \& congruence: branching bisimilarity ⋮ Unnamed Item ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ Unnamed Item ⋮ A probabilistic calculus of cyber-physical systems ⋮ Monads and Quantitative Equational Theories for Nondeterminism and Probability
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity
- On behavioural pseudometrics and closure ordinals
- Metrics for labelled Markov processes
- SOS formats and meta-theory: 20 years after
- Non-expansive \(\varepsilon\)-bisimulations for probabilistic processes
- Higher-level synchronising devices in Meije-SCCS
- Bisimulation through probabilistic testing
- Turning SOS rules into equations
- A logic for reasoning about time and reliability
- A behavioural pseudometric for probabilistic transition systems
- A structural approach to operational semantics
- Logical characterization of branching metrics for nondeterministic probabilistic transition systems
- Structural operational semantics for continuous state stochastic transition systems
- Compositionality of Hennessy-Milner logic by structural operational semantics
- The quantitative linear-time-branching-time spectrum
- Branching bisimulation for probabilistic systems: characteristics and decidability
- A general SOS theory for the specification of probabilistic transition systems
- Converging from Branching to Linear Metrics on Markov Chains
- Remarks on Testing Probabilistic Processes
- Probabilistic Barbed Congruence
- Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation
- Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
- Taking It to the Limit: Approximate Reasoning for Markov Processes
- Probabilistic bisimulation as a congruence
- Compositional Metric Reasoning with Probabilistic Process Calculi
- Compositional bisimulation metric reasoning with Probabilistic Process Calculi
- Metric Reasoning About $$\lambda $$-Terms: The General Case
- Generalized Bisimulation Metrics
- Game Refinement Relations and Metrics
- Formal verification of parallel programs
- Bisimulation can't be traced
- Linear Distances between Markov Chains
- Modal Decomposition on Nondeterministic Probabilistic Processes
- Metric reasoning about λ-terms: The affine case
- Divide and Congruence II
- A Proof System for Compositional Verification of Probabilistic Concurrent Processes
- Weak Simulation Quasimetric in a Gossip Scenario
- Precongruence formats for decorated trace semantics
- SOS specifications of probabilistic systems by uniformly continuous operators
- Formal verification of timed properties of randomized distributed algorithms
- Automata, Languages and Programming
- Semantics of Probabilistic Processes
- Metric semantics for true concurrent real time
