Think Stitch
PRINCIPIA  最近の更新


プロセスの比較 2: 拒否

この文書は SyncStitch ユーザガイド 第15章からの抜粋です。

拒否によるプロセスの比較

この章ではプロセスを比較するために SyncStitch が持つもう1つの検査機能について説明します。

前章で説明したトレース比較には弱点が2つありました。1つは区別したいのに区別できないプロセスがあるという点です。もう1つは「イベントが必ず起こる」という条件を表すことができない、という点です。

トレース比較で区別できないプロセスは非決定性を持つプロセスでした。区別ができない理由は非決定性という性質をトレース集合で表すことができないからです。そこで非決定性を表すために「拒否」という概念を導入します。トレースと拒否を組み合わせると、より精密にプロセスを比較できるようになります。さらに拒否を使うと「イベントが必ず起こる」という条件を表すことができるようになります。

この章では、はじめに拒否について説明します。次にトレースと拒否の組み合わせによるプロセスの比較について説明します。つづいて音楽プレーヤの設計を例として、トレースと拒否による比較の使い方を説明します。

この章で説明する項目

  • 受理と受理集合
  • 拒否と拒否集合 refusals(P)
  • アルファベット
  • トレース後のプロセス P/s
  • プロセスが等しい条件
  • 実装が仕様を満たす条件
  • 極大拒否集合と極小受理集合
  • シグナルイベント
  • 特徴プロセス
  • プロセスエクスプローラのトレースモード

非決定性を持つプロセスの分類

プロセスを比較する目的は、設計したプロセスが仕様を満たしているかどうか確認することです。その基準の1つとしてトレース比較を見てきました。しかしトレース比較には不十分な点があります。トレース比較の結果、トレース違反があった場合は仕様を満たしていないと確実にいうことができますが、なかった場合には仕様を満たしていると確実にいえるわけではないからです。確実にいえない理由は、トレース集合が同じなのに、外から見た動作が異なるプロセスがあるからです。この点を例を使ってもう1度確認します。

左が仕様を表すプロセス、右が設計で作ったプロセスだとします。トレース比較によれば、この実装は仕様を満たすことになってしまいます。トレース集合が同じなのでトレース違反はないからです。しかし実際には仕様を満たしていません。利用者が仕様にある動作を期待してイベント c を提示すると、必ず同期するはずなのにデッドロックすることがあるからです。

問題は、プロセスを区別するトレース比較の能力が低いということです。比較の結果、仕様を満たしていると確実にいえるためには、仕様を満たしているものと満たしていないものを、もっと精密に分けられる基準が必要です。

トレース集合の異なるプロセスは異なるプロセスであることがわかっているので、ここで必要なことは、同じトレース集合を持つプロセスを区別することです。言い換えると、トレース集合によって大まかに分類されたプロセスを、さらに細かく分類することができような基準が必要だということです。1つのトレース集合に対応する複数のプロセスのうち、利用者から見て同じものはどれとどれで、異なるものはどれなのか、という判断ができる基準です。そこでまず、同じトレースを持つプロセスを分類するという問題を考えることにします。

このような問題を考えるときには、できるだけ簡単な例を挙げて調べる方法が有効です。ただ、あまり簡単にしすぎると調べたいと思っている性質が消えてしまうことがあります。例えばトレース集合として空列 () だけからなる集合を考えると、利用者から見えるものが何もなくなってしまうので、考えようがありません。性質が消えてしまう境界線がどこにあるのか、最初はわかりませんからやってみるしかありません。簡単な方から初めて、徐々に複雑な場合を調べるということです。

同じトレース集合を持つプロセスが複数あるのは非決定性があるからです。非決定性を表すには少なくともイベントが2個必要です。そこでイベントを a, b として、トレース集合 {(), (a), (b)} を持つプロセスを考えます。記号 {e1, e2,... , en} は e1, e2,... , en を要素とする集合を表します。いままで使っていた記法で書くと

()
(a)
(b)

となります。要素の数が少ないときには、集合の記法の方が簡潔なので、そちらを使うことにします。

このトレース集合をもつプロセスを挙げてみると、次の図のようになります。A は非決定性を持たないプロセスです。B〜J は非決定的選択の基本形になるものです。K は tau 遷移混在形の例、L は発散を含む例、M は tau 遷移混在形でかつ発散を含む例です。tau 遷移混在形や発散を含むものは後で考えることにして、まず A〜J について考えます。

問題はこのうちのどれとどれが同じプロセスで、どれが異なるプロセスなのかということです。最終的に知りたいことは、それを判断する基準です。

プロセスは外から見える現象の違いによって区別します。トレース集合が同じなので、ただ見ているだけでは区別できません。そこで、より積極的に、プロセスを利用する立場から相互作用を行ったときに区別できるかどうかを考えます。利用者を表す試験プロセスを用意して、対象のプロセスと相互作用をさせたときに何が起こるか考えるわけです。いってみれば思考実験を行うということです。

相互作用をさせるということは、対象とするプロセスと試験プロセスを並行合成して、イベントが発生するかどうかを見るということです。外から見ることのできる対象プロセスの動作をすべて把握するためには、試験プロセスが相互作用を行う唯一の相手だとする必要があります。したがって並行合成の同期リストには、対象プロセスが発生する可能性のあるすべてのイベントを指定します。

このように実験環境を整えると、実験で調整できるパラメータは、試験プロセスが提示するイベントの集合が何かということだけになります。イベントの集合をいろいろ選んで実験を行うということです。いろいろなイベントの集合に対応する結果のあり方が、対象プロセスの性質を表すことになります。

問題は実験の結果としてわかることは何かということです。これについては例を見る方がわかりやすいので、先に例を見ることにします。

最初の試験プロセスとして、イベント a だけを発生させる次のプロセスを考えます。

これとプロセス A を並行合成すると、必ずイベント a が発生します。これに対してプロセス B と並行合成した場合は、イベント a が発生するかもしれないし、しないかもしれません。

これは実際にプロセスを実装して動かしたらわかることではありません。実際に動かした場合に結果としてわかることは、イベントが発生したか・発生しなかったか、発生した場合にはどのイベントが発生したのか、ということです。発生しなかったというのは、並行合成したプロセスがイベントを発生させることはない、という意味ではなく、単に実験時間が終了するまでには起こらなかったというだけです。

しかしここで知りたいことは、このような個別の実験結果ではありません。非決定性があるために、実験の結果はまちまちになる可能性があるからです。ここで必要なのは、トレースのところで説明した設計者の立場に立つことです。利用者が1度の実験で知ることができるのは「イベント x が発生した/イベントは発生しなかった」という区別だけです。実験を繰り返し行ったとしても、わかるのは「イベント x はすべての実験で発生した/イベント x は発生したことも、しなかったこともあった/イベント x は一度も発生しなかった」ということだけです。「すべての実験で発生した」ということは「必ず発生する」ということではありません。しかし設計者に必要なのは「必ず発生する/発生しないことがある」という区別です。なぜなら仕様は確実に満たさなければならないからです。そのためには確実に起こることと、そうでないことを区別する必要があります。この区別はプロセス内部の作りを知らなければわかりません。そういう意味で、ここで行うことは本当の意味の実験ではなく、理論的な計算に近いものです。プロセス A の場合に必ずイベントが発生するということも、プロセス B の場合に2つの可能性があるということも、どちらも状態遷移図を見て初めてわかることです。結論としては、試験プロセスとの並行合成から知るべきことは、提示したイベントのどれかが必ず発生するかどうかということです。

では、他のプロセスについても見ていきます。プロセス D〜J はイベントが発生するかもしれないし、しないかもしれません。興味深いことにプロセス C では必ずイベントが発生します。どちらの遷移先にもイベント a の付いた遷移があるからです。

同様にイベント b だけを発生させる試験プロセスで実験を行います。この場合は対称的にプロセス D で必ずイベントが発生します。ここまでの結果をまとめると次のようになります。○は必ずイベントが発生するということを意味します。×はイベントが発生するかもしれないし、発生しないかもしれないという意味です。

A B C D E F G H I J
{a} × × × × × × × ×
{b} × × × × × × × ×

イベントが2つあるので、試験プロセスはもう1つあります。イベント a と b を両方提示する場合です。つまりプロセス A を試験プロセスとして使うことになります。この場合プロセス B が必ずどちらかのイベントで同期してくるようになります。非決定的選択のどちらが選ばれたとしても a, b どちらかが発生できるからです。同じくプロセス E も必ず同期するようになります。これに対して F〜J には停止状態への遷移があるので、何を提示しても必ずイベントが発生するようにはならないことがわかります。

A B C D E F G H I J
{a} × × × × × × × ×
{b} × × × × × × × ×
{a, b} × × × × ×

イベントは2種類だけですから、もう他に試験プロセスはありません。これが利用者から見て判断できるプロセスの違いのすべてです。結論として、A, B, C, D, F が相異なるプロセスの代表で、B と E は同じプロセス、F〜J はすべて同じプロセスということになります。

受理

プロセスにイベントの集合 X を提示したとき、X に含まれるいずれかのイベントが必ず発生するならば、X をプロセスの受理といいます。 この条件を満たすイベントの集合だけが受理です。

上の表でプロセスを1つ選んだとき、○のついている行に対応するイベントの集合が受理です。受理はプロセスが持つ属性だと考えられるので、「プロセスが受理を持つ」といういい方をします。「イベントの集合を受理する」というように述語としても使います。

受理集合

プロセスは複数の受理を持つこともあるし、1つも持たないこともあります。 例えばプロセス D は2つの受理 {b} と {a, b} を持ちます。 プロセス F は受理を持っていません。このように非決定性を持つプロセスは、どのような受理を持っているか、ということで分類することができます。上の表でいうと、縦に並んだ○×全体のパターンで区別できるということです。

そこでこのパターンを表すために、プロセスが持つすべての受理を集めて集合にします。 これを受理集合といいます。受理集合によってプロセスを区別できるわけです。

例えばプロセス D の受理集合は次のようになります。

{ {b}, {a, b} }

集合の集合なので、括弧が2重になります。

プロセス F は受理を持っていないので、受理集合は要素を1つも持っていない集合になります。要素を1つも持っていいない集合のことを空集合といいます。空集合は記号 {} で表すことにします。要素がないので、括弧の中に何もないということです。

拒否

表で○が付いているイベントの集合に注目する代わりに、×が付いているイベントの集合の方に注目することもできます。これを拒否といいます。拒否を言葉で説明すると次のようになります。

プロセスにイベントの集合 X を提示したとき、X に含まれるどのイベントも発生しない可能性があるならば、X をプロセスの拒否といいます。この条件を満たすイベントの集合だけが拒否です。

受理と同じく、拒否もプロセスが持つ属性だと考えられるので、「プロセスが拒否を持つ」といういい方をします。「イベントの集合を拒否する」というように述語としても使います。

受理に加えて拒否を考える理由は、後で見るように拒否の方が少しよいところがあるからです。先に受理を説明したのは、考え方として直接的でわかりやすいからです。今後は主に拒否を使います。しかし受理で考えた方がわかりやすい場合は、受理で考えてから拒否に翻訳するようにします。

拒否集合

プロセスが持つすべての拒否の集合を拒否集合といいます。拒否集合によってもプロセスを区別することができます。

プロセス P の拒否集合を refusals(P) という記号で表します。例えばプロセス D の拒否集合は次のようになります。表で×が付いているイベントの集合に加えて、空集合 {} が含まれます。イベントを何も提示しなければ発生するはずはないからです。

refusals(D) = { {}, {a} }

受理集合と異なり、プロセス F の拒否集合は空集合ではありません。プロセス F も空集合 {} を拒否するからです。

refusals(F) = { {} }

イベントが必ず発生するという条件

拒否を使うと、イベントが必ず発生するという条件を表すことができます。直観的にいうと、イベントが必ず発生するということは、プロセスがイベントを発生させる可能性があって、かつ拒否しないということだからです。プロセスがイベント e を発生させる可能性があるとします。これはトレース集合からわかります。もしイベント e だけを含むイベントの集合 {e} がプロセスの拒否でなければ、イベント e を提示すれば必ず発生することになります。つまり「イベント e が必ず発生する」という条件は「トレース (e) がトレース集合に含まれていて、かつイベントの集合 {e} が拒否ではない」ということです。

例えば、プロセス D は (a) と (b) をトレースとして持っているので、a, b どちらも発生させる可能性があります。イベント a だけを含む集合 {a} はプロセス D の拒否です。したがって必ず発生するとはいえません。しかしイベント b だけを含む集合 {b} はプロセス D の拒否ではありません。したがって必ず発生することがわかります。

アルファベット

拒否を考えるときには、プロセスで使うイベントの範囲をはっきりさせておく必要があります。注目している遷移のイベントだけでなく、他のイベントを含む集合についても拒否するかどうかを考えるからです。

プロセスが使う可能性のある、すべてのイベントの集合をアルファベットといいます。プロセスが話す A, B, C といったイメージです。プロセスが複数ある場合には、それぞれについてアルファベットを決めるのではなく、全体で1つのアルファベットを決めます。世の中の文献で使われている慣習にしたがって、アルファベットをギリシャ文字 Σ で表します。数列の和を表すシグマと同じ記号ですが、ここではイベントの集合を表すことにします。

例えばイベント a と b の2つだけを考えているときは

Σ = {a, b}

4つのイベント a, b, c, d を考えているときには

Σ = {a, b, c, d}

となります。

プロセスがチャネルを使う場合は、対応するチャネルイベントがアルファベットに含まれていると考えます。例えば、次のように定義されたチャネル ch を考えます。

(define-channel ch (x) '((0) (1) (2)))

このチャネルには、チャネルイベント ch.0, ch.1, ch.2 が対応します。プロセスが、このチャネルの他にはイベントもチャネル使わない場合、アルファベットは次のようになります。

Σ = {ch.0, ch.1, ch2}

もう1つ一般的な例を示しておきます。状態遷移モデルで使うイベントとチャネルが、定義ウィンドウで次のように定義されているとします。

(define-event a)
(define-event b)
(define-channel ch (x) '((0) (1) (2)))
(define-channel ch2 (x y) '((0 0) (0 1) (1 0)))

このとき、アルファベットは次のようになります。

Σ = {a, b, ch.0, ch.1, ch.2, ch2.0.0, ch2.0.1, ch2.1.0}

プロセスの終了を考える場合

終了するプロセスを考えるときには、アルファベットに終了イベント tick を含めて考える必要があります。 そこで、終了イベントを含むアルファベットを記号 Σ で表すことにします。 これは Σ に終了イベント tick を加えたイベントの集合という意味です。記号 ✓ は tick と同じ意味です。 並行プロセスの理論で使われている記号です。Σtick ではあまりにもバランスが悪いので、✓ を使うことにします。 数学的に書くと Σ✓ = Σ ∪ {✓} となります。

例えば

Σ = {a, b}

の場合は、

Σ = {a, b, tick}

となります。

拒否集合を求める方法

ここまではイベントが a と b の2つしかない簡単な場合について考えてきました。 この節では、状態遷移図とアルファベットを制限しない一般の場合について、状態遷移図の作りから拒否集合を求める方法を考えます。 これによって一般の場合でも、拒否集合を使うとプロセスを分類できることがわかります。 ただし例外があって、終了プロセスや発散がある場合の動作を分類するためには、拒否集合の定義を修正する必要があります。 それでも発散がある場合は完全に分類できないことがわかります。

状態遷移図の構成を次のようにわけて、それぞれについて拒否集合をどのように求めることができるかを考えます。

  • 安定状態
  • 非決定的選択の基本形
  • tau 遷移混在形
  • 発散
  • 終了プロセス

安定状態の場合

安定状態の場合を考えます。安定状態は tau 遷移も終了イベント tick の付いた遷移もない状態です。イベントとチャネルによる遷移だけを持つ状態です。例としてプロセス A を使います。

すぐにわかることは、イベント a の遷移があれば、a を含むイベントの集合 X が拒否にならないことです。なぜなら X を提示すると必ずイベント a が発生するからです。つまり X が受理になってしまうからです。同じことがイベント b についてもいえます。したがってプロセス A の拒否は、a も b も含んではいけないということになります。

これだけでは a も b も含んでいないイベントの集合が必ず拒否であるとはまだいえません。a も b も含んでいないイベントの集合の中に、拒否でないものが紛れ込んでいるかもしれないからです。そこで a も b も含んでいないイベントの集合のうち、任意のものを1つ選んでプロセスに提示したとします。これを X とします。X には a も b も含まれていないので、a でも b でも同期しません。プロセス A は他に遷移を持っていないので、イベントはまったく発生しないことになります。よって X は拒否になることがわかりました。どのイベントの集合を取ってきても、a も b も含まれていなければ拒否だということがわかったので、これが拒否のすべてだということになります。

例として、アルファベットを Σ = {a, b, c, d} とすると、プロセス A の拒否集合は次のようになります。

refusals(A) / Σ ={a, b, c, d} のとき

{}
{c}
{d}
{c, d}

イベント a と b を含まない集合の中で、要素の数がいちばん多い集合は {c,d} です。 アルファベット Σ = {a, b, c, d} から a と b を除いた残りだからです。 プロセス A の拒否集合を見ると、拒否はすべて {c, d} の部分集合になっていることがわかります。 しかもすべての部分集合が現れています。 安定状態の拒否集合はいつでもこのようになります。 理由は次のとおりです。

安定状態の遷移に付いているすべてのイベントの集合を I とします。 プロセス A の例でいうと I = {a, b} です。 このときアルファベット Σ から I に含まれる要素をすべて除いた残りの集合 X は拒否になります。 X と I に共通するイベントがないので、同期しないからです。 これはもっともイベントの多い拒否です。

次に X からイベントをいくつか取り除いてできる集合 Z も拒否になります。 なぜならプロセスに X を提示してもイベントが発生しないのに、イベントを減らしたら起こる可能性が高くなるはずはないからです。 したがって X のどのような部分集合もすべて拒否になることがわかります。 これ以外の集合には I のどれかが含まれることになりますから拒否になりません。 したがって X のすべての部分集合が、拒否のすべてであることがわかります。

この考え方に従えば、安定状態の拒否集合を求めることができます。手順をまとめると次のように成ります。

  • 遷移に現れるすべてのイベントを集めます。これを集合 I とします。
  • アルファベット Σ から I に含まれるイベントをすべて取り除いた残りの集合 X を作ります。
  • 集合 X の部分集合をすべて求めます。これが安定状態の拒否集合です。

アルファベット Σ から I に含まれるイベントをすべて取り除いた残りの集合を、記号で Σ - I と書きます。 これを2つの集合の差といいます。 例えば アルファベットが Σ = {a, b, c, d} で I = {a, b}の場合は Σ - I = {c, d} です。

停止プロセス STOP の唯一の状態は、遷移を持たない安定状態です。 遷移がないので集合 I は空集合になります。 したがって X = Σ になるので、停止プロセスはどのようなイベントの集合も拒否します。 例えば Σ = {a, b, c} の場合、停止プロセス STOP の拒否 refusals(STOP) は次のようになります。 数学的にいうと、これは集合 {a, b, c} のすべての部分集合からなる集合です。

refusals(STOP) = { {}, {a}, {b}, {c}, {a, b}, {a, c}, {b, c}, {a, b, c} }

非決定的選択の基本形の場合

非決定的選択の基本形について考えます。プロセス P の初期状態が非決定的選択になっていて、それそれの分岐先がプロセス Q, R であるとします。

結論からいうと、プロセス P の拒否集合は、プロセス Q の拒否集合とプロセス R の拒否集合を合わせたものになります。 数学的にいうと和集合ということです。記号を使うと、次のようになります。

refusals(P) = refusals(Q) ∪ refusals(R)

記号 ∪ は和集合を表します。2つの集合の要素をすべて集めた集合という意味です。

なぜこのようになるのか説明します。 プロセス Q の拒否を X とします。 これをプロセス P に提示すると、非決定的選択によって Q に遷移する可能性があって、しかもイベントが発生しない可能性があります。 したがってプロセス P の拒否でもあることがわかります。 プロセス R についても同じことがいえます。 逆に、プロセス P の拒否を X とします。 もしこれが プロセス Q の拒否でなければ、受理ということになります。 X は P の拒否ですから、イベントが発生しない場合がないといけません。 もし Q の方に遷移すると必ずイベントが発生してしまうので、R の方に遷移したときに、イベントが発生しない場合があることになります。 つまり X は R の拒否だということです。 これでプロセス P の拒否集合がプロセス Q の拒否集合とプロセス R の拒否集合の和集合であることが確認できました。 1点、拒否でなければ受理になるという部分については後で補足を行います。

例としてプロセス B の拒否集合を求めます。アルファベットを Σ = {a, b, c} とします。

非決定的選択が行われた後の状態はどちらも安定状態なので、先の手順で拒否集合を求めることができます。 上の分岐の場合、イベントの集合は I = {a} ですから、一番要素の多い拒否は {b, c} です。 したがって拒否集合は次のようになります。

refusals() = { {}, {b}, {c}, {b, c} }

同様に下の分岐の拒否集合は次のようになります。

refusals() = { {}, {a}, {c}, {a, c} }

プロセス B の拒否集合は、この2つを合わせたものになります。

refusals(B) = { {}, {a}, {b}, {c}, {a, c}, {b, c} }

次にプロセス D を見てみます。

上の分岐先はプロセス A と同じです。ここではアルファベットを Σ = {a, b, c} としているので、最も要素の多い拒否は {c} です。 したがって拒否集合は次のようになります。

refusals(A) = { {}, {c} }

下の分岐については先ほどプロセス B のところで求めました。両者を合わせると、プロセス D の拒否集合は次のようになります。

refusals(D) = { {}, {a}, {c}, {a, c} }

最後にプロセス F を見てみます。

下の分岐は停止プロセスです。 したがってすべてのイベントの集合を拒否します。 すると上の分岐の拒否集合がどのようなものだったとして、両者を合わせたものはすべてのイベントの集合を集めたものになります。

refusals(F) = { {}, {a}, {b}, {c}, {a, b}, {a, c}, {b, c}, {a, b, c} }

プロセス G〜J はすべて分岐の一方が停止プロセスなので、プロセス F と同じ拒否集合を持ちます。

tau 遷移混在形の場合

tau 遷移混在形について考えます。 一般に tau 遷移を持っている状態は拒否に関係しません。 これは受理の助けを借りるとわかります。 イベントの集合 X を提示したとき、tau 遷移があると自発的に発生してしまうので、その状態で必ずイベントが発生するということはありません。 したがって受理は tau 遷移の先で決まることになります。 遷移先状態が再び tau 遷移を持っている場合は、さらにその先で決まります。 結局、受理は最終的にたどり着く安定状態で決まります。 この一般的状況を次の図に示しました。 イベントの集合 X がこのプロセスの受理であるかどうかは、青で示した安定状態だけで決まります。 黄色で示した不安定状態は関係しません。

受理が安定状態だけで決まるということは、拒否もまた安定状態だけで決まるということです。 なぜかというと、受理集合と拒否集合は、考えられるイベントの集合すべてを2つに分けたものだからです。 ○×表でいえば、どの欄も○か×のどちらかだけが付いていて、空欄はないということです。 したがって○の付く欄が決まれば、残りは×であることが決まってしまいます。 数学的にいうと、拒否集合は受理集合の補集合です。

例えばアルファベットを Σ = {a, b, c} とすると、イベントの集合は全部で 23=8 個あります。

{ {}, {a}, {b}, {c}, {a, b}, {a, c}, {b, c}, {a, b, c} }

もしプロセスの受理集合が決まって、次のようであったとします。

{ {a}, {a, b}, {a, c}, {a, b, c} }

すると拒否集合は残りの集合として決まってしまうということです。

{ {}, {b}, {c}, {b, c} }

tau 遷移を持つ状態が拒否に関係しないということは、tau 遷移と並んでいる遷移のイベントも拒否には関係ないということです。 すると拒否を求める場合、tau 遷移混在形は非決定的選択の基本形と見なすことができます。 非決定的選択の拒否集合は、それぞれの分岐先の拒否集合を合わせたものなので、結論として、tau 遷移混在形の拒否集合は、tau 遷移だけでたどり着くことのできる、すべての安定状態における拒否集合を合わせたものになります。

例としてプロセス K を考えます。アルファベットを Σ = {a, b, c} とします。

初期状態には tau 遷移があるので、イベント a の付いた遷移は拒否集合に関係しません。 拒否集合は tau 遷移の遷移先で決まります。 したがってプロセス K の拒否集合は次のようになります。

refusals(K) = refusals() = { {}, {a}, {c}, {a, c} }

これは前に計算したプロセス D の拒否集合とじなので、プロセス K はプロセス D と同じであることがわかりました。

非決定性のところで、tau 遷移混在形を非決定的選択の基本形に変換できるということを説明しました。変換の規則を表す図をもう1度示します。

プロセス D はプロセス K を変換したものになっています。拒否集合を使って、この変換が正しいことを確かめてみます。

図に対応して、記号 A, B, C が遷移に付いているイベントの集合を表すとします。 tau 遷移混在形の場合は A が関係しないので、B の拒否集合と C の拒否集合を合わせたものになります。 一方、変換後の状態遷移図では、4つの場合の拒否集合を合わせたものになります。

B の拒否は、次に示した左側の図の斜線部から任意に選んだイベントの集合です。 これに対して変換後の一番上の状態は、イベントの集合 A と B を合わせた遷移を持っているので、拒否は右図の斜線部から任意に選んだ集合です。 しかし右の斜線部は左の斜線部に含まれているので、右の斜線部から選んだ集合は必ず左の斜線部に含まれます。 したがって A と B を合わせた遷移を持つ状態の拒否集合は、B の拒否集合に含まれることになります。 同じように A と C を合わせた遷移を持つ状態の拒否集合は、C の拒否集合に含まれます。 すると変換後の状態遷移図の拒否集合は B と C の拒否集合を合わせたものになり、tau 遷移混在形と同じであることになります。

発散がある場合

tau 遷移混在形のときに考えた一般形には1つ例外があります。 それは tau 遷移をどのようにたどっても安定状態にたどり着かない場合です。 安定状態にたどり着けないのは、無限の状態があって tau 遷移が無限に続いているか、あるいはtau 遷移だけからなる循環があるときです。 tau 遷移が無限に続いているような状態遷移図は除外して考えることにします。 すると安定状態にたどり着けないのは、どのように tau 遷移をたどっても tau 遷移の循環に行き当たる、次図のような場合です。

図において紫色で示した状態は tau 遷移だけからなる循環の中にあるので発散した状態です。 さらに、そこに至る途中の黄色で示した状態も発散した状態です。 そこから見て、tau 遷移を無限に繰り返すことができるからです。 つまりこのプロセスは最初から発散していることになります。

発散しているプロセスのすべてが安定状態を持っていないわけではありません。 次の図に示すように最初から発散していても、tau 遷移だけをたどって安定状態に達することのできる場合もあります。 そこで安定状態がある場合とない場合を分けて考える必要があります。

tau 遷移を持つ状態は拒否に関係しないという規則に従うと、安定状態のないプロセスは拒否をまったく持っていないことになります。 つまり拒否集合が空集合ということです。 しかし拒否の定義に照らして考えると、これはおかしなことです。 発散したプロセスにどのようなイベントの集合を提示しても、イベントが発生しないことがあるからです。 つまり定義どおりに解釈すると、発散したプロセスはすべてのイベントの集合を拒否することになります。 これは停止プロセスと同じです。

この矛盾を解消するために、ここでは tau 遷移を持つ状態は拒否に関係しないという規則の方を優先することにします。 理由は、安定状態のない発散したプロセスを停止プロセスと区別することができるからです。

このようにすると別の問題が起こります。 安定状態のない発散したプロセスは明らかに受理を持たないので、受理集合も拒否集合もどちらも空集合になります。 すると拒否でないイベントの集合は必ず受理だということができなくなるので、非決定的選択の拒否集合を求める規則が根拠を失うことになります。 そこで規則そのものを拒否の定義の一部だと考えることにします。 まとめると修正した拒否の定義は次のようになります。 拒否集合を次の規則で定義します。 そして拒否集合に含まれるものだけを拒否とします。

  • 安定状態の拒否集合は前に説明したとおりです。
  • tau 遷移を持つ状態は拒否に関係しません。
  • 非決定的選択の拒否集合は、各分岐先の拒否集合を合わせたものです。

意味による定義から求め方の規則による定義になりました。 実用的には、安定状態を持たない発散したプロセスと停止プロセスを区別できるようになったので、便利になりました。 代償として、受理と拒否の対称性が破れてしまいました。 受理に対しても同様の修正を考えることはできますが、あまり自然なものにはなりません。

修正した拒否の定義を使うと、安定状態を持つ発散したプロセスの拒否集合も求めることができるようになります。これは具体的な例で見ることにします。

例としてプロセス M を考えます。

プロセス M は安定状態を持たない発散したプロセスなので、拒否集合は空集合です。

refusals(M) = {}

次にプロセス L を考えます。アルファベットを Σ = {a, b, c} とします。

規則により非決定的選択の拒否集合は、それぞれの分岐の拒否集合を合わせたものです。 上の分岐はプロセス A と同じです。 下の分岐は安定状態を持たない発散なので、拒否集合は空集合です。 したがってプロセス L の拒否集合は次のようになります。

refusals(M) = refusals(A) = { {}, {c} }

プロセス L は発散していますが、拒否を持っています。 残念ながら修正した定義による拒否を使っても、発散したプロセスを完全に識別することはできません。 実用的にも、発散を分類することにはあまり意味がありません。 発散はどのようなものでも解消すべき問題だからです。 発散は発散検査で見つけることができるので、拒否で識別できる必要はありません。 拒否には非決定性を持つプロセスを区別するという本来の目的があります。 発散検査と拒否による比較で役割分担をするということです。

終了プロセス

終了プロセスの拒否集合を考えます。 プロセスの終了は終了イベント tick で表します。 終了イベント tick は相互作用を表すイベントではないので、試験プロセスが提示して同期するかどうか調べるというわけにはいきません。 したがってそもそも拒否という考え方の対象にならないように見えます。

しかし拒否にはもう1つ目的があります。 イベントが必ず発生するという条件を表すことです。 プロセスはいつでも自発的に終了することができるので、終了プロセス SKIP は終了イベントを拒否しないと考えることができます。 終了プロセスはこれ以外のイベントを発生させないので、tick を含まないイベントの集合はすべて拒否します。

例えばアルファベットを Σ = {a, b, tick} とします。 終了イベントを考えるので、Σ ではなく tick を含む Σ を考えます。 終了プロセス SKIP の拒否は次のようになります。

refusals(SKIP) = {  {}, {a}, {b}, {a, b} }

これは tick を含めない場合の停止プロセス STOP の拒否集合と同じですが、tick を含める場合、停止プロセスは tick も拒否するので、拒否集合は次のようになります。

refusals(STOP) = { {}, {a}, {b}, {a, b}, {tick}, {tick, a}, {tick, b}, {tick, a, b} }

終了プロセスについて基本的に知っておく必要のあることは以上です。 しかし終了に関する例外的な状況を正しく区別するためには、再び拒否の定義を見直す必要が出てきます。 万全を期すために、例外的な状況についても見ておくことにします。

まず終了イベントと相互作用を表すイベントが混在する場合があり得ます。

SyncStitch 上では、このプロセスを状態遷移図として記述することはできません。 このような例外的な状況を誤って作らないように、終了イベント tick を直接使うことを禁止しているからです。 しかしプロセス式を使うと (alt SKIP (! aSTOP)) と表すことができます。 このプロセスではイベント a が必ず発生するとはいえません。 イベント a が提示されたとしても、それを無視して自発的に終了してしまうかもしれないからです。 強いて具体的な例を挙げるならば、シャットダウンの指示を出したあとに表示されるキャンセルボタンのようなものです。 キャンセルボタンを押すとシャットダウンがキャンセルされるかもしれないし、間に合わずにシャットダウンしてしまうかもしれないということです。

したがってこのプロセスはイベント a だけを要素にもつ集合 {a} を拒否します。 これを求める規則はないので、拒否の定義に追加します。 終了イベントの付いた遷移を持つ状態は、終了イベント tick を含まないすべてのイベントの集合を拒否するとします。 自発的に終了できるので、他のイベントが必ず発生するとはいえない、ということです。プロセス (alt SKIP (! a STOP)) の拒否集合は次のようになります。これは SKIP の拒否集合と同じです。

refusals((alt SKIP (! a STOP))) = { {}, {a}, {b}, {a, b} }

終了イベント tick と内部イベント tau が混在する場合もあり得ます。

このプロセスを T と呼ぶことにします。 プロセス T を作るには、イベント x を補助に使って次のようにします。 補助といっても特別な意味はありません。 tau 遷移を作ることだけが目的なので、他のところで相互作用を表すイベントとして使われていないものであれば、何でもかまいません。

(hide (list x)
  (alt SKIP (! x (! a STOP))))

この場合でもプロセスは自発的に終了する可能性があります。終了イベント tick と内部イベント tau はどちらも自発的に発生するので、このプロセスは非決定的選択に近いものです。実際、プロセス T は次のプロセスと同じであると考えられます。

このような現実に即した拒否集合を得るためには、終了イベントに関する規則を tau 遷移に関する規則よりも優先する必要があります。この修正をほどこした拒否集合の定義は次のようになります。

  • 安定状態の拒否集合は前に説明したとおりです。
  • tau 遷移を持つ状態のうち、終了イベント tick の付いた遷移を持たない状態は、拒否に関係しません。
  • 終了イベント tick の付いた遷移を持つ状態は、tick を含まないすべてのイベントの集合を拒否します。
  • 非決定的選択の拒否集合は、各分岐先の拒否集合を合わせたものです。

プロセス T の拒否集合は次のようになります。

refusals(T) = { {}, {a}, {b}, {a, b}, {tick}, {tick, b} }

8個あるイベントの集合のうち、含まれていないのは {a, tick} と {a, b, tick} です。 終了イベントは相互作用に関係するイベントではありませんが、イベントの集合 {a, tick} は「イベント a が発生するか、あるいは終了するかのどちらかであることは確かですか?」という問いだと考えることができます。 このイベントの集合が拒否ではないということは、問いの答えが「はい」であるということです。

トレース後のプロセス

ここまで見てきたプロセスの拒否集合は、プロセスの初期状態に対応する拒否集合です。 正確には初期状態から tau 遷移でたどり着くことのできる状態を集めたグループに対応する拒否集合です。 プロセスの外からは、このグループに属する状態を区別することができないので、グループ全体が1つの状態であるかのように見えます。 この状態グループの非決定性に関する性質は、グループに含まれる安定状態で決まります。

2つのプロセスを比較するときは、初期状態に対応する拒否集合だけでなく、イベントが発生した後の状態に対応する拒否集合についても比較を行う必要があります。 つまりプロセスの各トレースについて、トレースを実行した後の状態に対応する拒否集合を比較するということです。 あるトレースを実行した後にプロセスがいる可能性のある状態は、非決定性があるために1つとは限りません。 これをすべて集めた状態のグループを考えると、プロセスがグループに属するどの状態にいるのか外から区別することができません。 したがってあるトレースを実行した後にプロセスが持つ拒否集合は、グループに属する安定状態がすべて関係することになります。

次の図はプロセスがトレース (a b) を実行した後にいる可能性のある状態のグループを示したものです。 グループに属する状態のうち、黄色の状態は不安定状態、青の状態は安定状態です。 この例からもわかるように、グループに属する状態は、すべてが tau 遷移で直接つながっているとは限りません。 それでもどの状態にいるのか外からはわからないので、グループとしての拒否集合はすべての安定状態の拒否集合を合わせたものになります。

このような状況を表すために、新しい記号を導入します。 プロセス P のトレースを s とするとき、プロセスがトレース s を実行した後に示す動作を P / s と表します。 これをトレース後のプロセスといいます。 P / s は動作を表すので、それ自体もプロセスだと考えることができます。 状態で説明すると、トレース後のプロセス P/s は、トレース s を実行した後にプロセスがいる可能性のあるすべての状態を、非決定的選択で1つにまとめたものです。

例えば P = (! a (! b STOP)) とすると、P/(a) =(! b STOP) となります。次の例では状態が2つに分かれます。

(define-process Q
  (ndc
    (! a (! b STOP))
    (! a (! c STOP))))

トレース (a) の後にプロセス Q がたどり着く状態は2つあります。 1つはプロセス式 (! b STOP) で表される状態、もう1つはプロセス式 (! c STOP) で表される状態です。 どちらにいるかは非決定的なので、

Q / (a) = (ndc (! b STOP) (! c STOP))

となります。空のトレース () に対しては P/() = P です。

トレース後のプロセスを使うと、プロセス P がトレース s を実行した後の拒否集合を refusals(P/s) と表すことができます。

トレースと拒否によるプロセスが同じであることの条件

これでプロセスを比較する道具がすべてそろいました。 トレース集合と拒否集合を使ってプロセスが同じとはどういうことかということを定義します。

2つのプロセス P と Q が同じであるとは、次の2つ条件が両方成り立つことです。

  • 2つのプロセスのトレース集合が同じです。記号で書くと traces(P) = traces(Q) です。
  • プロセス P, Q のすべてのトレース s について、プロセス P がトレース s を実行した後のプロセス P/s の拒否集合と、プロセス Q が同じトレース s を実行した後のプロセス Q/s の拒否集合が同じです。記号で書くと refusals(P/s) = refusals(Q/s) です。

ただし、どちらのプロセスも発散を含んでいないものとします。 以後、単に2つのプロセスが同じといった場合には、この意味で同じであるとします。2つのプロセス P と Q が同じであることを P = Q と表します。

実装が仕様を満たす条件

仕様を表すプロセス SPEC と実装を表すプロセス IMP があるとき、プロセス IMP が仕様を満たしているという条件を次のように定義します。

  • プロセス IMP のトレースはすべてプロセス SPEC のトレースです。記号で書くと traces(IMP) ⊆ traces(SPEC) です。
  • プロセス IMP のすべてのトレース s について、プロセス IMP がトレース s を実行した後のプロセス IMP/s のすべての拒否は、プロセス SPEC が同じトレース s を実行した後のプロセス SPEC/s の拒否でなければなりません。 記号で書くと refusals(IMP/s) ⊆ refusals(SPEC/s) です。

この2つの条件が成り立つかどうか調べることを、トレースと拒否による比較と呼ぶことにします。この2つの条件が成り立つことを記号で次のように表します。

記号 ⊑ は実装が仕様を満たすという関係を表しています。 この関係は対称ではないので、対称ではない形の記号を使います。 形からわかるように、数学的には ≤ や ⊆ の親戚です。 ただ、条件で使われている ⊆ とは左辺と右辺が逆になっているので注意してください。 条件をみると、2つのプロセス P と Q が P ⊑ Q と Q ⊑ P を両方満たすことと、P=Q が成り立つことは同じ意味であることがわかります。

SyncStitch は2つのプロセス P と Q について P ⊑ Q が成り立つかどうか検査する機能を持っています。 条件が2つあるので、検査の結果、条件が成り立たない場合も2つあります。 1つ目の条件を満たさない場合はトレース違反です。 2つ目の条件を満たさない場合を拒否違反といいます。

2つ目の条件は2つの意味を持っています。 1つは仕様が非決定的選択を持っている場合に、どちらを選んで実装してもよいという意味です。 例えば仕様を表すプロセス P がプロセス Q と R の非決定的選択を持っている場合、P の拒否集合は Q の拒否集合と R の拒否集合を合わせたものです。 実装の拒否集合が仕様の拒否集合の部分でよいということは、Q の拒否集合だけ、あるいは R の拒否集合だけを持っていてもよいということです。

もう1つの意味は、仕様が拒否しないイベントの集合を実装が拒否してはならないということです。 これを受理で言い換えると、仕様が受理しなければならないとしたものを実装は受理しなければならないということです。 これはトレース比較の基準の元では仕様が強制することのできなかった条件です。 トレースと拒否を組み合わせると、実装がやってはいけないこと、やらなければいけないことを両方規定することができます。

例1

実装がイベント b の遷移を持っていません。しかしトレースは仕様の範囲内なので、トレース違反はありません。

イベント a が発生した後の拒否集合を見ると、次のようになっています。

refusals(SPEC / (a)) = { {}, {a} }
refusals(IMP / (a)) = { {}, {a}, {b}, {a, b} }

実装は仕様が拒否しないイベントの集合 {b}, {a, b} を拒否しているので拒否違反です。 仕様に非決定性がない場合は、トレースにあるイベントを拒否しないので、実装は必ず対応する遷移を持たなければなりません。

例2

仕様と実装は同じトレース集合 { (), (a), (b) } を持っています。

空のトレース () に対応する拒否は、それぞれ次のようになります。

refusals(SPEC) = { {} }
refusals(IMP) = { {}, {a}, {b} }

この場合も拒否違反があります。 仕様が非決定性を持たない場合、対応するイベントの遷移があるだけでなく、必ず発生するようにしなければなりません。

例3

実装はイベント b の遷移を持っていません。トレース違反はありません。

空のトレース () に対応する拒否は、それぞれ次のようになります。

refusals(SPEC) = { {}, {a}, {b} }
refusals(IMP) = { {}, {b} }

実装の拒否はすべて仕様の拒否なので、拒否違反もありません。 したがってこの実装は仕様を満たしています。 仕様に非決定的選択がある場合は、どれを実装してもよいという意味になります。

極大拒否集合と極小受理集合

拒否集合をコンパクトに表すための技として、極大拒否集合と極小受理集合というものを導入します。

アルファベットを Σ = {a, b, c, d} として、プロセス A を考えます。

拒否集合は次のようになります。

refusals(A) = { {}, {c}, {d}, {c, d} }

安定状態の拒否集合を求める規則からわかるように、プロセス A の拒否集合は、イベントの集合 {c, d} の部分集合をすべて集めたものです。 安定状態だけに限らず、一般にイベントの集合 X が拒否であれば、X の部分集合も拒否になります。提示するイベントを減らせば、イベントの発生する可能性が低くなるだけだからです。

拒否が持っているこの性質を使うと、イベントの集合 {c, d} だけを覚えておけば拒否集合を再現することができます。 このように拒否集合の中で他の拒否の部分集合になっていない拒否を極大拒否といいます。

極大拒否は1つとは限りません。例えばプロセス B を考えます。

拒否集合は次のようになります。

refusals(B) / Σ ={a, b, c, d} のとき

{}
{a}
{b}
{c}
{d}
{a, c}
{a, d}
{b, c}
{b, d}
{c, d}
{a, c, d}
{b, c, d}

このうち、他の拒否の部分集合になっていないものは2つあって、{a, c, d} と {b, c, d} です。 残りの拒否はすべて、このどちらかの部分集合になっています。

以上のことから、極大拒否をすべて集めたものを持っていれば、拒否集合が再現できることがわかります。 プロセスの拒否集合から極大拒否だけを選んですべて集めたものを極大拒否集合といいます。プロセス P の極大拒否集合を記号で RM(P) と表します。プロセス A, B の極大拒否集合はそれぞれ次のようになります。

RM(A) = { {c, d} }
RM(B) = { {a, c, d}, {b, c, d} }

極大拒否 X を考える代わりに、X に含まれていないすべてのイベントからなる集合を考えることもできます。 X に含まれていないイベントの集合とは、アルファベット Σ から X に含まれているイベントを取り除いた残りの集合です。 数学的にいうと X の補集合です。 これを極小受理といいます。 例えばプロセス A では、{c, d} が極大拒否なので、{a, b} が極小受理になります。 極大拒否の代わりに極小受理を集めておいても拒否集合を再現することができます。 すべての極小受理を集めた集合を極小受理集合といいます。 プロセス P の極小受理集合を記号で Am(P) と表します。

プロセス A, B の極小受理集合はそれぞれ次のようになります。 元の拒否集合と比較すると、とてもコンパクトになりました。

Am(A) = { {a, b} }
Am(B) = { {a}, {b} }

[注意] 極大拒否が他の拒否に含まれない拒否であるように、受理集合の中で、他の受理を部分集合として持たない受理を考えることができます。 これは上で定義した極大拒否の補集合とは異なります。 対称性からいえばこちらを極小受理というべきかもしれませんが、上で見たとおり極大拒否の補集合の方が役に立つので、極小受理という名前は極大拒否の補集合を表すために使います。

極大拒否集合と極小受理集合を使って、非決定性を持つ各プロセスについてまとめたものを表で示します。

非決定性を持つプロセスのまとめ 1 /Σ={a,b,c}

プロセス 拒否集合 極大拒否集合 極小受理集合
{}, {c} {c} {a,b}
{},{a},{b},{c},{a,c}, {b,c} {a,c},{b,c} {a},{b}
{},{b},{c},{b,c} {b,c} {a}
{},{a},{c},{a,c} {a,c} {b}
{},{a},{b},{c},{a,b},{a,c},{b,c},{a,b,c} {a,b,c} {}
{},{c} {c} {a,b}
なし なし なし

非決定性を持つプロセスのまとめ2 / Σ = {a,b,tick}

プロセス 拒否集合 極大拒否集合 極小受理集合
{}, {a}, {b},{a,b} {a,b} {tick}
{}, {a}, {b},{a,b} {a,b} {tick}
{}, {a}, {b}, {tick}, {a,b}, {b,tick} {a,b}, {b,tick} {a}, {tick}

極小受理集合による拒否違反の判定

SyncStitch はプロセスの比較で拒否違反を見つけたとき、拒否集合の代わりに極小受理集合を表示します。 そのとき、いちいち拒否集合に戻してから考えるのではなく、極小受理のままで考えられるようにしておくと便利です。 そこで、拒否違反があるかどうかを極小受理からを直に判定する方法を説明します。

仕様と実装の比較は対称ではないので、判定が必要な状況は限定されたものになります。 実装の拒否が仕様の拒否であることを判定するので、仕様の方はあらかじめ拒否集合を知っておく必要がありますが、実装の方は安定状態ごとに調べれば十分です。

すると判定する状況は次の図に示すような状況です。 仕様については極小受理集合がわかっているとします。これを Am とします。 一方、実装の方はある安定状態にいるとします。この安定状態から出ているすべての遷移に付いているイベントの集合を I とします。

実装プロセスが拒否違反をしているかどうか判定する方法は次のとおりです。 極小受理集合 Am に含まれる極小受理の中に、イベントの集合 I に含まれているものが1つでもあれば拒否違反はありません。 含まれているものがなければ拒否違反があります。

例えばプロセス B を仕様、右のプロセスを実装だとします。

このプロセスの初期状態では I={a} です。 プロセス B の極小受理は {a} と {b} で、前者は I と同じです。 したがって拒否違反はありません。

次にプロセス A を仕様だとします。 極小受理は {a, b} だけで、これは I に含まれていません。 したがって拒否違反があります。

この判定の方法が正しい理由を説明します。 拒否違反がないということは、実装の拒否がすべて仕様の拒否だということです。 実装は安定状態にいるので、拒否は Σ -I の部分集合です。 もし要素をいちばん多く含む拒否 Σ - I が仕様の拒否であれば、その部分集合もすべて含まれることになるので、実装のすべての拒否が仕様の拒否になります。 Σ - I が拒否であるということは、Σ - I を含む極大拒否 X があるということです。 この状況を図に示します。緑色の領域すべてが I です。 X は点線で囲まれた領域の中すべてです。Σ - I は X に含まれています。

これを逆から考えると Σ - X が I の部分集合だということです。 Σ - X は次の図で水色で示した領域です。 これは上の図の緑色で示した領域 I に含まれています。

X は極大拒否なので、Σ - X は極小受理です。 したがって拒否違反がないということは、 I に含まれる極小受理がある、ということです。

トレースと拒否によるプロセス比較のまとめ

トレースと拒否によるプロセス比較についてまとめておきます。

  1. プロセスにイベントの集合 X を提示したとき、X に含まれるいずれかのイベントが必ず発生するならば、X をプロセスの受理といいます。
  2. プロセスが持つすべての受理の集合を受理集合といいます。
  3. プロセスにイベントの集合 X を提示したとき、X に含まれるどのイベントも発生しない可能性があるならば、X をプロセスの拒否といいます。
  4. プロセスが持つすべての拒否の集合を拒否集合といいます。プロセス P の拒否集合を記号 refusals(P) で表します。
  5. 拒否集合を使うと非決定性を持つプロセスを区別することができます。
  6. 拒否集合を使うとイベントが必ず起こるという条件を表すことができます。
  7. 拒否集合は、状態遷移図の構成から規則によって求めることができます。
  8. 拒否集合を使っても、発散するプロセスを区別することはできません。
  9. プロセスが発生させる可能性のあるすべてのイベントの集合をアルファベットといいます。アルファベットを記号 Σ で表します。終了イベント tick を含める場合は、記号 Σ で表します。
  10. プロセス P がトレース s を実行した後の動作を表すプロセスを、トレース後のプロセスといいます。トレース後のプロセスを記号 P/s で表します。
  11. 2つのプロセスが同じであるとは、トレース集合が同じで、かつ各トレースを実行した後の拒否集合が同じということです。ただし発散する場合を除きます。
  12. 実装が仕様を満たす条件は、実装を表すプロセスのトレースが仕様を表すプロセスのトレースで、かつ各トレースを実行した後の実装の拒否集合が仕様の拒否集合に含まれていることです。仕様のプロセスを SPEC、実装のプロセスを IMP とするとき、実装が仕様を満たす条件を記号で SPEC ⊑ IMP と表します。
  13. 実装の拒否が仕様の拒否でない場合を拒否違反といいます。
  14. 拒否集合に含まれる拒否のうち、他のどの拒否にも含まれていないものを極大拒否といいます。
  15. 1つの拒否集合に含まれる極大拒否だけをすべて集めた集合を極大拒否集合といいます。極大拒否集合があれば元の拒否集合を求めることができます。極大拒否集合を使うと拒否集合をコンパクトに表すことができます。
  16. アルファベットから極大拒否に含まれるイベントをすべて除いた残りの集合を極小受理といいます。
  17. 1つの拒否集合に対応する極大拒否集合を考えたとき、これに含まれる各極大拒否に対応する極小受理をすべて集めた集合を極小受理集合といいます。極小受理集合があれば、元の拒否集合を求めることができます。極小受理集合を使うと拒否集合をコンパクトに表すことができます。
2013/09/03
© 2013,2014,2015 PRINCIPIA Limited