\textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics

DOI10.1016/J.JLAMP.2017.10.002MaRDI QIDQ1683708zbMATH OpenOpenAlexFDO

Authors Marco Bernardo

Publication date 1 December 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2017.10.002

zbMATH Keywords

behavioral metamodelsbisimulation semanticscompositionalitytrace semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Towards general axiomatizations for bisimilarity and trace semantics
• Compositionality and bisimulation: A negative result
• Beyond Bisimulation: The “up-to” Techniques
• Compositional bisimulation metric reasoning with Probabilistic Process Calculi
• scientific article; zbMATH DE number 1330448
• Up-to techniques for generalized bisimulation metrics
• Compositional verification of concurrent systems by combining bisimulations
• Deriving Bisimulation Congruences with Borrowed Contexts
• A compositional protocol verification using relativized bisimulation
• \(\tau\)-bisimulations and full abstraction for refinement of actions

Cites work

• A Theory of Communicating Sequential Processes
• A theory of timed automata
• A uniform definition of stochastic process calculi
• A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
• Algebraic laws for nondeterminism and concurrency
• Approximating labelled Markov processes
• Automatic verification of real-time systems with discrete probability distributions.
• Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes
• Bisimulation of labelled state-to-function transition systems coalgebraically
• Bisimulation through probabilistic testing
• Bisimulations meet PCTL equivalences for probabilistic automata
• Finite state Markovian decision processes
• Formal verification of parallel programs
• Foundations of Software Science and Computational Structures
• Handbook of weighted automata
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 729460 (Why is no real title available?)
• scientific article; zbMATH DE number 7318983 (Why is no real title available?)
• Non-bisimulation-based Markovian behavioral equivalences
• Probabilistic communicating processes
• Reactive, generative, and stratified models of probabilistic processes
• Relating strong behavioral equivalences for processes with nondeterminism and probabilities
• Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
• Revisiting trace and testing equivalences for nondeterministic and probabilistic processes
• Scalar Outcomes Suffice for Finitary Probabilistic Testing
• Structural operational semantics for non-deterministic processes with quantitative aspects
• Structural Operational Semantics for Weighted Transition Systems
• Structural operational semantics.
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.

Cited in

(3)

• Towards general axiomatizations for bisimilarity and trace semantics
• Logical characterization of fluid equivalences
• Performance preserving equivalence for stochastic process algebra dtsdPBC

This page was built for publication: \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1683708)