On-the-fly model checking for extended action-based probabilistic operators | Publicación