Reseña: On the formalization of continuous-time Markov chains in HOL
Se ha publicado un trabajo de razonamiento formalizado en HOL4 titulado On the formalization of continuous-time Markov chains in HOL.
Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Concordia University, Montreal, Canadá).
Su resumen es
Continuous-time Markov chain has been extensively applied to model diverse real-world systems. The analysis of these systems has been conducted using conventional simulation technique and computer algebra systems, more recently, probabilistic model checking. However, these methods either cannot guarantee accurate analysis or are not scalable due to the unacceptable computation consumption. As a complemental technique, theorem proving is proposed to reason about continuous-time Markov chain using HOL theorem proving. To our best knowledge, the formalization of continuous-time Markov chain has not been found in any theorem prover. In this report, we provide the idea on the formal definition of continuous-time Markov chain and two of its formally verified properties as the first step to formalize the continuous-time Markov chain theory. Also, we present the next step and the predict the potential challenges in the formalization process. Finally, a certain of applications are listed to be targeted using the formalized continuous-time Markov chain.