Timed reachability on queuing networks?

Anne Remke (Univ. of Twente)

 

Abstract:

 Jackson queuing networks are a quite general class of queuing
networks, that can be applied in a various number of settings. Their
underlying state space is highly structured, however in multiple
dimensions, depending on the number of queues. For only one queue the
underlying state space is just a very simple QBD.  Recently, we
extended CSL model checking towards QBDs. Model checking this infinite
model class is feasible due to the structure of QBDs.

We discuss whether model checking the class of Jackson queuing
networks is possible. We derive the underlying CTMC and discuss
several state-space representations. Steady-state analysis on Jackson
QNs is already well kown. Transient analysis on Jackson QNs is
possible using uniformization with representatives . Currently we try
to merge this to a framework for timed reachability on Jackson QNs.