2026-03-08T21:40:18Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00129601 2025-01-21T00:28:42Z 6504:8103:8110

有理時間を含むプログラムの仕様表現および動作解析 Representation and Analysis of Rationally Timed Programs 有理時間を含むプログラムの仕様表現や検証・動作解析についての2種類の方法について提案する。1つは拍車を用いる方法である。拍車は数学的には我々の立場ではそれ自身プロセスの特別な場合として扱われる概念であるが,直観的にはプロセスのスケジューラを一般化した概念であり,時相論理のnext operatorを一般化したものと考えることもできる。プログラムを拍車の履歴を入力とする一種のオートマトンとして捉える事により検証が容易になった。もう1つは形式的体系「束時相論理」(envelope system)である。時刻で真理値の変化する命題の真理集合を考え,閉包概念を特殊化したenvelopeと呼ぶ集合演算子を用いることにより証明に集合演算の直観を持ち込む事が可能となった。これらを実時間問題に連用して動作解析を行った例を示す。 conference paper 情報処理学会 1996-03-06 application/pdf 全国大会講演論文集 ソフトウェア 第52回 3 4 AN00349328 https://ipsj.ixsq.nii.ac.jp/record/129601/files/KJ00001329822.pdf jpn