Classified Discrete-Time Markov Chains: Computer Science & IT Book Chapter | IGI Global

×

Receive a 20% Discount on All Purchases Directly Through IGI Global's Online Bookstore.
Additionally, libraries can receive an extra 5% discount. Learn More

Subscribe to the latest research through IGI Global's new InfoSci-OnDemand Plus

InfoSci®-OnDemand Plus, a subscription-based service, provides researchers the ability to access full-text content from over 93,000+ peer-reviewed book chapters and 24,000+ scholarly journal articles covering 11 core subjects. Users can select articles or chapters that meet their interests and gain access to the full content permanently in their personal online InfoSci-OnDemand Plus library.

Purchase the Encyclopedia of Information Science and Technology, Fourth Edition and Receive Complimentary E-Books of Previous Editions

When ordering directly through IGI Global's Online Bookstore, receive the complimentary e-books for the first, second, and third editions with the purchase of the Encyclopedia of Information Science and Technology, Fourth Edition e-book.

Create a Free IGI Global Library Account to Receive a 25% Discount on All Purchases

Exclusive benefits include one-click shopping, flexible payment options, free COUNTER 4 and MARC records, and a 25% discount on all titles as well as the award-winning InfoSci^{®}-Databases.

InfoSci^{®}-Journals Annual Subscription Price for New Customers: As Low As US$ 4,080*

This collection of over 185 e-journals offers unlimited access to highly-cited, forward-thinking content in full-text PDF and HTML with no DRM. There are no platform or maintenance fees and a guarantee of no more than 5% increase annually.

Hasan, Osman and Sofiène Tahar. "Classified Discrete-Time Markov Chains." Formalized Probability Theory and Applications Using Theorem Proving. IGI Global, 2015. 87-115. Web. 22 Jan. 2019. doi:10.4018/978-1-4666-8315-0.ch007

APA

Hasan, O., & Tahar, S. (2015). Classified Discrete-Time Markov Chains. In Formalized Probability Theory and Applications Using Theorem Proving (pp. 87-115). Hershey, PA: IGI Global. doi:10.4018/978-1-4666-8315-0.ch007

Chicago

Hasan, Osman and Sofiène Tahar. "Classified Discrete-Time Markov Chains." In Formalized Probability Theory and Applications Using Theorem Proving, 87-115 (2015), accessed January 22, 2019. doi:10.4018/978-1-4666-8315-0.ch007

The main focus of this chapter is on the formalization of classified DTMCs. The chapter begins by presenting the formalization of some foundational notions of classified states, which are categorized based on reachability, periodicity, or absorbing features. Then, these results along with the formal definition of a DTMC, presented in the previous chapter, are used to formalize classified Markov chains, such as aperiodic and irreducible DTMCs. Based on these concepts, some long-term properties are verified for the purpose of formally checking the correctness of the functions of Markovian systems or analyzing the performance of Markov chain models.

The foremost concept of states classification is the first passage time τj, which is sometimes referred to as the first hitting time. It is defined as the minimum time required to reach a state j from the initial state i:

τj = min { t > 0: Xt = j }(7.1)

The first passage time can be defined in HOL4 as:

Definition 7.1

Ⱶ ∀ X x j. FPT X x j = MINSET { t | 0 < t ∧ (X t x = j) }

where X is a random process and x is a sample in the probability space associated with the random variable X_{t}. Note that the first passage time is also a random variable.

The conditional distribution of τj defined as the probability of the events starting from state i and visiting state j at time n is expressed as f_{ij}^{(n)} = Pr { τj = n | X_{0} = i }.

This definition can be formalized in HOL4 as (Liu, 2013):

Definition 7.2

Ⱶ ∀ X p i j n.
f X p i j n = prob p ({ x | FPT X x j = n } | { x | X 0 x = i })

Another important notion, denoted as f_{ij}, is the probability of the events starting from state i and visiting state j at all times n, is expressed as f_{ij} = f_{ij}^{(n)} . It can be expressed in HOL4 as (λ n. f X p i j n) sums f_{ij}. Thus f_{jj} provides the probability of events starting from state j and eventually returning back to j. If f_{jj} = 1, then the mean return time of state j is defined as μ_{j}= n f_{jj}^{(n)}. The existence of this infinite summation can be specified as summmable (λ n. n ∗ f X p j j n) in HOL.

A state j in a DTMC { X_{t} } _{t ≥ 0} is called transient if f_{jj} < 1, and persistent if f_{jj} = 1. If the mean return time μ_{j} of a persistent state j is finite, then j is said to be persistent non null state (or positive persistent state). Similarly, if μ_{j} is infinite, then j is termed as persistent null state.

The greatest common divisor (gcd) of a set is a frequently used mathematical concept in defining classified states. We formalize the gcd of a set as follows:

Definition 7.3

Ⱶ ∀A. GCD SET A = MAXSET { r | ∀x. x ∈A ⇒ divides r x }

where MAXSET is a function in the set theory of HOL4 such that MAXSET s defines the maximum element in the set s. A period of a state j is any n such that p_{jj}^{(n)}is greater than 0 and we write d_{j} = gcd { n: p_{jj}^{(n)} > 0 }as the gcd of the set of all periods.

A state i is said to be accessible from a state j (written i → j), if there exists a nonzero n-step transition probability of the events from state i to j. Two states i and j are called communicating states (written i ↔ j) if they are mutually accessible. A state j is an absorbing state if the one-step transition probability p_{jj} =1. The formalization of some other foundational notions of the classified states is given in Table 1.