Probabilistic Model Checking of the One-Dimensional Ising Model

Toshifusa SEKIZAWA  Tatsuhiro TSUCHIYA  Koichi TAKAHASHI  Tohru KIKUNO 

Publication
IEICE TRANSACTIONS on Information and Systems  Vol.E92-D  No.5  pp.1003-1011
Publication Date: 2009/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
verification,  probabilistic model checking,  the Ising model,  Discrete Time Markov Chain, 

Full Text: PDF(705.5KB)

Summary: 
Probabilistic model checking is an emerging verification technology for probabilistic analysis. Its use has been started not only in computer science but also in interdisciplinary fields. In this paper, we show that probabilistic model checking allows one to analyze the magnetic behaviors of the one-dimensional Ising model, which describes physical phenomena of magnets. The Ising model consists of elementary objects called spins and its dynamics is often represented as the Metropolis method. To analyze the Ising model with probabilistic model checking, we build Discrete Time Markov Chain (DTMC) models that represent the behavior of the Ising model. Two representative physical quantities, i.e., energy and magnetization, are focused on. To assess these quantities using model checking, we devise formulas in Probabilistic real time Computation Tree Logic (PCTL) that represent the quantities. To demonstrate the feasibility of the proposed approach, we show the results of an experiment using the PRISM model checker.