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 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
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
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
Antonia Lechner ; Richard Mayr ; Joël Ouaknine ; Amaury Pouly ; James Worrell.
Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in general and PSPACE-complete for the special case of […]
Published on December 7, 2018
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 […]
Published on March 6, 2023