52 citations · 206 across the 25 of their papers we have counts for
4 papers · 1 filter
Model Checking Flat Freeze LTL on One-Counter Automata
Antonia Lechner, Richard Mayr, Joël Ouaknine +2
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-coun…
Simulation Problems Over One-Counter Nets
Piotr Hofman, Slawomir Lasota, Richard Mayr +1
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…
Qualitative Analysis of VASS-Induced MDPs
Parosh Aziz Abdulla, Radu Ciobanu, Richard Mayr +2
We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are…
Reduction of Nondeterministic Tree Automata
Ricardo Almeida, Lukáš Holík, Richard Mayr
We present an efficient algorithm to reduce the size of nondeterministic tree automata, while retaining their language. It is based on new transition pruning techniques, and quotie…