Availability Analysis of IaaS Cloud Using Analytic Models availability of an Internet distributed system. Analytic models described in this chapter can perhaps be combined with the statistical models proposed by Javadi et al. In (Uemura, Dohi, & Kaio, 2009), Uemura et al. used discrete time semi-Markov process to describe the stochastic behavior of a scalable intrusion tolerant system. In contrast, for Cloud availability analysis, the chapter starts with Petri net (PN) based models, to facilitate automated generation of Markov chains and subsequently decompose the large PN model into small PNs and eventually to Markov chains. In (Chen, Zhou, & Xiong, 2010) Chen et al. used a deterministic and stochastic PN method to il- lustrate the performance of producer/consumer based application models in Cloud context. Unlike the approach proposed here, they focus only on performance behavior of Cloud. In the previous work (Ghosh, Longo, Naik, & Trivedi, 2010), the authors showed an SRN modeling approach for be associated to the net transitions so that the stochastic process underlying a SPN is a CTMC. In generalized SPNs (GSPN) (Marsan, Balbo, & Conte, 1984), transitions are allowed to be either timed (exponentially distributed firing time, drawn as rectangular boxes) or immediate (zero firing time, represented by thin black bars). Immediate transitions always have priority over timed transi- tions and if both timed and immediate transitions are enabled in a marking then timed transitions are treated as if they were not enabled. If several immediate transitions compete for firing, a speci- fied probability mass function is used to break the tie. A marking of a GSPN is called vanishing if at least one immediate transition is enabled in it. A marking is called tangible otherwise. GSPN also introduces the concept of inhibitor arc (rep- resented by a small hollow circle at the end of the arc) which connects a place to a transition. A transition with an inhibitor arc cannot fire if