Search

• < Previous
• 1
• Next >

---

Decisive Markov Chains

Parosh Aziz Abdulla ; Noomene Ben Henda ; Richard Mayr.

We consider qualitative and quantitative verification problems for infinite-state Markov chains. We call a Markov chain decisive w.r.t. a given set of target states F if it almost certainly eventually reaches either F or a state from which F can no longer be reached. While all finite Markov chains&nbsp;[&hellip;]

---

Stochastic Parity Games on Lossy Channel Systems

Parosh Aziz Abdulla ; Lorenzo Clemente ; Richard Mayr ; Sven Sandberg.

We give an algorithm for solving stochastic parity games with almost-sure winning conditions on {\it lossy channel systems}, under the constraint that both players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2 1/2-player games&nbsp;[&hellip;]

---

Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness

Parosh Abdulla ; Pritha Mahata ; Richard Mayr.

We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which each token is equipped with a real-valued clock and where the semantics is lazy (i.e., enabled transitions need not fire; time can pass and disable transitions). We consider the following verification problems for TPNs.&nbsp;[&hellip;]

---