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

You are using a new version of the IGI Global website.
If you experience a problem, submit a ticket to
helpdesk@igi-global.com,
and continue your work on the old website.

×

Receive a 20% Discount on All Titles Ordered Through IGI Global's Online Bookstore Including All Electronic Resources
Ideal for Online Learning Environments During the COVID-19 Pandemic View All Titles

Receive a 20% Discount All Titles Ordered Through IGI Global’s Online Bookstore Including All Electronic Resources

Hosted on IGI Global’s advanced InfoSci platform, IGI Global’s electronic resources are available with no embargo of content, unlimited simultaneous users with no additional charge, and no maintenance fees with remote access options available for your institution, making them ideal for online learning environments during the COVID-19 pandemic.

Convert Your IGI Global Print Holdings to Electronic Format through IGI Global’s InfoSci® Platform or ProQuest’s E-Book Central Platform

To assist you during the COVID-19 pandemic, IGI Global will convert libraries previously acquired print holdings to electronic formats directly through our InfoSci® platform or ProQuest’s E-Book Central platform at a 50% discount. Send us a list of IGI Global publications you would like to convert, and we’ll promptly facilitate the set-up and access.

View Over 900+ IGI Global Titles Related to COVID-19 Pandemic

IGI Global offers a rich volume of content related to treatment, mitigation, and emergency and disaster preparedness surrounding epidemics and pandemics such as COVID-19. All of these titles are available in electronic format at a 20% discount making them ideal resources for online learning environments.

New Product! InfoSci-Knowledge Solutions Databases

IGI Global is now offering a new collection of InfoSci-Knowledge Solutions databases, which allow institutions to affordably acquire a diverse, rich collection of peer-reviewed e-books and scholarly e-journals. Ideal for subject librarians, these databases span major subject areas including business, computer science, education, and social sciences.

Acquire a Source of Open Access (OA) APC Funding for Your Institution Through IGI Global's OA Fee Waiver (Offset Model) Initiative

For any library that invests in IGI Global's InfoSci-Books and/or InfoSci-Journals databases, IGI Global will match the library’s investment with a fund of equal value to go toward subsidizing the OA APCs for their faculty patrons when their work is submitted/accepted under OA into an IGI Global journal.

Create a Free IGI Global Library Account to Receive an Additional 5% Discount on All Purchases

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

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. 28 Mar. 2020. 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 March 28, 2020. 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.