Search

• < Previous
• 1
• Next >

---

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;]

---

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;]

---

Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy

Benjamin Bisping ; David N. Jansen ; Uwe Nestmann.

We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes. We identify the relevant dimensions that measure&nbsp;[&hellip;]

---