Name
Abstract | ||
|---|---|---|
Markov chains are extensively used in the modeling and analysis of engineering and scientific problems. Usually, paper-and-pencil proofs, simulation or computer algebra software are used to analyze Markovian models. However, these techniques either are not scalable or do not guarantee accurate results, which are vital in safety-critical systems. Probabilistic model checking has been proposed to formally analyze Markovian systems, but it suffers from the inherent state-explosion problem and unacceptable long computation times. Higher-order-logic theorem proving has been recently used to overcome the above-mentioned limitations but it lacks any support for discrete Birth-Death process and Independent and Identically Distributed (IID) random process, which are frequently used in many system analysis problems. In this paper, we formalize these notions using formal Discrete-Time Markov Chains (DTMC) with finite state-space and classified DTMCs in higher-order logic theorem proving. To demonstrate the usefulness of the formalizations, we present the formal performance analysis of two software applications. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/SYSCON.2017.7934785 | 2017 Annual IEEE International Systems Conference (SysCon) |
Keywords | Field | DocType |
formal performance analysis,software applications,finite state-space,DTMC,formal Discrete-Time Markov Chains,system analysis problems,independent and identically distributed random process,higher order logic theorem proving,state-explosion problem,Markovian systems,probabilistic model checking,safety-critical systems,Markovian model analysis,computer algebra software,paper-and-pencil proofs,Markov chains,higher order logic,IID process,Birth-Death process | Markov process,Computer science,Automated theorem proving,Markov chain,Stochastic process,Symbolic computation,Theoretical computer science,Mathematical proof,Independent and identically distributed random variables,Higher-order logic | Conference |
ISSN | ISBN | Citations |
1944-7620 | 978-1-5090-4624-9 | 0 |
PageRank | References | Authors |
0.34 | 6 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Liya Liu | 1 | 0 | 0.34 |
| Osman Hasan | 2 | 401 | 60.79 |
| Sofiène Tahar | 3 | 915 | 110.41 |