For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Probabilistic Model Checking of the One-Dimensional Ising Model
Toshifusa SEKIZAWA Tatsuhiro TSUCHIYA Koichi TAKAHASHI Tohru KIKUNO
IEICE TRANSACTIONS on Information and Systems
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
verification, probabilistic model checking, the Ising model, Discrete Time Markov Chain,
Full Text: PDF>>
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.