Comparative branching-time semantics for Markov chains

DOI10.1016/j.ic.2005.03.001zbMath1101.68053OpenAlexW2115555017WikidataQ57801888 ScholiaQ57801888MaRDI QIDQ2387196

Holger Hermanns, Christel Baier, Verena Wolf, Joost-Pieter Katoen

Publication date: 2 September 2005

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://research.utwente.nl/en/publications/comparative-branchingtime-semantics-for-markov-chains(8d4ddecc-c26e-43f9-b2a1-c8a880613ba2).html

zbMATH Keywords

Markov chainTemporal logic(weak) Bisimulation(weak) SimulationComparative semantics

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Markov chains (discrete-time Markov processes on discrete state spaces) (60J10) 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) Continuous-time Markov processes on discrete state spaces (60J27)

Related Items (35)

Lumping and reversed processes in cooperating automata ⋮ Non-bisimulation-based Markovian behavioral equivalences ⋮ A space-efficient simulation algorithm on probabilistic automata ⋮ Proportional lumpability and proportional bisimilarity ⋮ A Semantics for Every GSPN ⋮ Trust evidence logic ⋮ Least upper bounds for probability measures and their applications to abstractions ⋮ Probabilistic bisimulation for realistic schedulers ⋮ On Abstraction of Probabilistic Systems ⋮ Computing Behavioral Relations for Probabilistic Concurrent Systems ⋮ Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ A Hemimetric Extension of Simulation for Semi-Markov Decision Processes ⋮ Deciding Simulations on Probabilistic Automata ⋮ Three-valued abstraction for probabilistic systems ⋮ Unnamed Item ⋮ On the tradeoff between compositionality and exactness in weak bisimilarity for integrated-time Markovian process calculi ⋮ Opacity for linear constraint Markov chains ⋮ Persistent Stochastic Non-Interference ⋮ Lumping-based equivalences in Markovian automata: algorithms and applications to product-form analyses ⋮ Relating strong behavioral equivalences for processes with nondeterminism and probabilities ⋮ Compositional Design of Stochastic Timed Automata ⋮ On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems ⋮ Unnamed Item ⋮ The How and Why of Interactive Markov Chains ⋮ Probabilistic Bisimulation for Realistic Schedulers ⋮ The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism ⋮ Assisting the design of a groupware system - Model checking usability aspects of thinkteam ⋮ Bisimulations Meet PCTL Equivalences for Probabilistic Automata ⋮ Branching bisimulation congruence for probabilistic systems ⋮ Non-termination and secure information flow ⋮ Logical characterization of fluid equivalences ⋮ Model checking for performability ⋮ Bisimulation and Simulation Relations for Markov Chains ⋮ Markovian Testing and Trace Equivalences Exactly Lump More Than Markovian Bisimilarity

Cites Work

• Interactive Markov chains. And the quest for quantified quality
• The existence of refinement mappings
• Optimal state-space lumping in Markov chains
• Probabilistic weak simulation is decidable in polynomial time
• Characterizing finite Kripke structures in propositional temporal logic
• A calculus of communicating systems
• Bisimulation through probabilistic testing
• A logic for reasoning about time and reliability
• Approximating labelled Markov processes
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
• Reactive, generative, and stratified models of probabilistic processes
• Forward and backward simulations. I. Untimed Systems
• Deciding bisimilarity and similarity for probabilistic processes.
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
• Finite Continuous Time Markov Chains
• Exact and ordinary lumpability in finite Markov chains
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• Temporal logics for the specification of performance and reliability
• Model-checking continuous-time Markov chains
• CONCUR 2003 - Concurrency Theory
• Extended Markovian Process Algebra
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Comparative branching-time semantics for Markov chains