The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
La vérification de modèle probabiliste est une technologie de vérification émergente pour l'analyse probabiliste. Son utilisation a commencé non seulement en informatique mais également dans des domaines interdisciplinaires. Dans cet article, nous montrons que la vérification de modèles probabilistes permet d'analyser les comportements magnétiques du modèle d'Ising unidimensionnel, qui décrit les phénomènes physiques des aimants. Le modèle d'Ising est constitué d'objets élémentaires appelés spins et sa dynamique est souvent représentée par la méthode Metropolis. Pour analyser le modèle d'Ising avec une vérification de modèle probabiliste, nous construisons des modèles de chaîne de Markov à temps discret (DTMC) qui représentent le comportement du modèle d'Ising. Deux grandeurs physiques représentatives, à savoir l'énergie et la magnétisation, sont étudiées. Pour évaluer ces quantités à l'aide de la vérification de modèle, nous concevons des formules en logique d'arbre de calcul probabiliste en temps réel (PCTL) qui représentent les quantités. Pour démontrer la faisabilité de l'approche proposée, nous montrons les résultats d'une expérience utilisant le vérificateur de modèle PRISM.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Toshifusa SEKIZAWA, Tatsuhiro TSUCHIYA, Koichi TAKAHASHI, Tohru KIKUNO, "Probabilistic Model Checking of the One-Dimensional Ising Model" in IEICE TRANSACTIONS on Information,
vol. E92-D, no. 5, pp. 1003-1011, May 2009, doi: 10.1587/transinf.E92.D.1003.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E92.D.1003/_p
Copier
@ARTICLE{e92-d_5_1003,
author={Toshifusa SEKIZAWA, Tatsuhiro TSUCHIYA, Koichi TAKAHASHI, Tohru KIKUNO, },
journal={IEICE TRANSACTIONS on Information},
title={Probabilistic Model Checking of the One-Dimensional Ising Model},
year={2009},
volume={E92-D},
number={5},
pages={1003-1011},
abstract={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.},
keywords={},
doi={10.1587/transinf.E92.D.1003},
ISSN={1745-1361},
month={May},}
Copier
TY - JOUR
TI - Probabilistic Model Checking of the One-Dimensional Ising Model
T2 - IEICE TRANSACTIONS on Information
SP - 1003
EP - 1011
AU - Toshifusa SEKIZAWA
AU - Tatsuhiro TSUCHIYA
AU - Koichi TAKAHASHI
AU - Tohru KIKUNO
PY - 2009
DO - 10.1587/transinf.E92.D.1003
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E92-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2009
AB - 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.
ER -