TY - GEN
T1 - Probe automata for passage time specification
AU - Amparore, Elvio Gilberto
AU - Beccuti, Marco
AU - Donatelli, Susanna
AU - Franceschinis, Giuliana
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
KW - GSPN
KW - Markov chains
KW - passage time
UR - http://www.scopus.com/inward/record.url?scp=80055034486&partnerID=8YFLogxK
U2 - 10.1109/QEST.2011.20
DO - 10.1109/QEST.2011.20
M3 - Conference contribution
AN - SCOPUS:80055034486
SN - 9780769544915
T3 - Proceedings of the 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011
SP - 101
EP - 110
BT - Proceedings of the 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011
T2 - 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011
Y2 - 5 September 2011 through 8 September 2011
ER -