Susanna Donatelli
Università di Torino, Italy
Title: Markov regenerative processes solution and stochastic model checking: an on-the-fly approach
Abstract:
Stochastic model checking is a technique to check if a Markov chain satisfies a path property. This typically requires the computation of the probability of the set of paths of the continous Time Markov chain (CTMC) that satisfy a given set of requirements that are given in terms of visited states, events occurrence and time constraints at which the events occur. In particular we shall address the stochastic logic , in which the properties to be satisfied are specified as one-clock timed automata. It has been proved that the check of a
property requires the solution of a Markov Regenerative Process (MRgP) of a size that is of the order of the size of the CTMC multiplied by the size of the timed automata state space: space and time can be a severe impairement of the efficacy of stochastic model checking. In this talk we shall review recent techniques for MRgP solution and standard techniques for the state space construction of timed automata, to show how they can work in a synergic manner to devise a model checking algorithm for
that works on components (to save time), and that is able to build the components on-the-fly, only when needed (to save space). We shall finally show how the whole technique has been implemented and how it can be accessed through the GreatSPN tool, a tool for the solution and analysis of (stochastic) Petri nets.
Dieter Fiems
Ghent University, Belgium
Title: Data-driven appointment scheduling
Abstract:
We consider the problem of evaluating and constructing appointment schedules for patients in a health-care facility where a single physician treats patients in consecutive order, as is common for general practitioners, clinics and for outpatients in hospitals. Specifically, given a fixed-length session during which a physician sees K patients, each patient has to be given an appointment time during this session in advance. Optimising a schedule with respect to patient waiting times, physician idle times, session overtime, etc. usually requires a heuristic search method involving a huge number of repeated schedule evaluations. Methods for lowering the computational cost of obtaining accurate predictions is the main thread of this talk.
Borrowing from queueing theory, we first show that a Lindley-type recursion in a discrete-time framework can be used to obtain accurate predictions for the moments of the patient waiting times and the doctor’s idle times and overtime in the simplest setting where patients are identical, punctual and always show up. Unfortunately, in realistic scenarios, patients are neither statistically identical (in many scenarios, the consultation times of particular patients can be estimated based on the lengths of prior consultations of the same patient or of patients with similar conditions) nor punctual and a considerable number of patients do not show up. Various extensions to evaluate schedules with unpunctuality and no-shows are discussed, both completely numerical methods as well as methods which combine numerical results and Monte-Carlo simulation. The evaluation methods are then used in combination with a local search algorithm to optimise the schedule.
Finally, noting that it is often beneficial to be scheduled early during a session, we consider an appointment game in which patients can opt to be seen in a later session, as to reduce their waiting during the session. Both the unobservable and observable game are considered, i.e., the patients are either aware of the number of patients already scheduled in the future sessions, or they are not.
Uri Yechiali
Tel Aviv University, Israel
Title: Tandem stochastic systems: Jackson networks, asymmetric exclusion processes, asymmetric inclusion processes and catalan numbers
Abstract:
A tandem stochastic system is a network of n sites (queues) in series, where particles (customers, jobs, packets, etc.) move uni-directionally from one site to the next until they leave the system. When each site is an M/M/1 queue, where the buffer size of each site is unlimited but only single particles can move between sites, the system is known as Tandem Jackson Network (TJN). The TJN is famous for its product-form solution of the multi-dimensional distribution function of the sites’ queue-sizes (occupancies).
Another well-known tandem system is the Asymmetric Exclusion Process (ASEP), where each site can hold at most a single particle, a constraint that causes blockings on particles’ forward movements.
In contrast, the newly introduced (Reuveni, Eliazar and Yechiali)* Asymmetric Inclusion Process (ASIP) is a tandem series of sites, each with unbounded buffer capacity, and with unlimited-size batch service. That is, when service is completed at site k, all particles present there move simultaneously to site k+1 and form a cluster together with the cluster of particles (if any) already residing in site k+1.
We analyze the innovative ASIP network and show that its multi-dimensional Probability Generating Function (PGF) does not possess a product-form solution. Nevertheless, we present a method to calculate this PGF. Surprisingly though, the load (total number of particles up to site k) does possess a product-form solution. We consequently show that homogeneous systems (i.e. systems with identical servers) are optimal for various load-related objective functions.
Considering the total number of particles in a site-interval of length m (m=1,2,…,n) that start at site k, the corresponding probability distribution function generates a discrete two-dimensional boundary-value problem which we solve explicitly. It is further proved that the probability of site k being positively occupied is proportional to . Catalan’s numbers arise naturally in this context. Finally, we derive limit laws (when the number of sites becomes large) for various system’s variables. In particular, we show that the ‘load’, as well as the ‘draining time’, each obeys a Gaussian distribution (with corresponding coefficients), while the ‘inter-exit time’ follows a Rayleigh distribution.
*The presentation is based on joint works with S. Reuveni and I. Eliazar