Solution (source code)

= Solution

First consider an <M-M-K queue> with $K$ servers, arrival rate $\lambda$, and service rate $\beta$ at each server. Assume $\lambda<K\beta$ so that a <stationary distribution> exists. Its population is a <birth-death process> with rates $q_{n,n+1}=\lambda$ and $q_{n,n-1}=\beta\min(n,K)$. The equilibrium probabilities satisfy <detailed balance>
$$
\pi_n\lambda=\pi_{n+1}\beta\min(n+1,K).
$$
Thus the population process is a <reversible Markov chain>. In its <time reversal of a continuous-time Markov chain>, forward departures become upward jumps whose rate is the constant $\lambda$, <independent> of the state. They can be generated by a rate-$\lambda$ <Poisson process> <independent> of the initial reversed state. Reversing time preserves the <Poisson process> law, proving \b[the equilibrium departure process is Poisson with rate $\lambda$], the <Burke theorem for a multi-server queue>.

The same argument gives the departure component of <quasireversibility> needed for the tandem calculation: \b[the present upstream population is <independent> of its entire past departure process]. Indeed, these departures become future arrivals in the reversed chain, <independent> of its initial population. First check this on finite time windows, then extend to the full past. A Poisson output alone, without this <independence>, would not justify multiplying queue-empty probabilities.

Now let $a=\nu\mu$, where $\mu$ denotes the mean service time at passport control, so the service rate at each of its two servers is $1/\mu$. The <stationary distribution> of the <M-M-s queue> with $s=2$ has normalizing sum
$$
\pi_0^{-1}=1+a+\frac{a^2}{2}\sum_{k=0}^\infty(a/2)^k
=\frac{2+a}{2-a}.
$$
Hence its empty probability is $(2-a)/(2+a)$. Its output feeds a stable <M D 1 queue> with rate $\nu$ and deterministic service time $\tau$. In a stationary work-conserving single-server queue, the busy fraction is the rate of completed work, $\nu\tau$, so the empty probability is $1-\nu\tau$.

The downstream stationary workload is a causal function of past upstream departures. For example, it is the limit of workloads constructed from arrivals in increasingly long finite past intervals; stability makes this stationary construction well defined. The backward <independence> just proved therefore makes the two present queue populations <independent>. Consequently
$$
\boxed{\mathbb P(\text{both queues empty})=\frac{2-\nu\mu}{2+\nu\mu}(1-\nu\tau).}
$$

With walking time $\sigma$, the downstream arrival stream is the upstream departure stream shifted by $\sigma$. Its present workload depends only on departures up to time $-\sigma$. The number walking at time zero is the number of departures in $(-\sigma,0]$, which has <Poisson distribution> of mean $\nu\sigma$ and is <independent> of the earlier departures. The upstream present population is <independent> of both parts of its past departure stream. Thus the three empty events factor, giving
$$
\boxed{\mathbb P(\text{both queues empty and none walking})=\frac{2-\nu\mu}{2+\nu\mu}(1-\nu\tau)e^{-\nu\sigma}.}
$$
The factor $e^{-\nu\sigma}$ is the empty probability of the deterministic-travel infinite-server stage. Both printed stability inequalities ensure the stationary calculations apply.