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

---

Simulation Problems Over One-Counter Nets

Piotr Hofman ; Slawomir Lasota ; Richard Mayr ; Patrick Totzke.

One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN are&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;]

---