JAIST Repository
https://dspace.jaist.ac.jp/Title

A Case Study : Analyzing the One Dimensional
Ising Model by Probabilistic Model Checking

Author(s)Sekizawa, Toshifusa; Tsuchiya, Tatsuhiro; Kikuno,Tohru; Takahashi, Koichi

CitationIssue Date

2008‑03‑03

TypePresentation

Text version

publisher

URL

http://hdl.handle.net/10119/8291

RightsDescription

5th VERITE : JAIST/TRUST‑AIST/CVS joint workshop
on VERIfication TEchnologyでの発表資料, 開催：2008年3月3日, 開催場所：北陸先端科学技術大学院
大学・情報科学研究科棟 5F コラボレーションルーム
７, JAIST 21世紀COEシンポジウム 2008「検証進化可能電子社会」と共催

Japan Advanced Institute of Science and Technology

A Case Study:
Analyzing the One Dimensional Ising Modelby Probabilistic Model Checking
Toshifusa Sekizawa1,2, Tatsuhiro Tsuchiya2,Tohru Kikuno2, and Koichi Takahashi1
1: National Institute of Advanced Industrial Science and Technology (AIST),
Research Center for Verification and Semantics (CVS).
2: Graduate School of Information Science and Technology, Osaka University.
March 3, 2008
March 3, 2008

5th VERITE

1

Proposed Method• Analyzing the Ising modelusing probabilistic model checking.
As an example, we analyze
physical phenomena of the 1D Ising model.
simulation

model checking

experimentsmathematical model
theoretical analysis
physical phenomena
March 3, 2008

5th VERITE2

Outline• The Ising model• Probabilistic Model Checking• Discussion

March 3, 2008

5th VERITE

3

The Ising model
The Ising model is:• a simplified model for magnets.
• G = (S, E)– spin S = (s1, s2, …), si = +1, -1
elementary microscopic objects.
s = +1 represents up, and s = -1 represents down.

– energy E
macroscopic physical quantity.

March 3, 2008

5th VERITE

4

The one dimensional Ising model
The 1D Ising model has:
• n spins, s1, s2, …, sn, located on a line in order.
• boundary condition sn+1 = s1.
• interactions restricted to nearby spins (si, si+1).
• energy• physical quantity– magnetizationsn
March 3, 2008

5th VERITE

s1

s2
5

Random spin flipping
1.
2.

3.

4.

Choose a spin randomly.
Fix other spinsand evaluate the energy
difference, whereandIf, the spin flipping is accepted. Otherwise
accepted with probability, where T istemperature.
Repeat steps 1 to 3 sufficient number of times.
E(s1, ..., si, ..., sn)
s1s2...

si...

sn

accepted?
E(s1, ..., si’, ..., sn)

s1March 3, 2008

s2...

si’...

sn
5th VERITE

6

Behaviour of the Ising model
We consider• neighbourhood of equilibrium
where energy E0 = -n, and magnetization M0 = 0 atequilibrium.
neighbourhood ofequilibrium
time
March 3, 2008

5th VERITE

7

Outline• The Ising model• Probabilistic Model Checking• Discussion

March 3, 2008

5th VERITE

8

Probabilistic model checking
A formal technique of verification.
• Input– a finite transition system (model)(DTMC: Discrete Time Markov Chain)– a property(PCTL: Probabilistic real time Computation Tree Logic)• Output– true / false

model checker: PRISM
model(n = 10)
property

March 3, 2008

true / false(1024 states, 11142 transitions)

5th VERITE

9DTMC (Discrete Time Markov Chain)

March 3, 2008

5th VERITE

10

PCTL
PCTL (Probabilistic real time Computation Tree Logic) is a
probabilistic extension of the temporal logic CTL.
[H. Hanson, et al. Formal Asp. Comput. 1994]• Syntax:•Semantics(*snip*)March 3, 2008

5th VERITE

11

Examples of DTMC + PCTL0.50.51.0p• “The probability of reaching a state where p holds
within 10 steps is greater than 0.3.”• “A state where p holds is reachable (withprobability 100%).”March 3, 2008

5th VERITE

12PRISM
Probabilistic Symbolic Model Checker[http://www.prismmodelchecker.org/]• input– a DTMC model– a property• PCTL formula• calculating probability• (transition) rewards• output– true / false, probability, value of expected rewards

March 3, 2008

5th VERITE

13

Modelling
Modelling the 1D Ising model• 10 spins, s1, …, s10, located on a line in order.
• interaction coefficient J = -1 (anti-ferromagnetic).
• boundary condition s11 = s1.
• temperature T is constant in a model.
• transition rule is the random spin flipping.
• each transition has value of reward 1.
• energy• magnetization
March 3, 2008

5th VERITE

14

Properties verified“equilibrium is reachable from arbitrary state,after reaching equilibrium,
the system stays in neighbourhood of equilibrium
within 100 times of spin flipping with probability
more than 70%.”

March 3, 2008

5th VERITE15

Outline• The Ising model• Probabilistic Model Checking• Discussion

March 3, 2008

5th VERITE

16

Discussion
Probabilistic model checking and Computer simulation:• probabilistic model checking
based on exhaustive search.
– advantage: formal definitions, reusability of models.
– disadvantage: unsuitable to verify time dependency.

• computer simulation
based on evaluation along time series.
– advantage: suitable for statistic analysis.
– disadvantage: unsuitable for formal methods.

March 3, 2008

5th VERITE

17

Conclusion
Probabilistic model checking• is useful to analyze the (1D) Ising model.
• will be able to cooperate with computer
simulation.

March 3, 2008

5th VERITE

18

Future work• Solving the state explosion problem.
– abstraction, symmetry reduction, etc.

• Analyzing the 2D Ising model.
– more practical problems such as phasetransition.

• Analyzing other probabilistic systems.
– genetic algorithm, etc.

March 3, 2008

5th VERITE

19

(end of slides)

March 3, 2008

5th VERITE

20

This presentation is based on:T. Sekizawa, T. Tsuchiya, T. Kikuno, and K. Takahashi,“Analyzing the One Dimensional Ising Model byProbabilistic Model Checking”,
Proceedings of the IASTED Asian Conference on Modellingand Simulation, pp.199-204, ACTA Press, October 2007.

March 3, 2008

5th VERITE

21