Probabilistic analysis for state reachability of wireless lossy channel systems

In this paper we perform some probabilistic analysis on state reachabilities of wireless lossy channel systems (WLCS) using Continuous Stochastic Logic (CSL) for Quasi Birth-Death model (QBD). To study WLCS in a continuous time setting, we first extend Probabilistic Lossy Channel Systems (PLCS) towards WLCS. We show that the state set S⁰ is an attractor of WLCS model, and discuss the accumulated steady-state probabilistic reachability and the transient probabilistic reachability for WLCS. The results from the case study of WLCS show the versatility of our analytical technique and our works lead to a significantly analysis foundation where the underlying communication medium is lossy.