TLA+入門とパーティーでの活用事例（2023）

本記事では、形式仕様記述言語TLA+の基本概念と実践的な使い方を、パーティー（パーティーゲームやパーティー計画）を題材に解説する。状態機械や時相論理を用いてシステムの正しさを検証する手法を、具体的な例を通して学べる入門記事である。