Encyclopedia of Information Science and Technology, Fourth Edition (10 Volumes) Now 50% Off

Take 50% off when purchasing the Encyclopedia directly through IGI Global's Online Bookstore. Plus, 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,950

This collection of over 175 e-journals offers unlimited access to highly-cited, forward-thinking content in full-text PDF and XML 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. 19 Jun. 2018. 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 June 19, 2018. 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.