Comparative branching-time semantics for Markov chains

DOI10.1016/J.IC.2005.03.001MaRDI QIDQ2387196zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Christel Baier, Holger Hermanns, 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

(weak) Bisimulation(weak) SimulationComparative semanticsMarkov chainTemporal logic

Mathematics Subject Classification ID

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

Recommendations

• CONCUR 2003 - Concurrency Theory
• Transition semantics for branching time
• Applying Formal Methods: Testing, Performance, and M/E-Commerce
• Branching-time model-checking of probabilistic pushdown automata
• Branching-time model-checking of probabilistic pushdown automata
• Linear-Time Model Checking Branching Processes
• Timed comparisons of semi-Markov processes
• Topological aspects of branching-time semantics
• Model-checking continuous-time Markov chains

Cites work

• A calculus of communicating systems
• A logic for reasoning about time and reliability
• Approximating labelled Markov processes
• Bisimulation through probabilistic testing
• Branching time and abstraction in bisimulation semantics
• Characterizing finite Kripke structures in propositional temporal logic
• CONCUR 2003 - Concurrency Theory
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Deciding bisimilarity and similarity for probabilistic processes.
• Exact and ordinary lumpability in finite Markov chains
• Extended Markovian Process Algebra
• Finite Continuous Time Markov Chains
• Forward and backward simulations. I. Untimed Systems
• Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
• scientific article; zbMATH DE number 1701760 (Why is no real title available?)
• scientific article; zbMATH DE number 4179422 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 149518 (Why is no real title available?)
• scientific article; zbMATH DE number 1306878 (Why is no real title available?)
• scientific article; zbMATH DE number 1325007 (Why is no real title available?)
• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• 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 1927572 (Why is no real title available?)
• scientific article; zbMATH DE number 1927573 (Why is no real title available?)
• scientific article; zbMATH DE number 1759619 (Why is no real title available?)
• scientific article; zbMATH DE number 1759621 (Why is no real title available?)
• scientific article; zbMATH DE number 1884410 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• scientific article; zbMATH DE number 7280017 (Why is no real title available?)
• scientific article; zbMATH DE number 3249395 (Why is no real title available?)
• scientific article; zbMATH DE number 3082073 (Why is no real title available?)
• Interactive Markov chains. And the quest for quantified quality
• Model-checking continuous-time Markov chains
• Optimal state-space lumping in Markov chains
• Probabilistic weak simulation is decidable in polynomial time
• Reactive, generative, and stratified models of probabilistic processes
• Temporal logics for the specification of performance and reliability
• The existence of refinement mappings
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
• Three logics for branching bisimulation

Cited in

(44)

• Assisting the design of a groupware system - Model checking usability aspects of thinkteam
• Probabilistic bisimulation for realistic schedulers
• Opacity for linear constraint Markov chains
• Lumping-based equivalences in Markovian automata: algorithms and applications to product-form analyses
• Proportional lumpability and proportional bisimilarity
• Trust evidence logic
• Relating strong behavioral equivalences for processes with nondeterminism and probabilities
• Logical characterization of fluid equivalences
• Non-bisimulation-based Markovian behavioral equivalences
• Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
• A space-efficient simulation algorithm on probabilistic automata
• Least upper bounds for probability measures and their applications to abstractions
• Model checking for performability
• Lumping and reversed processes in cooperating automata
• On Abstraction of Probabilistic Systems
• Computing Behavioral Relations for Probabilistic Concurrent Systems
• Bisimulations and logical characterizations on continuous-time Markov decision processes
• The how and why of interactive Markov chains
• Bisimulations meet PCTL equivalences for probabilistic automata
• Non-termination and secure information flow
• Persistent stochastic non-interference
• Deciding Simulations on Probabilistic Automata
• On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems
• A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
• Three-valued abstraction for probabilistic systems
• scientific article; zbMATH DE number 1927572 (Why is no real title available?)
• On the tradeoff between compositionality and exactness in weak bisimilarity for integrated-time Markovian process calculi
• scientific article; zbMATH DE number 7559464 (Why is no real title available?)
• Persistent stochastic non-interference
• Probabilistic bisimulation for realistic schedulers
• Bisimulation and Simulation Relations for Markov Chains
• Markovian testing and trace equivalences exactly lump more than Markovian bisimilarity
• A semantics for every GSPN
• Compositional design of stochastic timed automata
• CONCUR 2003 - Concurrency Theory
• The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
• The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
• A Hemimetric Extension of Simulation for Semi-Markov Decision Processes
• On the use of model and logical embeddings for model checking of probabilistic systems
• A probabilistic modal logic for context-aware trust based on evidence
• A spectrum of approximate probabilistic bisimulations
• Trace semantics for stochastic systems with nondeterminism
• A faster-than relation for semi-Markov decision processes
• Branching bisimulation congruence for probabilistic systems

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

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