6 results
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 […]
Published on March 14, 2016
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 […]
Published on November 8, 2007
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 […]
Published on November 12, 2013
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 […]
Published on January 5, 2015
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. […]
Published on February 7, 2007
Javier Esparza ; Antonin Kucera ; Richard Mayr.
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model […]
Published on March 7, 2006