(57)【要約】【課題】  プロセス処理順序制御の安全性を実時間で容易に、確実に保障するプロセス処理順序制御方法を提供する。【解決手段】  完備束構造をなすベクトル注釈真理値（ｉ，ｊ）｛０≦ｉ，ｊ≦ｍ，  ｉ，ｊ，ｍは整数｝によって２つのプロセス間の時間的前後関係を数値化したbf-EVALP式を用いる。２つのプロセス間の時間的前後関係についての安全性規則を、ベクトル注釈真理値（ｉ０，ｊ０）を付した前件部と結論部からなるbf-EVALP式で予め表しておき、プロセスの進行に伴い増加したベクトル注釈真理値（ｉ，ｊ）が上記bf-EVALP式のベクトル注釈真理値（ｉ０，ｊ０）以上になったとき、結論部が推論されることにより、実時間で安全性検証を行いつつプロセス処理を実行する。【選択図】      図１
2008146430.tif 000002
【特許請求の範囲】
【請求項１】
逐次変化する複数のプロセス間の時間的前後関係を数値化し、パラコンシステント論理プログラムbf-EVALP (before-after Extended Vector Annotated Logic Program) に従ってプロセスの処理順序を検証しつつ制御することを特徴とするパラコンシステントプロセス処理順序制御方法。
【請求項２】
完備束構造をなすベクトル注釈真理値（ｉ，ｊ）｛０≦ｉ，ｊ≦ｍ、  ｉ，ｊ，ｍは整数｝によって上記複数のプロセス間の時間的前後関係を数値化したbf-EVALP式を含むことを特徴とする請求項１に記載するパラコンシステントプロセス処理順序制御方法。
【請求項３】
上記ベクトル注釈真理値（ｉ，ｊ）が、プロセスの経過とともに増加し、すべてのプロセスの終了とともに（０，０）にリセットされるものであることを特徴とする請求項２に記載するパラコンシステントプロセス処理順序制御方法。
【請求項４】
上記のプロセスが、所定の区間を時間的前後関係を持ちながら進行する第１の列車と第２の列車とであって、それらの列車の時間的前後関係についての安全性規則を、ベクトル注釈真理値（ｉ０，ｊ０）を付した前件部と結論部からなるbf-EVALP式で予め表しておき、列車の進行に伴い上記のように増加したベクトル注釈真理値（ｉ，ｊ）が上記bf-EVALP式のベクトル注釈真理値（ｉ０，ｊ０）以上になったとき、結論部が推論されることを特徴とする請求項３に記載のパラコンシステントプロセス処理順序制御方法。
【請求項５】
上記のプロセスが、ビール工場においてタンクを結ぶパイプラインを所定の順序・組み合わせで流れるビール、水、洗浄液などの液体を、混合・分離機能を有するバルブを経由して流すことであって、それらプロセスの時間的前後関係についての安全性規則をベクトル注釈真理値（ｉ０，ｊ０）を付した条件式（bf-EVALP式）で予め表しておき、プロセスの経過に伴い上記のように増加したベクトル注釈真理値（ｉ，ｊ）が上記条件式のベクトル注釈真理値（ｉ０，ｊ０）以上になったとき、プロセスが処理されることを特徴とする請求項３に記載のパラコンシステントプロセス処理順序制御方法。
【発明の詳細な説明】
【技術分野】
【０００１】
請求項に係る発明は、形式的安全性検証および安全性検証に基づく実時間でのプロセス処理順序制御方法に関するものである。
【背景技術】
【０００２】
全ての制御システムに於いてその安全性確保は最重要課題である。最近この安全性検証に、形式的（論理的）手法を導入する動きが欧米を中心に活発化している。ところがこの安全性検証についてはシステムを静的に捉え、古典論理の範囲で行われることが主流である。このような状況の中で、数年前に論争推論（defeasible reasoning）、義務概念と矛盾を扱えるパラコンシステント論理プログラムEVALP (Extended Vector Annotated Logic Program) を提案し、その特色を生かした制御システムの知的安全性検証（主として交通制御システム、パイプライン制御などの安全性検証）及びその制御への応用を研究してきた（非特許文献１）。
【０００３】
また、プロセス処理の時間的順序関係を動的に扱える明確な形式的理論がないこともあって、プロセス処理の順序制御については、人間による判断、単純な装置、コンピュータプログラムなどによる、安全性検証の伴わない制御が行われてきた。特許文献１のような列車制御方法もある。
【非特許文献１】Kazumi Nakamatsu and Jair M. Abe, Railway Signal and Paraconsisntency, Advances in Logic Based Iintelligent Systems, IOS Press, 2005
【特許文献１】特公平７−１０６７０４号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
現在、定着したプロセス処理順序制御方式はない。例えば、各々のプロセス処理は自動化されていたとしても、プロセスの開始・終了のタイミング制御及びその安全性検証については、制御パネルの表示、計画表等を見て人間が制御している所が多々存在する。特許文献１に記載の制御方法にしても、処理順序は制御するが、安全性検証は行わない。あるいは鉄道踏切遮断機制御などでは人間の判断が優先して遮断機を制御する踏切もあり、自動踏切だとしても単純な列車検知システムにだけ頼った制御を行っているのが現状である。いずれにせよ制御の安全性検証は行われていないと考えられる。このような状況で事実予期しない事故も発生している。
【０００５】
上記EVALPでは制御対象システム内で処理されるプロセスの時間的前後関係の安全性を動的に実時間で検証することが出来ない。例えば、化学プラントにおけるパイプラインシステムでは危険な化学反応を避けるため化学プロセス処理の順序を検証することが重要な問題になっている。このようなプロセス処理順序安全性検証を動的に行える扱いやすい論理体系は現在無いと考えられる。実際いくつかの区間時間を扱う時間論理体系は存在するが、これらは区間時間を静的対象として代数学的に扱うものであって、現実の動的制御には向いていない。当然、現実にはプロセス処理順序を扱える形式的安全性検証に基づく制御は行われてはいない。発明者は、このような経過において研究中、プロセス処理の順序関係を動的に扱えるbf-EVALP (before-after EVALP)と呼ぶEVALPを創作し、bf-EVALPに基づく動的プロセス処理順序安全性検証制御方式を発明した。
【０００６】
請求項に係る発明は、上述の点を考慮し、従来、人間や単純な装置などによって行われてきたプロセス処理順序制御の安全性を実時間で容易に、確実に保障するプロセス処理順序制御方法を提供するものである。
【課題を解決するための手段】
【０００７】
安全かつミスの無いようにプロセス処理順序制御を実施するには、時間的前後関係（順序関係）についての形式的安全性検証が容易な制御システムを構築することである。このため、プロセス処理時間の前後関係（before-after）が簡単に動的に扱えるパラコンシステント論理プログラムbf-EVALPを使って対象となるシステムに対しプロセス処理順序安全性検証論理モデルを構築した。
【０００８】
請求項1に記載のパラコンシステントプロセス処理順序制御方法は、逐次変化する複数のプロセス間の時間的前後関係を数値化し、パラコンシステント論理プログラムbf-EVALP (before-after Extended Vector Annotated Logic Program)に従ってプロセスの処理順序を検証しつつ制御することを特徴とする。
【０００９】
パラコンシステント論理プログラムbf-EVALPとは、義務概念と矛盾を表す注釈真理値を持つ論理プログラムであり、プロセス間の時間的前後関係を数値化して知識量として扱い、その時間的前後関係に関する事実・義務・許可などの概念や矛盾を推論する論理プログラムである。したがって、このようなbf-EVALPを利用し、逐次変化する複数のプロセス間の時間的前後関係を数値（整数値ベクトル）化して知識量として取り扱うことにより、簡単に動的にプロセス処理順序の安全性検証を実時間で行い、プロセス順序の制御をすることが可能になる。これらの知識は２つのプロセスの時間的前後関係を表す論理式Ｒに明示的に付帯する注釈真理値として表現され、bf-EVALPではこれらの注釈真理値は完備束構造をなす。
【００１０】
また、bf-EVALPではｎ個（ｎ≧３）のプロセスに対し、例えばプロセス１とプロセス２の時間的前後関係と、プロセス２とプロセス３の時間的前後関係とから、プロセス１とプロセス３の前後関係を推論できる。すなわち、多数のプロセス１，２，・・・，ｎの時間的前後関係を検証する場合、となり同士のプロセス間の時間的前後関係がすべて検証できれば、任意の２つのプロセス（たとえば、プロセス１とプロセス３）の時間的前後関係を知ることが出来る。従って、効率よくプロセス処理順序の安全性検証を行い、プロセス処理の順序制御をすることが可能になる。
【００１１】
請求項２に記載のパラコンシステントプロセス処理順序制御方法は、完備束構造をなすベクトル注釈真理値（ｉ，ｊ）｛０≦ｉ，ｊ≦ｍ，  ｉ，ｊ，ｍは整数｝によって上記複数のプロセス間の時間的前後関係を数値化したbf-EVALP式を含むことを特徴とする。
【００１２】
例えば、２つのプロセス間の時間的前後関係を表す論理式Ｒのベクトル注釈真理値（ｉ，ｊ）の第１成分ｉが２つのプロセスの時間的前後関係が「後」である知識量、第２成分ｊが「前」である知識量を表すとすると、ｉ，ｊが０または正整数であることから、時間的前後関係を離散的な整数値ベクトルで表現することが可能になる。従って、このようなプロセスの制御方法によれば、逐次変化するプロセスの、ある時点での時間的前後関係に基づき、あいまいさを残さずに推論することができ、その結果確実なプロセス処理順序制御が実現する。
【００１３】
請求項３に記載のパラコンシステントプロセス処理順序制御方法は、上記ベクトル注釈真理値（ｉ，ｊ）が、プロセスの経過とともに増加し、すべてのプロセスの終了とともに（０，０）にリセットされるものであることを特徴とする。
【００１４】
これにより、逐次変化する知識量を簡単なベクトル注釈真理値（ｉ，ｊ）の加算で追うことが可能になる。具体的には、たとえば、２つのプロセスPriとPrj間の時間的前後関係を次の４つの場面に分類し（図２参照）、その前後関係が逆の場合も含めて図１のような完備束を構成したとする。
（１）「プロセスPriがプロセスPrjの始まりより早く始まり、早く終わる」（注釈真理値db/da (discrete before/after)として表現され、ベクトル注釈真理値（０，７）／（７，０）と等価である。）
（２）「プロセスPriがプロセスPrjの始まりより早く始まり、プロセスPriの終了直後にPrjが始まる」（注釈真理値mb/ma (immediate before/after)として表現され、ベクトル注釈真理値（１，６）／（６，１）と等価である。）
（３）「プロセスPriがプロセスPrjの始まりより早く始まり、プロセスPrjの処理中に終わる」（注釈真理値jb/ja (joint before/after)として表現され、ベクトル注釈真理値（２，５）／（５，２）と等価である。）
（４）「プロセスPriがプロセスPrjの始まりより早く始まり、プロセスPrjの終わりより遅く終わる」（注釈真理値ib/ia (included before/after)として表現され、ベクトル注釈真理値（３，４）／（４，３）と等価である。）
【００１５】
２つのプロセスPriとPrjの開始前は、時間的前後関係についての知識量が何もない状態なので、ベクトル注釈真理値は（０，０）である。これは図１の完備束の最底部L0に位置する。
最初にプロセスPriが始まったとき、２つのプロセスがこれ以降どのような時間的前後関係になるか不明でも、ベクトルの第２成分に４を加えてベクトル注釈真理値を（０，４）とすればその時点での事実に基づく２つのプロセス間の時間的前後関係を表現できる。この位置は図１の完備束上では注釈真理値beとして表され、この位置からはプロセスの時間的前後関係に関する知識量が増えるに従って完備束の左半分にあるdb，mb，jb，ibのいずれにも到達可能となる。
次にプロセスPrjが始まったとする（図２(ｃ)または(ｄ)）。この情報は、この時点で２つのプロセスのどちらが先に終了するかがわからなくても、ベクトルの第１成分に２を加え、ベクトル注釈真理値を（２，４）とすることによって表現できる。完備束上でこの位置L1からはjb，ibに到達可能である。この時点では２つのプロセスPri, Prjの時間的前後関係はjb またはibの何れかとなることがわかっている。もし、プロセスPriが先に終了すればjb（図２(ｃ)の時間的前後関係）、逆にプロセスPrjが先であればib（図２(ｄ)の時間的前後関係）となる。
そして、２つのプロセスPriとPrjが共に終了したときにそれらの時間的前後関係を表すベクトル注釈真理値は（０，０）となる。
プロセスPrjとその次のプロセスPrkに対しては同様にしてプロセスPrjとPrkの時間的前後関係が推論でき、安全性検証を行うことができる。また、これとは反対に最初にプロセスPrjが始まったときは、ベクトルの第１成分に４を加えてベクトル注釈真理値を（４，０）とする。この位置は図１の完備束上では注釈真理値afとして表され、この位置からはプロセスの時間的前後関係に関する知識量が増えるに従って、ベクトル注釈真理値（ｉ，ｊ）の各成分が上記の場合の逆になり、完備束の右半分にあるda，ma，ja，iaのいずれにも到達可能となる。
【００１６】
このように、ある時点でのプロセスの経過情報が入力されたときに、その後２つのプロセスがどのような時間的前後関係になったとしても、整数値加算のみで対応するので、実時間で簡単にしかも確実に安全性検証を行うことができる。
プロセスPriとPrjの時間的前後関係は、上記（１）〜（４）の４つの場合に限られるものではなく、さらに細かい分類をすることも可能である。
【００１７】
請求項４に記載のパラコンシステントプロセス処理順序制御方法は、上記のプロセスが、所定の区間を時間的前後関係を持ちながら進行する第１の列車と第２の列車とであって、それらの列車の時間的前後関係についての安全性規則を、ベクトル注釈真理値（ｉ０，ｊ０）を付した前件部と結論部からなるbf-EVALP式で予め表しておき、列車の進行に伴い上記のように増加したベクトル注釈真理値（ｉ，ｊ）が上記bf-EVALP式のベクトル注釈真理値（ｉ０，ｊ０）以上になったとき、結論部が推論されることを特徴とする。
【００１８】
ここでいうbf-EVALP式とは、例えば式[１]のようにプロセス間の時間的前後関係を表す論理式Ｒを含むものを言う。
R(Pri,Prj,t):[(0,4),α]→Cross(t):[cl,β]    ―――  [1]
式[１]は、鉄道踏切遮断機において、安全性を保障するための安全性規則「時刻ｔにおいて、踏切区間に列車が存在しなくなるまで遮断機は閉めるべきである」を、図１の完備束を構成するベクトル注釈真理値を用いたbf-EVALP式で表したものである。Priは先行する第１の列車、Prjは後続の第２の列車、Crossは遮断機、clは「閉じる」というアクションを表している。また、αは事実、βは義務を表す注釈真理値である。ベクトル注釈真理値の順序関係（大小）は、知識量の多少に基づいており図１の完備束における上下の位置関係に対応している。例えば、db, mb, jb, ib, ia, ja, ma, daは同じ知識量であるがbe, afはそれらより少ない知識量である。
【００１９】
例えば、図３のような踏切区間に第１の列車が進入する前は、ベクトル注釈真理値は（０，０）（図１のL0）で、式１の前件部にあるベクトル注釈真理値（０，４）(図１のbe）より小さい（同図で下方に位置する）ため、結論部が推論されない。したがって、遮断機は開いている。その後、第１の列車が踏切区間に進入することにより、ベクトル注釈真理値が（０，４）（図１のbe）となり、式１の前件部のベクトル注釈真理値（０，４）以上となるので、結論部が推論され、遮断機が閉じる。ここで第２の列車が踏切区間に進入すると、ベクトル注釈真理値が（２，４）（図１のL1）となり、式１の前件部のベクトル注釈真理値（０，４）（図１のbe）以上（同図において上方）なので、結論部が推論される。したがって、このとき遮断機は閉じたままである。その後、第１の列車だけが先に踏切区間を出たとしてもベクトル注釈真理値は（２，５）（図１のjb）となり、遮断機は閉じたままである。（現行の踏切制御では同じ踏切区間に２つの列車が進入することは考えにくいが、仮にあったとして、このような場合、第１の列車が踏切区間を出た時点で、第２の列車が区間内に存在するにも関わらず、遮断機は開かれ安全は保障されない。）さらにその後、後続の列車も踏切区間を通過すると、ベクトル注釈真理値は（０，０）（図１のL0）に戻るので、式１の前件部のベクトル注釈真理値より小さくなり、結論部が推論されない。したがって、遮断機は開くことになる。もしここで、第２の列車の後第３の列車が進行している場合、第２と第３の列車の時間的前後関係をベクトル注釈真理値（ｉ，ｊ）を用いて表現すれば同様の安全性検証が行える。
このように、前件部のベクトル注釈真理値（ｉ，ｊ）の各成分が簡単な整数値であるため、２つの列車がどのような時間的前後関係で進行しても、あいまいさを残さずに推論ができる。したがって、確実に安全性検証を行いながらプロセス制御（列車運行に基づく踏切制御）を実行できる。ここでは、踏切遮断機制御の安全性検証を例示しているが、鉄道連動（信号やポイントの切り替え）についての安全性検証にも適用可能である。
【００２０】
請求項５に記載のパラコンシステントプロセス処理順序制御方法は、上記のプロセスが、ビール工場（または同様の、飲料等の液体製品の工場）においてタンクを結ぶパイプラインを所定の順序・組み合わせで流れるビール（または飲料等の液体製品。以下同様）、水、洗浄液などの液体を、混合・分離機能を有するバルブを経由して流すことであって、それらプロセスの時間的前後関係についての安全性規則をベクトル注釈真理値（ｉ０，ｊ０）を付した条件式（bf-EVALP式）で予め表しておき、プロセスの経過に伴い上記のように増加したベクトル注釈真理値（ｉ，ｊ）が上記条件式のベクトル注釈真理値（ｉ０，ｊ０）以上になったとき、プロセスが処理されることを特徴とする。
【００２１】
ここでいうプロセスとは、たとえば図４のように構成された４個のタンクT0，T1，T2，T3、５本のパイプPi0，Pi1，Pi2，Pi3，Pi4および混合・分離機能を有する２個のバルブV0，V1の場合では、ビール処理プロセスPr0（タンクT0からバルブV0を経由してタンクT1にビールを送る）とPr3（２つのタンクT0とT3にあるビールをバルブV0で混合してタンクT1とT2に送る）、洗浄プロセスPr1（タンクT3にある洗浄液をバルブV1，V0経由でタンクT2に送る）とPr2(タンクT3にある水をバルブV1，V0経由でタンクT2に送る)である。また、この場合の条件式（bf-EVALP式）とは
１．  〜Ｒ(Pr1,Pr0,t):[(0,4),α]∧
〜Ｒ(Pr2,Pr0,t):[(0,4),α]∧
〜Ｒ(Pr3,Pr0,t):[(0,4),α],
２．  Ｒ(Pr1,Pr0,t):[(0,4),α]∧
〜Ｒ(Pr1,Pr0,t):[(3,4),α],
３．  Ｒ(Pr1,Pr2,t):[(0,6),α]∧
〜Ｒ(Pr1,Pr2,t):[(0,7),α],
４．  Ｒ(Pr0,Pr3,t):[(0,6),α]∧
Ｒ(Pr2,Pr3,t):[(0,6),α]
をいう。
【００２２】
ここで、条件式中に現れる記号（〜）は存在論的否定であり、たとえば、条件式１の第１項は「プロセスPr1がプロセスPr0より早く始まったという事実は存在しない」という意味に解釈される。このように解釈すると、これら条件式は、上記の４つのプロセスが、図５で示される順序で処理されるべきだと考えることにより生じる安全性条件であり、各プロセスの開始前に検証される。意味はそれぞれ、
１．  プロセスPr0はどのプロセスより先に処理される。
（条件式の直接の解釈は、
プロセスPr1がプロセスPr0より先に始まった、
プロセスPr2がプロセスPr0より先に始まった、
プロセスPr3がプロセスPr0より先に始まった
という事実が存在しない）
２．  プロセスPr1はプロセスPr0の開始後に始まる。
（条件式の直接の解釈は、
プロセスPr0がPr1より先に始まった事実が存在し、
すでにプロセスPr1が（プロセスPr0より先に）終わった事実が存在しない）
３．  プロセスPr2はプロセスPr1の終了直後に始まる。
（条件式の直接の解釈は、
プロセスPr1はプロセスPr2の開始前に終了した事実が存在し、
プロセスPr2はプロセスPr1の終了直後には始まらなかったという事実が存在          しない）
４．  プロセスPr3は２つのプロセスPr0，Pr2が共に終了後に始まる。
（条件式の直接の解釈は、
プロセスPr0はプロセスPr3の開始前に終了した、
プロセスPr2はプロセスPr3の開始前に終了した
事実が存在する）
この第４の条件式では、プロセスPr0とPr3、プロセスPr2とPr3の時間的前後関係はベクトル注釈真理値(１，６)（図１のmb）または(０，７)（図１のdb）で表されていれば、プロセスPr0，Pr2は共にPr3開始前に終了していることが表される。これはベクトル注釈真理値としては（０，６）（図１のL2）以上であればよいことになるので、条件式中ではベクトル注釈真理値としては（０，６）として記述されている。
【００２３】
このような条件式のベクトル注釈真理値（ｉ０，ｊ０）に対し、プロセスの進行と共に上記のように変化するベクトル注釈真理値の大小を比較し、後者が前者以上であるときに、処理順序の安全性が検証されたものとして、そのプロセス処理が実行される。
上記の鉄道遮断機の制御と同様、実時間でプロセスの安全性を確実に検証しつつ、プロセス処理順序制御を行うことができる。
【発明の効果】
【００２４】
請求項１に係るパラコンシステントプロセス処理順序制御方法であれば、論理的手法（複数のプロセス間の時間的前後関係（処理順序）を実時間で数値化して知識量として扱う手法）であるが故に安全性検証に基づく制御が行え、自律制御システムのみならず人間の制御サポートシステムも容易に構築可能となる。
【００２５】
請求項２に係るパラコンシステントプロセス処理順序制御方法であれば、逐次変化する複数のプロセス間の時間的前後関係をあいまいさを残さずに数値化し、プロセス処理の順序制御を実時間で確実に行うことができる。
【００２６】
請求項３に係るパラコンシステントプロセス処理順序制御方法は、さらに、簡単な整数値加算のみで複数のプロセス間の時間的前後関係に対応するので、プロセス処理の順序制御を実時間で確実、簡単に行える。
【００２７】
請求項４に係るパラコンシステントプロセス処理順序制御方法であれば、複数の列車の逐次変化する時間的前後関係の安全性検証を実時間で確実に、簡単に行えるので、列車運行に基づく踏切制御を安全かつ確実に実行できる。
【００２８】
請求項５に係るパラコンシステントプロセス処理順序制御方法によれば、ビール工場におけるビール、水、洗浄液などの液体を流す時間的前後関係を、実時間で確実に、簡単に行えるので、安全性を検証しながらプロセス処理を実行できる。
【発明を実施するための最良の形態】
【００２９】
以下、図１〜図６に基づき、本発明によるパラコンシステントプロセス処理順序制御方法の実施形態について説明する。図１はベクトル注釈真理値（ｉ，ｊ）の要素で構成される完備束構造を示す図で、図２は、２つのプロセスの時間的前後関係を模式的に示す説明図である。
【００３０】
一般にパラコンシステント注釈真理値付き論理プログラムでは各リテラルには注釈真理値と呼ばれる真理値が明示的に付加されており、これらが完備束構造をなしている。この注釈真理値の完備束構造によって矛盾を含む多くの知識構造の表現・取り扱いが可能になる。EVALPでは注釈真理値が
[（ｉ，ｊ），μ]
という複合ベクトルの形をしている。ここで、ｉはこの注釈真理値が付加されるリテラルを正(肯定的)に支持する知識量を表し、ｊ は負(否定的)に支持する知識量を表している。０≦ｉ，ｊ≦ｍ（ｉ，ｊ，ｍは自然数）であり、μ∈｛α，β，γ｝は義務などの様相を表す注釈真理値である。αはそれが付加されるリテラルが事実、βは義務、γは非義務であることを示す指標となる。これらの指標によって義務概念（義務、許可、禁止）と事実を知識として取り扱えるようになっている。
【００３１】
このEVALPにおいて２つのプロセス間の時間的前後関係が扱えるようにするために、ベクトル注釈真理値（ｉ，ｊ）の第１成分ｉは２つのプロセスPriとPrjの時間的前後関係が後（After）である知識量、第２成分ｊは前（Before）である知識量を表現するものとした。この時、プロセスの時間的前後関係を表す知識量は次に述べるようなベクトル注釈真理値によって表現される。まず、プロセスの時間的前後関係を整理し、次の４つの場合に分類した。
【００３２】
（１）「プロセスPriがプロセスPrjの始まりより早く始まり、早く終わる」（図２(ａ)参照）
（２）「プロセスPriがプロセスPrjの始まりより早く始まり、プロセスPriの終了直後にPrjが始まる」（mb, ma）（図２(ｂ)参照）
（３）「プロセスPriがプロセスPrjの始まりより早く始まり、プロセスPrjの処理中に終わる」（jb, ja）（図２(ｃ)参照）
（４）「プロセスPriがプロセスPrjの始まりより早く始まり、プロセスPrjの終わりより遅く終わる」（ib, ia）（図２(ｄ)参照）
【００３３】
２つのプロセスPri，Prjの時刻ｔにおける時間的前後関係を述語R(Pri,Prj,t)と注釈真理値を用いてbf-EVALP式で表現すると、
・   R(Pri,Prj,t):[(0,7),α]  （「時刻tにおいてプロセスPriとプロセスPrjは（１）の関係（discrete before）（db）にあることは事実である。」ことを表現している。）またプロセスPriとPrjを入れ替えると、R(Prj,Pri,t):[(7,0),α]（discrete after）（da）の関係となる。
・  R(Pri,Prj,t):[(1,6),α]（「時刻tにおいてプロセスPriとプロセスPrjは（２）の関係（immediate before）（mb）にあることは事実である。」ことを表現している。）同様にR(Prj,Pri,t):[(6,1),α] （immediate after）（ma）でもある。
・  R(Pri,Prj,t):[(2,5),α]（「時刻tにおいてプロセスPriとプロセスPrjは（３）の関係（joint before）（jb）にあることは事実である。」ことを表現している。）同様にR(Prj,Pri,t):[(5,2),α] （joint after）（ja）でもある。
・  R(Pri,Prj,t):[(3,4),α]（「時刻tにおいてプロセスPriとプロセスPrjは（４）の関係（included before）（ib）にあることは事実である。」ことを表現している。）同様にR(Prj,Pri,t):[(4,3),α] （included after）（ia）でもある。
のように表現できる。またプロセスPriとプロセスPrjの関係を逆方向から見るとbeforeでなくafterの関係が得られ、ベクトル注釈真理値も第１、第２成分を交換したものが得られる。
【００３４】
これらのベクトル注釈真理値（ｉ，ｊ）を完備束構造で表現したものが、図１である。前述していない図中の記号とベクトル注釈真理値との対応は、before---(0,4)（「プロセスPriがプロセスPrjより先に始まった。」を表現する。）、after---(4,0)（「プロセスPrjがプロセスPriより先に始まった。」を表現する。）となる。ベクトル注釈真理値を図１のような完備束に限定したEVALPをbf-EVALPと名付けている。ただし、時間的前後関係の分類は４つに限られるものではなく、さらに細かい分類にすることも可能である。その場合、完備束の格子点は図１の格子点（８×８）より多くなる。
【００３５】
次にベクトル注釈真理値の評価、推論について述べる。ベクトル間の順序関係は
X1≦X2, Y1≦Y2  ⇔  (X1,Y1) ≦ (X2,Y2)
として定義されるので、例えば、センシング情報として２つのプロセスPr1，Pr2の時間的前後関係としてbf-EVALP式
R(Pr1,Pr2,t):[(3,4),α]
を得たとする。(0,4)≦(3,4)となるので、bf-EVALP式
R(Pr1,Pr2,t):[(0,4),α]
は成り立つが、(0,6)≦(3,4)とはならないので、bf-EVALP式
R(Pr1,Pr2,t):[(0,6),α]
は成り立たない。同様にしてβ(義務)≦α(事実)とはならないので（義務、非義務、事実は互いに独立と考えるのでこれらの概念の間には順序関係≦は成り立たないということ）、例えば、bf-EVALP式
R(Pr1,Pr2,t):[(0,4),β]
などは成り立たない。
【００３６】
このbf-EVALPを利用したパラコンシステントプロセス処理順序制御方法を、簡単な鉄道踏切制御とビール工場パイプラインのプロセス順序検証制御に適用した。その詳細を以下に述べる。
【００３７】
（１）
鉄道踏切警報遮断機制御（PCシミュレーション実施済）、化学プラント、原子力発電所等におけるパイプライン制御など考えられる応用範囲は広いと思われるが、実際に２００５年３月に岡山県内ＪＲ西日本山陽本線で起きた踏切内での列車と踏切横断車とのニアミス事故の状況に基づき解説する。この事故は、踏切区間内に２つの列車が続けて進入したため先行列車が区間を出た後、後続列車が区間内にいるにもかかわらず遮断機が上がりニアミス事故が起きた。ここで踏切区間とは、踏切警報遮断機を作動開始させる列車センサーの設置位置から作動終了させるセンサーの設置位置までを言う。
【００３８】
bf-EVALP制御方式でどのように安全性を確保するかをステップごとに示す。この方式では論理的に安全性が検証されれば遮断機を開き、そうでなければ閉じるという制御を行っている（制御のための構成としては、後述する図６のようなシステム１０が考えられる）。
【００３９】
ここで、図３に示すような踏切警報遮断機１のある踏切区間２内に矢印の方向から列車が入るとその列車プロセスが開始し、出るとその列車プロセスが終了すると考える。列車プロセスの開始は、列車センサーＡ１により検知し、列車プロセスの終了は列車センサーＡ２によって検知する。このニアミス事故では先行列車プロセスPriと後続列車プロセスPrjが図２（ｃ）のように時間的重なりがあったと考えられる。
まず、安全性を保障するための安全性規則
『踏切区間に列車が存在しなくなるまで遮断機は閉めるべきである。』
を想定し、bf-EVALP式に変換し、この式を基準にbf-EVALPの推論機能を利用した論理検証を行うことになる。この安全性基準はbf-EVALP式
R(Pri,Prj,t):[(0,4),α]→Cross(t):[cl,β]    ―――  [1]
によって表現される。
【００４０】
［ステップ１］
初期状態として踏切区間２に列車プロセスが全く存在しないときを仮定すると、
R(Pri,Prj,t):[(0,0),α]    ―――  [2]
だけが成り立つ。このbf-EVALP式[2]は２つのプロセスPri,Prjの時間的前後関係についてはどちらが先とも後ともいう情報が全くない（注釈真理値が(0,0)である）ことを示している。[1]式中の前件部内と[2]式のベクトル注釈真理値を比較すると、(0,0)≦(0,4)となり、[1],[2]式より[1]式の結論部Cross(t):[cl,β]「時刻tにおいて踏切は閉じるべきだ」という義務が推論されないので、遮断機１は開くように制御される。
【００４１】
［ステップ２］
この状態から先行列車が踏切区間２に進入し、プロセスPriが始まる（これは図２(ｃ)中、時刻Xsに踏切区間２入り口で列車センサーＡ１により列車が検知されることによって信号が入る）と次の後続列車プロセスPrjより先（before）であることは事実であるからそのことを表す
R(Pri,Prj,Xs):[(0,4),α]     ―――  [3]
というbf-EVALP式が得られる。この時点（Xs）において[1],[3]式より、「その時、踏切は閉じるべきである」という義務論理式Cross(Xs):[cl,β]が推論され、遮断機１が閉まるように制御される。[1],[3]式中のベクトル注釈真理値の関係は(0,4)≦(0,4)となるからである。
【００４２】
［ステップ３］
次に先行列車が踏切区間２を出る以前に後続列車が踏切区間２に入り後続列車プロセスPrjが始まる（図２(ｃ)中、時刻Ysに踏切区間２入り口で再度列車センサーＡ１により列車が検知される）と、後続列車プロセスPrjが先行列車プロセスPriの終了以前に始まったので、「先行列車プロセスPriが後続列車プロセスPrjよりただ先（before）である事実」情報を表すベクトル注釈真理値(0,4)に、その反対に少しだけ後（after）の情報を表すベクトル注釈真理値(2,0)が加えられる。そして、
R(Pri,Prj,Ys):[(2,4),α]     ―――  [4]
というbf-EVALP式が得られる。この時点（Ys）においても[1],[4]式より、義務論理式Cross(Ys):[cl,β]が推論される。したがって遮断機１は閉まるように制御される。[1],[4]式中のベクトル注釈真理値の関係は(0,4)≦(2,4)となるからである。
【００４３】
［ステップ４］
また、現実のニアミス事故の中で踏切遮断機が開いてしまった先行列車プロセスPriの終了時刻（Xf）においては
R(Pri,Prj,Xf):[(2,5),α]     ―――  [5]
というbf-EVALP式が得られる。[5]式は先行列車プロセスPriと後続列車プロセスPrjの時間的前後関係がこの時点（Xf）においても[1],[5]式より、義務論理式Cross(Xf):[cl,β]が推論され、bf-EVALP制御では安全性が検証されず遮断機１は上がらない。ここでは、先行列車プロセスPriが後続列車プロセスPrjが終了する前に終わってしまった事実（列車センサーＡ２により検知される）を踏まえてベクトル注釈真理値(2,4)にベクトル注釈真理値(0,1)が加えられ(2,5)となる。この場合も、[1],[5]式中のベクトル注釈真理値の関係は(0,4)≦(2,5)となる。
【００４４】
［ステップ５］
最終的に、後続列車プロセスPrjが終了すると、その時点で踏切区間２内に他に列車が存在しなければ
R(Pri,Prj,Yf):[(0,0),α]     ―――  [6]
というbf-EVALP式が得られる。[1],[6]式からは義務論理式Cross(Yf):[cl,β]が推論されないので遮断機１は開かれることになる。さらに後続の列車が踏切区間２内にすでに存在する場合は、２番目の列車プロセスPrjと３番目の列車プロセスPrkとの間の時間的前後関係R(Prj,Prk,t)に基づき制御がなされることになる。
【００４５】
（２）
次にビール工場のパイプライン制御に発明のパラコンシステントプロセス処理順序制御方法を用いた場合の実施例を、図１、図４および図５に基づき説明する。図４は、ビール工場のタンクやパイプラインを模式的に示す説明図で、図５は、図４のタンクやパイプラインを流れるビール、水、洗浄液の時間的前後関係を、模式的に示す説明図である。ビール工場ではパイプライン洗浄のために苛性ソーダと硝酸が利用されることがある。これら混合されると危険な液体のプロセス順序は厳密に守られなければならない。ここでは図４のような簡単なパイプラインを例に取りbf-EVALPによる順序制御を紹介する。
【００４６】
このパイプラインは4個のタンク｛T0, T1, T2, T4｝、5本のパイプ｛Pi0, Pi1, Pi2, Pi3, Pi4}、2個のバルブ{V0, V1}から構成されている。バルブは縦横方向に流れるそれぞれの液体を混合するか分離するかで制御を行う。このパイプラインを利用するビール処理プロセスPr0（タンクT0からバルブV0を経由してタンクT1にビールを送る）とPr3（２つのタンクT0とT3にあるビールをバルブV0で混合してタンクT1とT2に送る）、洗浄プロセスPr1（タンクT3にある洗浄液をバルブV1,V0経由でタンクT2に送る）とPr2(タンクT3にある水をバルブV1,V0経由でタンクT2に送る)が図５で示される順序で処理されるべきだと考えると、次のような安全性条件が生じる。
【００４７】
１． 最初にプロセスPr0が処理される。
（プロセスPr0，Pr3と並行にプロセスPr1，Pr2が処理される。）
２．プロセスPr1はPr0の処理開始後に処理される。
３． プロセスPr1が処理終了するとすぐにプロセスPr2が処理される。
４． プロセスPr1とPr2が終わるのを待ってプロセスPr3が処理される。
【００４８】
この時、条件１から４は次のbf-EVALP式で表現され、制御検証に利用される。つまり１，２，３，４の条件式が満たされれ（成り立て）ばそれぞれプロセスPr0, Pr1, Pr2, Pr3の処理許可が出されることになる。
【００４９】
１． 〜R(Pr1,Pr0,t):[(0,4),α]∧〜R(Pr2,Pr1,t):[(0,4),α]∧ 
〜R(Pr3,Pr1,t):[(0,4),α],
２． R(Pr0,Pr1,t):[(0,4),α]∧〜R(Pr0,Pr1,t):[(3,4),α],
３． R(Pr1,Pr2,t):[(1,6),α],
４． R(Pr0,Pr3,t):[(0,6),α]∧R(Pr2,Pr3,t):[(0,6),α]
【００５０】
ここで、１の条件式中に現れる記号（〜）は存在論的否定であり、例えば第1項は「プロセスPr1がプロセスPr0より先に始まったという事実が存在しない」という意味に解釈される。また３では、プロセスPr0, Pr2とプロセスPr3の関係はプロセスPr0, Pr2の両方が終わってからプロセスPr3が始まる（この前後関係はベクトル注釈真理値としては(1,6)または(0,7)として表されるので、注釈真理値としては(0,6)以上の情報があればいずれにせよ２つのプロセスPr0, Pr2は先に終了していることになる。）ことを示している。２の条件式ではプロセスPr0が先に始まってはいるが、プロセスPr1が先に終了していないことを表している。制御検証プロセスを具体的に示す。
【００５１】
[ステップ  1]
どのプロセスも処理が始まっていない時点t0では、bf-EVALP式
R(Pr0,Pr1,t0):[(0,0),α]，
R(Pr0,Pr2,t0):[(0,0),α]，
R(Pr0,Pr3,t0):[(0,0),α]，
R(Pr1,Pr2,t0):[(0,0),α]，
R(Pr1,Pr3,t0):[(0,0),α]，
R(Pr2,Pr3,t0):[(0,0),α]，
の前後関係が成り立つ。ベクトル注釈真理値(0,0)は対象となるプロセスの間の前後関係については肯定情報（第1成分によって表される０）も否定情報（第2成分によって表される０）もないことを表している。従って、１の条件式は満たされることになってプロセスPr0の処理許可が出る。ところが、２，３，４の条件式は満たされないので、プロセスPr1の処理許可は出ないことになる。このようにこの時、処理許可が出るのはプロセスPr0のみである。
【００５２】
[ステップ  ２]
プロセスPr0がすでに開始されていると、この時点t1では、bf-EVALP式
R(Pr0,Pr1,t1):[(0,4),α]，
R(Pr0,Pr2,t1):[(0,4),α]，
R(Pr0,Pr3,t1):[(0,4),α]，
R(Pr1,Pr2,t1):[(0,0),α]，
R(Pr1,Pr3,t1):[(0,0),α]，
R(Pr2,Pr3,t1):[(0,0),α]，
の前後関係が成り立つ。従って、１と２の条件式だけが満たされ、プロセスPr1の処理許可が出る。（プロセスPr0は処理中で許可が出る。）
【００５３】
[ステップ  ３]
プロセスPr0に続きプロセスPr1が始まると、この時点t2では、bf-EVALP式
R(Pr0,Pr1,t2):[(2,4),α]，
R(Pr0,Pr2,t2):[(0,4),α]，
R(Pr0,Pr3,t2):[(0,4),α]，
R(Pr1,Pr2,t2):[(0,4),α]，
R(Pr1,Pr3,t2):[(0,4),α]，
R(Pr2,Pr3,t2):[(0,0),α]，
の前後関係が得られるが、１と２の条件式は満たされるが、３と４の条件式は満たされないので、プロセスPr2, Pr3には処理許可が出されない。
【００５４】
[ステップ  ４] 
プロセスPr1が終了すると（プロセスPr0はまだ処理中）、この時点t3では、bf-EVALP式
R(Pr0,Pr1,t3):[(3,4),α]，-----[7]    
R(Pr0,Pr2,t3):[(0,4),α]，
R(Pr0,Pr3,t3):[(0,4),α]，
R(Pr1,Pr2,t3):[(0,6),α]，-----[8]
R(Pr1,Pr3,t3):[(0,6),α]，-----[9]
R(Pr2,Pr3,t3):[(0,0),α]，
の関係が得られる。プロセスPr2, Pr3は始まっていないので第4,5式[8]，[9]のベクトル注釈真理値は(0,6)である。Pr2,,Pr3がすぐに開始されれば(1,6)となり、そうでなければ(0,7)となる。何れにせよこの時点では(0,6)の情報は存在する。従って、３の条件式が満たされプロセスPr2の処理許可が出される。またプロセスPr1はすでに終了しているので、[7]式が２の条件式を満たさないため処理許可が出ず、プロセスPr0は処理中なので許可が出る。
【００５５】
[ステップ  ５]
プロセスPr2が処理許可されすぐに開始されると（プロセスPr0はまだ処理中）、この時点t4では、bf-EVALP式
R(Pr0,Pr1,t4):[(3,4),α]，
R(Pr0,Pr2,t4):[(2,4),α]，
R(Pr0,Pr3,t4):[(0,4),α]，
R(Pr1,Pr2,t4):[(1,6),α]，
R(Pr1,Pr3,t4):[(0,7),α]，
R(Pr2,Pr3,t4):[(0,4),α]，
の前後関係が得られる。従って、２と４の条件式は満たされないのでプロセスPr3とすでに終了したプロセスPr1は処理許可が出されない。
【００５６】
[ステップ  ６]
プロセスPr0がプロセスPr2の終了前に終了すると、この時点t5では、bf-EVALP式
R(Pr0,Pr1,t5):[(0,0),α]，-----[10]
R(Pr0,Pr2,t5):[(2,5),α]，
R(Pr0,Pr3,t5):[(0,6),α]，
R(Pr1,Pr2,t5):[(1,6),α]，
R(Pr1,Pr3,t5):[(0,7),α]，
R(Pr2,Pr3,t5):[(0,4),α]，
の前後関係が得られる。プロセスPr0, Pr1は両方が終了しているのでこの時点ではそれらの前後関係については[10]式のように情報がなくなる。従って、この時点では3の条件式以外満たされなくなり処理中のプロセスPr2以外のプロセスPr0, Pr1, Pr3は処理許可が出されない。
【００５７】
[ステップ  ７]
プロセスPr2が終了すると（プロセスPr0はすでに終了）、この時点t6では、bf-EVALP式
R(Pr0,Pr1,t6):[(0,0),α]，
R(Pr0,Pr2,t6):[(0,0),α]，
R(Pr0,Pr3,t6):[(0,7),α]，
R(Pr1,Pr2,t6):[(0,0),α]，
R(Pr1,Pr3,t6):[(0,7),α]，
R(Pr2,Pr3,t6):[(0,6),α]，
の前後関係が得られる。従って、ここで初めて４の条件式が満たされ、最後のプロセスPr3は処理許可が出される。他の３つのプロセスについてはすでに終了していて１，２，３の条件式が満たされないので処理許可は出ない。そして最後のプロセスPr3も終了するとプロセスの時間的前後関係を表すbf-EVALP式はベクトル注釈真理値が(0,0)となる。
【００５８】
これらの実施例で示したようにbf-EVALP方式ではプロセスの開始終了時間のセンシング情報に基づき簡単な整数値ベクトルの加減算と論理的推論によりプロセス順序安全性検証に基づく制御が可能となる。図６は、そのような制御を実現する制御システムの一例を示している。制御システム１０は、プロセスの開始終了を検知するセンサーＡ（前述のセンサーＡ１・Ａ２を含む）と、センサーＡからのセンシング情報に基づき、bf-EVALP式を用いてプロセスの時間的前後関係についての安全性検証を行う演算処理手段Ｂと、演算処理手段Ｂの結果、制御（例えば踏切警報遮断機の開閉、ビール工場におけるビール・水・洗浄液の通水など）を行う制御手段Ｃとからなる。
【００５９】
ちなみにJR西日本では１５００ｍの踏切区間で途中踏切より７００ｍ前方に列車検知器を増設することで事故再発防止としている。鉄道連動により踏切前方７００ｍには２つの列車が同時に進入することはないが、車両故障などによりないとは断言できない。また、このように単純な例ではbf-EVALP方式のような方式を使わなくとも、列車検知カウンターを設置利用するなどの代替方法があると思われるが、鉄道連動と連動する複雑な踏切制御では連動情報をどのように扱うかが問題となるが、通常のEVALPは鉄道連動の安全性検証制御にも有効であることは論文発表している。従ってこのように鉄道連動と連動する複雑な踏切制御の場合にもbf-EVALP制御方式が有効と思われる。実際、２００５年３月下旬に踏切遮断手の人為ミスによって起きた東武鉄道の踏切人身事故などの場合を考えるとbf−EVALP方式による踏切制御を人間のサポートシステムとして利用していれば防げた可能性がある。
【００６０】
その他、化学プラント、原子力発電所など、プロセスの時間的順序関係が致命的な事故を招く可能性がある場所ではこの方式が比類なく有効と考えられる。ネットワークの知的ルーティング制御への応用も考えられる。
【００６１】
この制御方式の適用実施は数多くの場合が考えられるが、制御装置自身が屋外、移動体上など全てが良い環境で利用されるとは考えにくい。そこで、ソフト、ハード両面より実装が容易であることが望ましい。そこで、実装の形態としては次のようなことが考えられる。どれが最良かは場合によって異なる。
１． 電子回路化。
２． PLC(Programmable Logic Controller)上に実装。またはEVALPが実装できる機能をもつPPLC(Programmable Paraconsistent Logic Controller)を開発し、その上に実装。
３． PC上に適当なプログラム言語にて実装。
【産業上の利用可能性】
【００６２】
EVALPは電子回路化、PLC(Programmable Logic Control)への実装が可能であり実時間高速制御にも向いている。従って、PC上のソフトウェアとしてのみならずハードウェアとしてもこの方式は実装可能であり、産業上での応用可能性は高いと考えられる。
【図面の簡単な説明】
【００６３】
【図１】発明のパラコンシステントプロセス処理順序制御方法に用いるベクトル注釈真理値が構成する完備束を模式的に示す図である。
【図２】図２(ａ)〜(ｄ)は、２つのプロセスPri，Prjの時間的前後関係を４つに分類したとき、それぞれを模式的に示す説明図である。
【図３】発明のパラコンシステントプロセス処理順序制御方法を列車の運行に適用した場合の、踏切区間２の模式図である。
【図４】発明によるパラコンシステントプロセス処理順序制御方法をビール工場に適用した場合の、タンク、パイプラインおよびバルブの配置を模式的に示す図である。
【図５】図４のビール工場において、ビール、水および洗浄液を流すプロセスの時間的前後関係を模式的に示す図である。
【図６】発明のパラコンシステントプロセス処理順序制御方法を用いた制御システム１０の概略を示す説明図である。
【符号の説明】
【００６４】
１  踏切警報遮断機
２  踏切区間
１０  制御システム
【図１】
2008146430.tif 000003
【図２】
2008146430.tif 000004
【図３】
2008146430.tif 000005
【図４】
2008146430.tif 000006
【図５】
2008146430.tif 000007
【図６】
2008146430.tif 000008