情報処理学会 第81回全国大会講演要旨

著者らは，複数の車両が電子連結することで隊列走行可能な端末交通システムの研究開発を行なっている．この交通システムの利点は，車列が随時再編成されることで旅客を乗り換えなしに輸送できる点にある．本論文では，この交通システムに対し，車両の運行スケジュールをモデル検査法によって生成する手法を提案する．その基本的なアイディアは，スケジュールが満たすべき条件を時相論理式で記述し，その否定をモデル検査器のNuSMVで検証するというものである．これにより，求めるべきスケジュールを検証の結果得られる反例から求めることができる．また本論文では，様々な形態の交通網に適用することにより，提案手法の有用性を示す．