8 citations · 22 across the 17 of their papers we have counts for
4 papers · 1 filter
The Complexity of Flat Freeze LTL
Benedikt Bollig, Karin Quaas, Arnaud Sangnier
We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter…
How hard is it to verify flat affine counter systems with the finite monoid property ?
Radu Iosif, Arnaud Sangnier
We study several decision problems for counter systems with guards defined by convex polyhedra and updates defined by affine transformations. In general, the reachability problem i…
Reachability in Networks of Register Protocols under Stochastic Schedulers
Patricia Bouyer, Nicolas Markey, Mickael Randour +2
We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol…
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…