T. Sekizawa, T. Tsuchiya, T. Kikuno, and K. Takahashi
Verification, Probabilistic Model Checking, the Ising Model, Discrete Time Markov Chain.
Probabilistic model checking is an emerging verification technology for probabilistic analysis. It has started being used not only in the computer science field but also in in terdisciplinary fields. In this paper, we show that prob abilistic model checking allows one to analyze magnetic behaviours of the one dimensional Ising model which de scribes physical phenomena of magnets. The Ising model consists of elementary microscopic objects called spins and is often statically analyzed using the Metropolis method. Spins are microscopic elements, while the interesting prop erties to be measured are macroscopic physical quantities such as the energy. To analyze the Ising model with prob abilistic model checking, we build labelled Discrete Time Markov Chain (DTMC) models in which states represent spins and macroscopic physical quantities and transitions occur according to the Metropolis method. Two represen tative physical quantities, energy and magnetization, are fo cused on. We use PRISM, a probabilistic model checker, to assess these quantities. To this end, we provide specifica tions expressed in PCTL (Probabilistic real time Computa tion Tree Logic) to instruct PRISM to compute the quanti ties.
Important Links:
Go Back
