Probe automata for passage time specification

Passage time distribution has drawn increasing attention over the past years as an important measure to define and verify service level agreements. The definition of passage time requires the specification of a condition to start/stop the computation, and possibly of a restriction on the system behavior to be considered between start and stop. Different characterizations have been defined in the past, either state-based, action-based or a mix of the two, either for Markov chains, or for stochastic Petri nets and process algebras. In this paper we propose probe automata as a way to specify passage time for GSPNs that allows one to select entering, goal, and forbidden states, as well as paths of interest starting from any reachable state. The specification is in terms of conditions over the current marking, the transition (sequence) being fired, as well as over the marking reached through the firing. Probe automata subsume previous definitions of passage time for GSPNs and for Tagged GSPNs, the extension of GSPNs that was defined in the past for computing passage time of a tagged token in a GSPN.