diff --git a/model-checking-book/example.go b/model-checking-book/example.go
new file mode 100644
index 0000000..06ab7d0
--- /dev/null
+++ b/model-checking-book/example.go
@@ -0,0 +1 @@
+package main
diff --git a/model-checking-book/go.mod b/model-checking-book/go.mod
new file mode 100644
index 0000000..13930f0
--- /dev/null
+++ b/model-checking-book/go.mod
@@ -0,0 +1,3 @@
+module github.com/uta8a/playground/model-checking-book
+
+go 1.23.4
diff --git a/model-checking-book/kripke.go b/model-checking-book/kripke.go
new file mode 100644
index 0000000..8062599
--- /dev/null
+++ b/model-checking-book/kripke.go
@@ -0,0 +1,154 @@
+package main
+
+import (
+	"fmt"
+	"hash/fnv"
+	"sort"
+	"strings"
+)
+
+type kripkeModel struct {
+	worlds     worlds
+	initial    worldID
+	accessible map[worldID][]worldID
+}
+
+type worldID uint64
+type worlds map[worldID]world
+
+func (wlds worlds) member(wld world) bool {
+	_, ok := wlds[wld.id]
+	return ok
+}
+
+func (wlds worlds) insert(wld world) {
+	wlds[wld.id] = wld
+}
+
+type world struct {
+	id              worldID
+	environment     environment
+	programCounters map[procName][]statement
+}
+
+func NewWorld(env environment, counters map[procName][]statement) world {
+	id := id(env, counters)
+	return world{id: id, environment: env, programCounters: counters}
+}
+
+func id(env environment, counters map[procName][]statement) worldID {
+	strs := []string{}
+	vnames := []string{}
+
+	for name := range env.variables {
+		vnames = append(vnames, string(name))
+	}
+	sort.Strings(vnames)
+
+	for _, name := range vnames {
+		val := env.variables[varName(name)]
+		strs = append(strs, fmt.Sprintf("%s=%d", name, val))
+	}
+
+	pnames := []string{}
+	for name := range counters {
+		pnames = append(pnames, string(name))
+	}
+	sort.Strings(pnames)
+	for _, name := range pnames {
+		stmts := counters[procName(name)]
+		strs = append(strs, fmt.Sprintf("%s=%+v", name, stmts))
+	}
+
+	hasher := fnv.New64a()
+	hasher.Write(([]byte(strings.Join(strs, ","))))
+	return worldID(hasher.Sum64())
+}
+
+func initialWorld(sys system) world {
+	vars := map[varName]int{}
+	for name, val := range sys.variables {
+		vars[name] = val
+	}
+
+	counters := map[procName][]statement{}
+	for _, proc := range sys.processes {
+		counters[proc.name] = proc.statements
+	}
+
+	newEnv := environment{
+		variables: vars,
+	}
+
+	return NewWorld(newEnv, counters)
+}
+
+func stepLocal(env environment, pname procName, stmts []statement) ([]localState, error) {
+	if len(stmts) == 0 {
+		return []localState{}, nil
+	}
+
+	return stmts[0].execute(env, pname, stmts[1:])
+}
+
+func stepGlobal(wld world) ([]world, error) {
+	wlds := []world{}
+
+	// プロセスを選ぶループ
+	for pname, stmts := range wld.programCounters {
+		states, err := stepLocal(wld.environment, pname, stmts)
+		if err != nil {
+			return []world{}, err
+		}
+		// そのプロセスの動作の可能性に対するループ
+		for _, state := range states {
+			counters := map[procName][]statement{}
+			for n, ss := range wld.programCounters {
+				if n == pname {
+					counters[n] = state.statements
+				} else {
+					counters[n] = ss
+				}
+			}
+			wld := NewWorld(state.environment, counters)
+			wlds = append(wlds, wld)
+		}
+	}
+
+	return wlds, nil
+}
+
+func KripkeModel(sys system) (kripkeModel, error) {
+	init := initialWorld(sys)
+
+	visited := worlds{}
+	visited.insert(init)
+	accs := map[worldID][]worldID{}
+
+	stack := []world{init}
+	for len(stack) > 0 {
+		current := stack[len(stack)-1]
+		stack = stack[:len(stack)-1]
+
+		acc := []worldID{}
+		nexts, err := stepGlobal(current)
+		if err != nil {
+			return kripkeModel{}, err
+		}
+		for _, next := range nexts {
+			acc = append(acc, next.id)
+
+			if !visited.member(next) {
+				visited.insert(next)
+				stack = append(stack, next)
+			}
+		}
+		accs[current.id] = acc
+	}
+
+	return kripkeModel{
+		worlds:     visited,
+		initial:    init.id,
+		accessible: accs,
+	}, nil
+}
diff --git a/model-checking-book/main.go b/model-checking-book/main.go
new file mode 100644
index 0000000..bbe0fb9
--- /dev/null
+++ b/model-checking-book/main.go
@@ -0,0 +1,18 @@
+package main
+
+import (
+	"log"
+	"os"
+)
+
+// $ go run ./...
+// 何も返ってこなければ成功
+func main() {
+	sys := Mutex()
+	model, err := KripkeModel(sys)
+	if err != nil {
+		log.Fatal(err)
+
+	}
+	model.WriteAsDot(os.Stdout)
+}
diff --git a/model-checking-book/mutex.dot b/model-checking-book/mutex.dot
new file mode 100644
index 0000000..65fea8b
--- /dev/null
+++ b/model-checking-book/mutex.dot
@@ -0,0 +1,111 @@
+digraph {
+  11221991691700317303 [label="critical=0"];
+  11221991691700317303 [ penwidth = 5 ];
+  921510197053021043 [label="critical=0"];
+  3487952452228750286 [label="critical=1"];
+  1719250695456733177 [label="critical=2"];
+  7436987335548333450 [label="critical=1"];
+  1280363200138696619 [label="critical=0"];
+  15882637993728910432 [label="critical=1"];
+  15782641524140305967 [label="critical=2"];
+  7036388809428607951 [label="critical=0"];
+  3238549733672927470 [label="critical=1"];
+  17929327978746845670 [label="critical=1"];
+  5752008125370460663 [label="critical=2"];
+  12639326343918287883 [label="critical=2"];
+  3372605456242150480 [label="critical=1"];
+  1161750338396871911 [label="critical=0"];
+  10778493553980671058 [label="critical=3"];
+  9472190305011600930 [label="critical=1"];
+  12398303882891926298 [label="critical=1"];
+  3649300105249688795 [label="critical=0"];
+  3019680412146324886 [label="critical=1"];
+  5126610833276348920 [label="critical=1"];
+  2808960358517481579 [label="critical=2"];
+  1394296989391464834 [label="critical=1"];
+  17106298229703682801 [label="critical=2"];
+  4058687436091955395 [label="critical=0"];
+  3975512886879023247 [label="critical=0"];
+  11490742439060118968 [label="critical=1"];
+  11490742439060118968 -> 15882637993728910432;
+  11490742439060118968 -> 3372605456242150480;
+  11490742439060118968 -> 11221991691700317303;
+  921510197053021043 -> 7036388809428607951;
+  921510197053021043 -> 12398303882891926298;
+  921510197053021043 -> 3649300105249688795;
+  11221991691700317303 -> 4058687436091955395;
+  11221991691700317303 -> 921510197053021043;
+  11221991691700317303 -> 3975512886879023247;
+  12398303882891926298 -> 11221991691700317303;
+  12398303882891926298 -> 17929327978746845670;
+  12398303882891926298 -> 1394296989391464834;
+  17106298229703682801 -> 3019680412146324886;
+  17106298229703682801 -> 10778493553980671058;
+  17106298229703682801 -> 17929327978746845670;
+  3487952452228750286 -> 1280363200138696619;
+  3487952452228750286 -> 5752008125370460663;
+  3487952452228750286 -> 17106298229703682801;
+  17929327978746845670 -> 3487952452228750286;
+  17929327978746845670 -> 3975512886879023247;
+  17929327978746845670 -> 2808960358517481579;
+  3019680412146324886 -> 15782641524140305967;
+  3019680412146324886 -> 3975512886879023247;
+  3019680412146324886 -> 3238549733672927470;
+  3372605456242150480 -> 921510197053021043;
+  3372605456242150480 -> 5126610833276348920;
+  3372605456242150480 -> 2808960358517481579;
+  1394296989391464834 -> 4058687436091955395;
+  1394296989391464834 -> 3487952452228750286;
+  1394296989391464834 -> 1719250695456733177;
+  5126610833276348920 -> 5752008125370460663;
+  5126610833276348920 -> 7036388809428607951;
+  5126610833276348920 -> 12639326343918287883;
+  1161750338396871911 -> 5126610833276348920;
+  1161750338396871911 -> 3238549733672927470;
+  1161750338396871911 -> 3487952452228750286;
+  15882637993728910432 -> 15782641524140305967;
+  15882637993728910432 -> 5126610833276348920;
+  15882637993728910432 -> 4058687436091955395;
+  7036388809428607951 -> 1394296989391464834;
+  7036388809428607951 -> 1161750338396871911;
+  7036388809428607951 -> 9472190305011600930;
+  5752008125370460663 -> 10778493553980671058;
+  5752008125370460663 -> 15882637993728910432;
+  5752008125370460663 -> 1394296989391464834;
+  15782641524140305967 -> 11490742439060118968;
+  15782641524140305967 -> 12639326343918287883;
+  15782641524140305967 -> 7436987335548333450;
+  4058687436091955395 -> 7036388809428607951;
+  4058687436091955395 -> 1280363200138696619;
+  4058687436091955395 -> 7436987335548333450;
+  3975512886879023247 -> 3649300105249688795;
+  3975512886879023247 -> 11490742439060118968;
+  3975512886879023247 -> 1280363200138696619;
+  3238549733672927470 -> 12639326343918287883;
+  3238549733672927470 -> 3649300105249688795;
+  3238549733672927470 -> 17106298229703682801;
+  10778493553980671058 -> 2808960358517481579;
+  10778493553980671058 -> 15782641524140305967;
+  10778493553980671058 -> 1719250695456733177;
+  9472190305011600930 -> 1719250695456733177;
+  9472190305011600930 -> 3238549733672927470;
+  9472190305011600930 -> 921510197053021043;
+  3649300105249688795 -> 3372605456242150480;
+  3649300105249688795 -> 1161750338396871911;
+  3649300105249688795 -> 17929327978746845670;
+  1280363200138696619 -> 3019680412146324886;
+  1280363200138696619 -> 1161750338396871911;
+  1280363200138696619 -> 15882637993728910432;
+  12639326343918287883 -> 10778493553980671058;
+  12639326343918287883 -> 9472190305011600930;
+  12639326343918287883 -> 3372605456242150480;
+  2808960358517481579 -> 11490742439060118968;
+  2808960358517481579 -> 12398303882891926298;
+  2808960358517481579 -> 5752008125370460663;
+  1719250695456733177 -> 7436987335548333450;
+  1719250695456733177 -> 17106298229703682801;
+  1719250695456733177 -> 12398303882891926298;
+  7436987335548333450 -> 11221991691700317303;
+  7436987335548333450 -> 9472190305011600930;
+  7436987335548333450 -> 3019680412146324886;
+}
diff --git a/model-checking-book/mutex.go b/model-checking-book/mutex.go
new file mode 100644
index 0000000..0e6a4ee
--- /dev/null
+++ b/model-checking-book/mutex.go
@@ -0,0 +1,22 @@
+package main
+
+func badThread(name procName) process {
+	return Process(name,
+		For(
+			Case(When(True()),
+				Assign("critical", Add(Var("critical"), Int(1))),
+				// critical section
+				Assign("critical", Sub(Var("critical"), Int(1))),
+			),
+		),
+	)
+}
+
+func Mutex() system {
+	return System(
+		Variables{"critical": 0},
+		badThread("A"),
+		badThread("B"),
+		badThread("C"),
+	)
+}
diff --git a/model-checking-book/mutex.png b/model-checking-book/mutex.png
new file mode 100644
index 0000000..d8247be
Binary files /dev/null and b/model-checking-book/mutex.png differ
diff --git a/model-checking-book/sample.dot b/model-checking-book/sample.dot
new file mode 100644
index 0000000..1059699
--- /dev/null
+++ b/model-checking-book/sample.dot
@@ -0,0 +1,8 @@
+digraph {
+    1 [label="A"];
+    2 [label="B"];
+    3 [label="C"];
+    1 -> 2;
+    2 -> 3;
+    3 -> 2;
+}
diff --git a/model-checking-book/sample.png b/model-checking-book/sample.png
new file mode 100644
index 0000000..74d08cd
Binary files /dev/null and b/model-checking-book/sample.png differ
diff --git a/model-checking-book/semantics.go b/model-checking-book/semantics.go
new file mode 100644
index 0000000..ba9db30
--- /dev/null
+++ b/model-checking-book/semantics.go
@@ -0,0 +1,178 @@
+package main
+
+import "fmt"
+
+func (expr intValueExpression) eval(_ map[varName]int) (int, error) {
+	return expr.value, nil
+}
+
+func (expr variableExpression) eval(vars map[varName]int) (int, error) {
+	if val, ok := vars[expr.name]; ok {
+		return val, nil
+	}
+	return 0, fmt.Errorf("undefined variable: %s", expr.name)
+}
+
+func (expr addExpression) eval(vars map[varName]int) (int, error) {
+	l, err := expr.left.eval(vars)
+	if err != nil {
+		return 0, err
+	}
+	r, err := expr.right.eval(vars)
+	if err != nil {
+		return 0, err
+	}
+	return l + r, nil
+}
+
+func (expr subExpression) eval(vars map[varName]int) (int, error) {
+	l, err := expr.left.eval(vars)
+	if err != nil {
+		return 0, err
+	}
+	r, err := expr.right.eval(vars)
+	if err != nil {
+		return 0, err
+	}
+	return l - r, nil
+}
+
+func (expr boolValueExpression) eval(_ map[varName]int) (bool, error) {
+	return expr.value, nil
+}
+
+func (expr eqExpression) eval(vars map[varName]int) (bool, error) {
+	l, err := expr.left.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	r, err := expr.right.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	return l == r, nil
+}
+
+func (expr ltExpression) eval(vars map[varName]int) (bool, error) {
+	l, err := expr.left.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	r, err := expr.right.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	return l < r, nil
+}
+
+func (expr notExpression) eval(vars map[varName]int) (bool, error) {
+	val, err := expr.expression.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	return !val, nil
+}
+
+func (expr orExpression) eval(vars map[varName]int) (bool, error) {
+	l, err := expr.left.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	r, err := expr.right.eval(vars)
+	if err != nil {
+		return false, err
+	}
+	return l || r, nil
+}
+
+type environment struct {
+	variables map[varName]int
+}
+
+type localState struct {
+	environment environment
+	statements  []statement
+}
+
+func (stmt assignStatement) execute(env environment, pname procName, cont []statement) ([]localState, error) {
+	if _, ok := env.variables[stmt.varName]; !ok {
+		return []localState{}, fmt.Errorf("undefined variable: %s", stmt.varName)
+	}
+	vars := map[varName]int{}
+
+	// 新しい環境に詰め替える
+	for name, val := range env.variables {
+		if name == stmt.varName {
+			// 右辺として代入すべき値の評価
+			newVal, err := stmt.expression.eval(env.variables)
+			if err != nil {
+				return []localState{}, err
+			}
+			vars[name] = newVal
+		} else {
+			vars[name] = val // 評価されない部分はそのままコピー
+		}
+	}
+
+	state := localState{
+		environment: environment{variables: vars},
+		statements:  cont,
+	}
+	return []localState{state}, nil
+}
+
+func (grd whenGuard) execute(env environment, pname procName) (environment, bool, error) {
+	condition, err := grd.expression.eval(env.variables) // NOTE: envがガード中に更新される可能性がある
+	if err != nil {
+		return environment{}, false, err
+	}
+	// ガードの実行可能性の確認
+	if !condition {
+		return env, false, nil
+	}
+	return env, true, nil
+}
+
+func (stmt switchStatement) execute(env environment, pname procName, cont []statement) ([]localState, error) {
+	states := []localState{}
+
+	for _, c := range stmt.cases { // stmt.casesはstructの配列
+		newEnv, condition, err := c.guard.execute(env, pname)
+		if err != nil {
+			return []localState{}, err
+		}
+		// ガードの実行可能性の確認
+		if condition {
+			stmts := append(c.statements, cont...)
+			state := localState{
+				environment: newEnv,
+				statements:  stmts,
+			}
+			states = append(states, state) // この時点ではランダムではなく、前から順にtrueなconditionのものがstatesに積まれる。しかしstatesは全て拾われるので、後続処理で並列に実行され、結果が非決定的になる？
+		}
+	}
+	return states, nil
+}
+
+// PramoのForは抜けられない(caseが空の場合はプロセスがブロックされる)
+func (stmt forStatement) execute(env environment, pname procName, cont []statement) ([]localState, error) {
+	states := []localState{}
+
+	for _, c := range stmt.cases {
+		newEnv, condition, err := c.guard.execute(env, pname)
+		if err != nil {
+			return []localState{}, err
+		}
+		// ガードの実行可能性の確認
+		if condition {
+			stmts := append(c.statements, stmt) // NOTE: ここがswitch, forの違い。stmtは自身(forStatement)なので、もう一度この処理が後続として入るようになる。それによってループする。
+			stmts = append(stmts, cont...)      // NOTE: ここがswitch, forの違い
+			state := localState{
+				environment: newEnv,
+				statements:  stmts,
+			}
+			states = append(states, state)
+		}
+	}
+	return states, nil
+}
diff --git a/model-checking-book/syntax.go b/model-checking-book/syntax.go
new file mode 100644
index 0000000..ebe3730
--- /dev/null
+++ b/model-checking-book/syntax.go
@@ -0,0 +1,176 @@
+package main
+
+type system struct {
+	variables Variables
+	processes []process
+}
+
+func System(vars Variables, procs ...process) system {
+	return system{variables: vars, processes: procs}
+}
+
+type varName string
+type Variables map[varName]int
+
+type procName string
+
+type process struct {
+	name       procName
+	statements []statement
+}
+
+func Process(name procName, stmts ...statement) process {
+	return process{name: name, statements: stmts}
+}
+
+type intExpression interface {
+	eval(map[varName]int) (int, error)
+}
+
+var _ intExpression = intValueExpression{}
+var _ intExpression = variableExpression{}
+var _ intExpression = addExpression{}
+var _ intExpression = subExpression{}
+
+type intValueExpression struct {
+	value int
+}
+
+func Int(val int) intValueExpression {
+	return intValueExpression{value: val}
+}
+
+type variableExpression struct {
+	name varName
+}
+
+func Var(name varName) variableExpression {
+	return variableExpression{name: name}
+}
+
+type addExpression struct {
+	left  intExpression
+	right intExpression
+}
+
+func Add(l intExpression, r intExpression) addExpression {
+	return addExpression{left: l, right: r}
+}
+
+type subExpression struct {
+	left  intExpression
+	right intExpression
+}
+
+func Sub(l intExpression, r intExpression) subExpression {
+	return subExpression{left: l, right: r}
+}
+
+type boolExpression interface {
+	eval(map[varName]int) (bool, error)
+}
+
+var _ boolExpression = boolValueExpression{}
+var _ boolExpression = eqExpression{}
+var _ boolExpression = ltExpression{}
+var _ boolExpression = notExpression{}
+var _ boolExpression = orExpression{}
+
+type boolValueExpression struct {
+	value bool
+}
+
+func True() boolValueExpression {
+	return boolValueExpression{value: true}
+}
+
+type eqExpression struct {
+	left  intExpression
+	right intExpression
+}
+
+func Eq(l intExpression, r intExpression) eqExpression {
+	return eqExpression{left: l, right: r}
+}
+
+type ltExpression struct {
+	left  intExpression
+	right intExpression
+}
+
+func Lt(l intExpression, r intExpression) ltExpression {
+	return ltExpression{left: l, right: r}
+}
+
+type notExpression struct {
+	expression boolExpression
+}
+
+func Not(bexpr boolExpression) notExpression {
+	return notExpression{expression: bexpr}
+}
+
+type orExpression struct {
+	left  boolExpression
+	right boolExpression
+}
+
+func Or(l boolExpression, r boolExpression) orExpression {
+	return orExpression{left: l, right: r}
+}
+
+type statement interface {
+	execute(env environment, pname procName, cont []statement) ([]localState, error)
+}
+
+var _ statement = assignStatement{}
+var _ statement = switchStatement{}
+var _ statement = forStatement{}
+
+type assignStatement struct {
+	varName    varName
+	expression intExpression
+}
+
+func Assign(x varName, iexpr intExpression) assignStatement {
+	return assignStatement{varName: x, expression: iexpr}
+}
+
+type guard interface {
+	execute(env environment, pname procName) (environment, bool, error)
+}
+
+var _ guard = whenGuard{}
+
+type whenGuard struct {
+	expression boolExpression
+}
+
+func When(bexpr boolExpression) whenGuard {
+	return whenGuard{expression: bexpr}
+}
+
+type guardCase struct {
+	guard      guard
+	statements []statement
+}
+
+func Case(grd guard, stmts ...statement) guardCase {
+	return guardCase{guard: grd, statements: stmts}
+}
+
+type switchStatement struct {
+	cases []guardCase
+}
+
+func Switch(cases ...guardCase) switchStatement {
+	return switchStatement{cases: cases}
+}
+
+type forStatement struct {
+	cases []guardCase
+}
+
+func For(cases ...guardCase) forStatement {
+	return forStatement{cases: cases}
+}
diff --git a/model-checking-book/visualizer.go b/model-checking-book/visualizer.go
new file mode 100644
index 0000000..eeb1ec4
--- /dev/null
+++ b/model-checking-book/visualizer.go
@@ -0,0 +1,41 @@
+package main
+
+import (
+	"fmt"
+	"io"
+	"sort"
+	"strings"
+)
+
+func (wld world) label() string {
+	strs := []string{}
+
+	vnames := []string{}
+
+	for name := range wld.environment.variables {
+		vnames = append(vnames, string(name))
+	}
+	sort.Strings(vnames)
+	for _, name := range vnames {
+		val := wld.environment.variables[varName(name)]
+		strs = append(strs, fmt.Sprintf("%s=%d", name, val))
+	}
+
+	return strings.Join(strs, "\n")
+}
+
+func (model kripkeModel) WriteAsDot(w io.Writer) {
+	fmt.Fprintln(w, "digraph {")
+	for id, wld := range model.worlds {
+		fmt.Fprintf(w, "  %d [label=\"%s\"];\n", id, wld.label())
+		if id == model.initial {
+			fmt.Fprintf(w, "  %d [ penwidth = 5 ];\n", id)
+		}
+	}
+	for from, tos := range model.accessible {
+		for _, to := range tos {
+			fmt.Fprintf(w, "  %d -> %d;\n", from, to)
+		}
+	}
+	fmt.Fprintln(w, "}")
+}