Search

• < Previous
• 1
• Next >

---

Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations

Lijun Zhang ; Holger Hermanns ; Friedrich Eisenbrand ; David N. Jansen.

Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. However, decision algorithms for strong and weak simulation over Markov chains, and for strong simulation&nbsp;[&hellip;]

---

Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song ; Lijun Zhang ; Jens Chr. Godskesen ; Flemming Nielson.

Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its&nbsp;[&hellip;]

---

Efficient CSL Model Checking Using Stratification

Lijun Zhang ; David N. Jansen ; Flemming Nielson ; Holger Hermanns.

For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential&nbsp;[&hellip;]

---