Title

強磁性体モデルにおけるS^2値関数に対する変分問題・偏微分方程式について
(Variational problems and PDEs for S^2-valued maps in the ferromagnetic model)

Date

2025年5月7日（水）　16:45〜17:45 　（16:15より105談話室でtea)

Place

京都大学大学院理学研究科3号館110講演室
(Rm110, Building No.3, Graduate School of Science, Kyoto University)

Speaker

清水 一慶 (Ikkei Shimizu)氏 （京大・理）

Abstract

　強磁性体の磁化を記述する数理モデルの一つであるLandau-Lifshitzモデルでは、磁化を2次元球面S^2に値をとる関数として定式化し、そのエネルギー変分問題や偏微分方程式を通じて物理現象の説明が行われる。これらはその物理的意義に加え、豊富な数学的構造を備えていることから、数学的研究対象として現在に至るまで盛んに研究が行われている。また様々な数学分野との接点も垣間見ることができ、例えば調和写像、su(2)ゲージ場、非線形シュレディンガー方程式、可積分系などとの関連が知られている。談話会ではスキルミオン解の構成に関する自分の研究内容の紹介を交えつつ、Landau-Lifshitzモデルの数学解析に関する背景・先行研究・今後の課題等について俯瞰的に説明する。

Title

不動点を用いたモデル検査とProduct Constructionの不可能性定理
(Model checking via fixed points and no-go theorem for product construction)

Date

2025年4月30日（水）　16:45〜17:45
（16:15より数理研 2 階コモンルームでtea)　

Place

京都大学数理解析研究所 (RIMS) 110号室
(Rm110, Research Institute for Mathematical Sciences, Kyoto University)

Speaker

郡 茉友子 (Mayuko Kori)氏 （京大・数理研）

Abstract

　形式検証とは、システムの正しさを数理的に保証するための手法である。本講演では、形式検証の中でも特にモデル検査に焦点を当て、圏論的・束論的な不動点理論に基づく枠組みを紹介する。自己関手の余代数を用いることで、遷移システムやマルコフ決定過程など多様なシステムを表すことができ、不動点で意味を表すことができる。この不動点の性質を用いた様々な検証手法が存在する。特に、システムと仕様の積をとって検証問題を効率的に解くProduct Constructionという手法に注目し、確率的システムとオートマトンの 合成による、仕様を満たす確率の計算問題を取り上げる。そのうえで、マルコフ連鎖と非決定性有限オートマトンの合成が実現不可能であることを自然変換の特徴づけを用いて示す。