Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.

DOI10.1016/S1567-8326(02)00068-1zbMath1053.68065MaRDI QIDQ1400292

Josée Desharnais, Prakash Panangaden

Publication date: 13 August 2003

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

zbMATH Keywords

Markov processesBisimulationContinuous-timeCSL logicZeno paths

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (25)

Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey ⋮ Bisimulation for Feller-Dynkin processes ⋮ Towards a classification of behavioural equivalences in continuous-time Markov processes ⋮ The Hennessy-Milner equivalence for continuous time stochastic logic with mu-operator ⋮ Comparative branching-time semantics for Markov chains ⋮ When are stochastic transition systems tameable? ⋮ Expressiveness of probabilistic modal logics: a gradual approach ⋮ When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ Bisimulations for non-deterministic labelled Markov processes ⋮ Behavioural equivalences for continuous-time Markov processes ⋮ Approximating Markov processes through filtration ⋮ Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains ⋮ Stochastic coalgebraic logic: bisimilarity and behavioral equivalence ⋮ Modular Markovian Logic ⋮ Equilibrium and termination II: the case of Petri nets ⋮ Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking ⋮ Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations ⋮ Probabilistic Model Checking for Energy-Utility Analysis ⋮ Compositional Design of Stochastic Timed Automata ⋮ Weak bisimulation is sound and complete for pCTL\(^*\) ⋮ Bisimulation and cocongruence for probabilistic systems ⋮ Kleisli morphisms and randomized congruences for the Giry monad ⋮ Logical characterization of fluid equivalences ⋮ Model checking for performability ⋮ Bisimulation and Simulation Relations for Markov Chains

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bisimulation for labelled Markov processes
• Real Analysis and Probability
• A Compositional Approach to Performance Modelling
• Introdction to Measure and Probability
• Model-checking continuous-time Markov chains

This page was built for publication: Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.