Search

• < Previous
• 1
• Next >

---

Priced Timed Petri Nets

Richard M. Mayr ; Parosh Aziz Abdulla.

We consider priced timed Petri nets, i.e., unbounded Petri nets where each token carries a real-valued clock. Transition arcs are labeled with time intervals, which specify constraints on the ages of tokens. Furthermore, our cost model assigns token storage costs per time unit to places, and firing&nbsp;[&hellip;]

---

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

---

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

---

Efficient reduction of nondeterministic automata with application to language inclusion testing

Lorenzo Clemente ; Richard Mayr.

We present efficient algorithms to reduce the size of nondeterministic B\"uchi word automata (NBA) and nondeterministic finite word automata (NFA), while retaining their languages. Additionally, we describe methods to solve PSPACE-complete automata problems like language universality, equivalence,&nbsp;[&hellip;]

---

Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs

Richard Mayr ; Eric Munday.

We study countably infinite Markov decision processes (MDPs) with real-valued transition rewards. Every infinite run induces the following sequences of payoffs: 1. Point payoff (the sequence of directly seen transition rewards), 2. Mean payoff (the sequence of the sums of all rewards so far, divided&nbsp;[&hellip;]

---