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

×

Now Offering a 50% Discount When a Minimum of Five Titles in Related Subject Areas are Purchased TogetherAlso, receive free worldwide shipping on orders over US$ 395.(This offer will be automatically applied upon checkout and is applicable to print & digital publications)Browse Titles

Receive a 50% Discount When a Minimum of Five Titles are Purchased Together

This 50% discount is automatically applied upon checkout and is only applicable when five or more reference books and scholarly journals are ordered. Discount valid on purchases made directly through IGI Global’s Online Bookstore (www.igi-global.com) and cannot be combined with any other discount. It may not be used by distributors or book sellers and the offer does not apply to databases. Exclusions of select titles may apply.

IGI Global Converts Over 30+ Journals to Full Gold Open Access (OA)

With access to digital resources and OA content being critical during this time, IGI Global has converted 30 journals to full Gold OA. IGI Global OA provides a quality, expediate, high-quality OA publishing process, flexible funding options, and more, which allows researchers to benefit from freely and immediately sharing their peer-reviewed research with the world.

Additional Source of OA Funding When Your Institution Invests in IGI Global’s e-Collections

When an institution invests in IGI Global’s e-Book and/or e-Journal Collections, IGI Global will match the library’s investment with a fund of equal value to go toward subsidizing the OA article processing charges (APCs) for faculty at that institution when their work is submitted and accepted under OA (following peer review) into an IGI Global journal.

Based on the increased interest in our Research Anthologies line from last year and understanding current budgetary limitations, IGI Global is reducing the price of our multi-volume Research Anthologies up to 50%. These publications are ideal for accommodating library budgets, as they contain hand-selected research content of the highest quality.

Receive Complimentary Electronic Access to the First, Second, Third, and Fourth Edition of the Encyclopedia of Information Science and Technology with the Purchase of the Fifth Edition

For a limited time, receive the complimentary e-books for the first, second, third, and fourth editions with the purchase of the Encyclopedia of Information Science and Technology, Fifth Edition e-book*. Offer is only valid when purchasing the fifth edition’s hardcover + e-book or e-book only option directly through IGI Global’s Online Bookstore (www.igi-global.com/books) and is not intended for use by book distributors or wholesalers. Contact Customer Service, cust@igi-global.com, for details. Offer expires July 1, 2021.

Offering a 5% Pre-Publication Discount on All Reference Books Ordered Through IGI Global’s Online Bookstore*

To support customers with accessing the latest research, IGI Global is offering a 5% pre-publication discount on all hardcover, softcover, e-books, and hardcover + e-books titles. *5% discount offer is eligible on hardcover, softcover, e-books, and hardcover + e-books titles and is automatically applied directly to the shopping cart. Discount offer only valid on purchases made directly through IGI Global’s Online Bookstore and offer expires 30 days after the publication’s release. This automatic discount is not intended for use by book distributors or wholesalers.

Free shipping will be automatically applied to shopping cart orders over US$ 395.00 or more before tax, which can include a combination of print and non-shippable products (i.e. e-books, e-journals, and articles/chapters). It is only available when you order directly through IGI Global’s Online Bookstore and is only valid on standard U.S. and international shipping. There will be additional charges for express shipping and limitations may apply.

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 e-Book and e-Journal Collections.

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

APA

O. Hasan, & S. Tahar (2015). Classified Discrete-Time Markov Chains. IGI Global. http://doi:10.4018/978-1-4666-8315-0.ch007

Chicago

Osman Hasan , and Sofiène Tahar. "Classified Discrete-Time Markov Chains." In Formalized Probability Theory and Applications Using Theorem Proving. Hershey, PA: IGI Global, 2015. http://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.