(57)【要約】本開示は、製造プロセスに従って医薬化合物を製造することに関する。製造プロセスは、プロセスパラメータと、プロセスパラメータをリテラルとして使用する規定とを含む。制御システムが、規定を規定サブセットに分ける区分を決定し、各規定サブセットは、規定で使用されるリテラルに関して、他の規定サブセットから独立している。制御装置は、製造プロセスの簡略化された表現を作成する。これは、対応する規定サブセットからのリテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される。制御装置は、現在のプロセス実行のリテラルの値を、簡略化された表現のリテラルの値と比較することにより、製造プロセスの簡略化された表現に基づいて、製造プロセスの適合性を確認し、比較することで差異が識別された製造プロセスを調整する。制御装置は、差異が識別されなくなるまで、確認及び調整のステップを繰り返す。【選択図】図１０
2022501701.tif 000002
【特許請求の範囲】
【請求項１】
製造プロセスに従って医薬化合物を製造する方法であって、前記製造プロセスが、複数のプロセスパラメータと、前記複数のプロセスパラメータをリテラルとして使用する複数の規定とを含み、
前記規定を複数の規定サブセットに分ける区分を決定することであって、それぞれの前記規定サブセットが、それぞれの前記規定で使用される前記リテラルに関して、他の前記規定サブセットから独立している、前記決定することと、
前記製造プロセスの複数の簡略化された表現を作成することであって、前記複数の簡略化された表現のそれぞれが、前記複数の規定サブセットのうちの対応する１つからの１つ以上の前記リテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される、前記作成することと、
現在のプロセス実行の前記リテラルの値を、前記複数の簡略化された表現のリテラルの値と比較することにより、前記製造プロセスの前記複数の簡略化された表現に基づいて、前記製造プロセスの適合性を確認することと、
前記比較によって差異が識別された前記製造プロセスを調整することと、
前記差異が識別されなくなるまで、確認及び調整のステップを繰り返すことと
を含む、前記方法。
【請求項２】
プロセスを監視する方法であって、前記プロセスが、複数のプロセスパラメータと、前記複数のプロセスパラメータをリテラルとして使用する複数の規定とを含み、
前記規定を複数の規定サブセットに分ける区分を決定することであって、それぞれの前記規定サブセットが、それぞれの前記規定で使用される前記リテラルに関して、他の前記規定サブセットから独立している、前記決定することと、
前記プロセスの複数の簡略化された表現を作成することであって、前記複数の簡略化された表現のそれぞれが、前記複数の規定サブセットのうちの対応する１つからの１つ以上の前記リテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される、前記作成することと、
現在のプロセス実行の前記リテラルの値を、前記複数の簡略化された表現のリテラルの値と比較することにより、前記製造プロセスの前記複数の簡略化された表現に基づいて、前記製造プロセスの適合性を確認することと
を含む、前記方法。
【請求項３】
前記複数の簡略化された表現のそれぞれを作成することは、プレースとトランジションとで構成されるノードを持つ有向グラフを作成することを含む、請求項１または請求項２に記載の方法。
【請求項４】
前記有向グラフがペトリネットである、請求項３に記載の方法。
【請求項５】
前記複数の簡略化された表現を作成することは、前記グラフ内のノードに対応する前記リテラルが、前記複数の規定サブセットの前記対応する１つに含まれていない場合に、そのノードにサイレントというラベルを付けることを含む、請求項３または請求項４に記載の方法。
【請求項６】
前記複数の簡略化された表現を作成することは、サイレントノードを取り去ることによって前記グラフを簡略化することを含む、請求項５に記載の方法。
【請求項７】
前記複数の簡略化された表現を作成することは、前記プロセスが、前記表現の前記状態のうちの１つにあるような状態を含むグラフを作成することを含む、請求項６に記載の方法。
【請求項８】
前記グラフはプライム事象構造であり、前記方法は、他の前記規定サブセットから、前記リテラルに関連付けられたサイレントノードを取り去ることにより、前記プライム事象構造を簡略化することを含む、請求項７に記載の方法。
【請求項９】
前記サイレントノードを取り去ることが、挙動を維持するようにして行われる、請求項８に記載の方法。
【請求項１０】
前記製造プロセスの前記簡略化された表現をクリプキ構造に変換することと、前記クリプキ構造に基づいて適合性を確認することとをさらに含む、先行請求項のいずれか１項に記載の方法。
【請求項１１】
前記クリプキ構造の独立した並行ブランチを線形化することをさらに含む、請求項１０に記載の方法。
【請求項１２】
前記複数の簡略化された表現が、リテラルの値に関連付けられた状態を含み、前記複数の簡略化された表現のそれぞれを確認することは、前記現在のプロセス実行に従って前記状態をトラバースすることと、各状態で、前記現在のプロセス実行の前記リテラルの値を、前記簡略化された表現における前記現在の状態の前記リテラルと比較することとを含む、先行請求項のいずれか１項に記載の方法。
【請求項１３】
前記現在のプロセス実行の前記リテラルの前記値と、前記複数の簡略化された構造のうちの１つの構造の前記リテラルの前記値との差異を検出することによって、不適合を判定すると、前記差異が検出された前記複数の簡略化された構造のうちの前記１つの構造を示すグラフィカルユーザインタフェースを生成することをさらに含む、先行請求項のいずれか１項に記載の方法。
【請求項１４】
前記グラフィカルユーザインタフェースは、前記差異が検出された前記複数の簡略化された構造のうちの前記１つの構造に関連付けられている前記規定サブセットを示す、請求項１３に記載の方法。
【請求項１５】
前記ユーザインタフェースは、前記規定サブセットからの前記１つ以上のリテラルを示す、請求項１４に記載の方法。
【請求項１６】
コンピュータシステムによって実行されると、前記コンピュータシステムに先行請求項のいずれか１項に記載の方法を実行させる、コンピュータソフトウェア。
【請求項１７】
プロセスを監視するためのコンピュータシステムであって、
複数のプロセスパラメータと、前記複数のプロセスパラメータをリテラルとして使用する複数の規定とを格納するためのコンピュータメモリと、
プロセッサであって、
前記規定を複数の規定サブセットに分ける区分を決定することであって、それぞれの前記規定サブセットが、それぞれの前記規定で使用される前記リテラルに関して、他の前記規定サブセットから独立している、前記決定することと、
前記プロセスの複数の簡略化された表現を作成することであって、前記複数の簡略化された表現のそれぞれが、前記複数の規定サブセットのうちの対応する１つからの１つ以上の前記リテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される、前記作成することと、
現在のプロセス実行の前記リテラルの値を、前記複数の簡略化された表現のリテラルの値と比較することにより、前記製造プロセスの前記複数の簡略化された表現に基づいて、前記製造プロセスの適合性を確認することと
を行うように構成されている、前記プロセッサと、
前記適合性の確認の表示をユーザに提供するための出力ポートと
を備える、前記コンピュータシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
関連出願の相互参照
本出願は、２０１８年９月５日出願の豪州仮特許出願第２０１８９０３３０２号に基づいて優先権を主張するものであり、この豪州仮特許出願の内容を全体として参照により本明細書に援用する。
【０００２】
技術分野
本開示は、プロセスを監視することに関し、特に、限定されるわけではないが、製薬プラントの現在の操作を監視することに関する。
【背景技術】
【０００３】
医薬品製造とは、医薬品を工業規模で合成するプロセスのことである。薬剤製造のプロセスは、粉砕、造粒、コーティング、錠剤プレスなどの一連の単位操作に分解することができる。規模に関わらず、薬剤を製造できるようになるまでには、実際の製剤化に多くの作業が必要となる。製剤開発の科学者は、化合物の均一性、安定性、及びその他の多くの要因を評価する。評価段階の後、固体、半固体、即時放出または制御放出、錠剤またはカプセルなどの必要な形態で薬剤を送達するためのソリューションが開発される。固形剤を製造するのに使用される最終配合物を作製するために、幅広い種類の賦形剤が混合され得る。混合され得る材料の範囲（賦形剤、医薬品有効成分）は、条件に合った混合均一性の生成物を実現するために扱われるいくつかの変数を提起する。これらの変数には、粒度分布（材料の凝集体または塊を含む）、粒子形状（球、棒、立方体、平板、及び不定形）、水分（または他の揮発性化合物）の存在、及び粒子表面特性（粗さ、凝集性）が含まれ得る。薬剤製造過程では、薬剤粉末の平均粒径を小さくするために、粉砕が必要になることが多い。これには、均質性と投与量の均一性とを高めること、バイオアベイラビリティを高めること、及び薬剤化合物の溶解性を高めることなど、いくつかの理由がある。造粒は、粉砕の反意語とされている。つまり、これは、小さな粒子が結合して、顆粒と呼ばれる大きな粒子を形成するプロセスである。いくつかの理由で造粒が使用される。造粒は、必要な比率で全ての成分を含有する顆粒を作成することにより、混合物中の成分の「脱混合」を防ぎ、（小粒子は流れにくいので）粉末の流動特性を改善し、錠剤形成のための圧縮特性を改善する。溶解性及びバイオアベイラビリティが低い薬剤の送達を可能にするために、固形製剤経口投薬処理にホットメルトエクストルージョンが利用され得る。ホットメルトエクストルージョンを使用して、高分子担体中に難溶性薬剤を分子分散させ、それによって溶解速度及びバイオアベイラビリティを向上させることができる。このプロセスでは、熱、圧力、及び撹拌を加えて材料を混合し、それをダイから「押し出す」。二軸式高せん断押出機が、材料を混合し、同時に粒子を粉砕する。得られた粒子を混合して、錠剤に圧縮するか、またはカプセルに充填することができる。
【０００４】
これらのことから、医薬品の製造は複雑であり、正しい公称範囲内になければならない多数のパラメータと、所定の公称シーケンスで互いに続く必要があるステップとを含むことが分かる。それに加えて、リーン生産方式及びデジタルマニュファクチャリングへの傾向が見られる。しかし、これらの新しいビジネス組織の方法には、実現するための技術的ソリューションが必要とされる。現在のところ、全てのエンティティによるプロセスが、包括的な規定セットに適合しているということを確実にすることが課題となっている。
【０００５】
そのため、多数の規定の適合性を確認できる技術的なプロセスが求められている。ただし、プロセスの複雑化に伴い、実行する必要のある確認の回数は急速に増加する。例えば、オーストラリアの公正な労働に関する法律には、１，０００を超える条項があり、適合性に関して確認すべき現実的プロセスは、３０〜６０のアクティビティを含む。この結果、２＾６０＊２＾１０００＝２＾１０６０ほどの複雑さが生じる。このような数値は、現在の標準的なコンピュータアーキテクチャでは、適合性のためのプロセスを確認するのに何年もかかるため、実用的ではなく、事実上不可能である。そこで、既存の限られたコンピュータハードウェアで実行できるような、複雑さの問題に対処する、プロセスの適合性確認の方法が必要である。
【０００６】
複雑な製造と他の技術プロセスとに関する別の問題は、プロセスの正しい操作を監視するタスクを課されているユーザが、多くの場合、多数のパラメータ、規定、及び条件に圧倒されてしまうことである。特に、プロセスのある時点でエラーが発生した場合は、一般的には、その最初のエラーの結果として多数のエラーが発生する。その場合、最初のエラーがどこで発生したのか、またはプロセスのどの部分に注意を払う必要があるのかをユーザが認めることは、事実上不可能である。このことは、航空機、宇宙船、または原子力発電所など、大災害を回避するために迅速な意思決定が必要とされる安全関連のプロセスでは特に重要になる可能性がある。
【０００７】
本明細書に含まれている文書、行為、材料、デバイス、物、またはこれらに類するものに関するいかなる議論も、これらの事項のいずれかもしくは全てが先行技術基盤の一部を形成していること、またはこれらが、本願の各請求項の優先日前に存在していたとして、本開示に関連する分野で周知の一般知識であったことを認めるものとはみなされない。
【０００８】
本明細書を通じて、単語「ｃｏｍｐｒｉｓｅ（含む）」、または「ｃｏｍｐｒｉｓｅｓ（含む）」もしくは「ｃｏｍｐｒｉｓｉｎｇ（含む）」などの変形は、既定された要素、完全体またはステップ、または要素群、完全体またはステップ群を包含するが、いかなる他の要素、完全体またはステップ、または要素群、完全体群またはステップ群をも排除することを意味するものではないことが理解されよう。
【発明の概要】
【０００９】
製造プロセスに従って医薬化合物を製造するための方法が提供される。この製造プロセスは、複数のプロセスパラメータと、複数のプロセスパラメータをリテラルとして使用する複数の規定とを含む。本方法は、
規定を複数の規定サブセットに分ける区分を決定することであって、それぞれの規定サブセットが、それぞれの規定で使用されるリテラルに関して、他の規定サブセットから独立している、決定することと、
製造プロセスの複数の簡略化された表現を作成することであって、複数の簡略化された表現のそれぞれが、複数の規定サブセットのうちの対応する１つからの１つ以上のリテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される、作成することと、
現在のプロセス実行のリテラルの値を、複数の簡略化された表現のリテラルの値と比較することにより、製造プロセスの複数の簡略化された表現に基づいて、製造プロセスの適合性を確認することと、
比較によって差異が識別された製造プロセスを調整することと、
差異が識別されなくなるまで、確認及び調整のステップを繰り返すことと、を含む。
【００１０】
プロセスは、複数のプロセスパラメータと、複数のプロセスパラメータをリテラルとして使用する複数の規定とを含み得る。本方法は、
規定を複数の規定サブセットに分ける区分を決定することであって、それぞれの規定サブセットが、それぞれの規定で使用されるリテラルに関して、他の規定サブセットから独立している、決定することと、
プロセスの複数の簡略化された表現を作成することであって、複数の簡略化された表現のそれぞれが、複数の規定サブセットのうちの対応する１つからの１つ以上のリテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される、作成することと、
現在のプロセス実行のリテラルの値を、複数の簡略化された表現のリテラルの値と比較することにより、製造プロセスの複数の簡略化された表現に基づいて、製造プロセスの適合性を確認することとを含み得る。
【００１１】
複数の簡略化された表現のそれぞれを作成することは、プレースとトランジションとで構成されるノードを持つ有向グラフを作成することを含んでもよい。有向グラフはペトリネットであってもよい。
【００１２】
複数の簡略化された表現を作成することは、グラフ内のノードに対応するリテラルが、複数の規定サブセットの対応する１つに含まれていない場合に、そのノードにサイレントというラベルを付けることを含んでもよい。複数の簡略化された表現を作成することは、サイレントノードを取り去ることによってグラフを簡略化することを含んでもよい。複数の簡略化された表現を作成することは、プロセスが、表現の状態のうちの１つにあるような状態を含むグラフを作成することを含んでもよい。グラフはプライム事象構造であり、本方法は、他の規定サブセットから、リテラルに関連付けられたサイレントノードを取り去ることにより、プライム事象構造を簡略化することを含み得る。サイレントノードを取り去ることは、挙動を維持するようにして行われてもよい。
【００１３】
本方法は、製造プロセスの簡略化された表現をクリプキ構造に変換することと、クリプキ構造に基づいて適合性を確認することとをさらに含み得る。本方法は、クリプキ構造の独立した並行ブランチを線形化することをさらに含み得る。
【００１４】
複数の簡略化された表現が、リテラルの値に関連付けられた状態を含んでもよく、複数の簡略化された表現のそれぞれを確認することは、現在のプロセス実行に従って状態をトラバースすることと、各状態で、現在のプロセス実行のリテラルの値を、簡略化された表現における現在の状態のリテラルと比較することとを含んでもよい。
【００１５】
本方法は、現在のプロセス実行のリテラルの値と、複数の簡略化された構造のうちの１つの構造のリテラルの値との差異を検出することによって、不適合を判定すると、差異が検出された複数の簡略化された構造のうちの１つの構造を示すグラフィカルユーザインタフェースを生成することをさらに含み得る。グラフィカルユーザインタフェースは、差異が検出された複数の簡略化された構造のうちの１つの構造に関連付けられている規定サブセットを示してもよい。ユーザインタフェースは、規定サブセットからの１つ以上のリテラルを示してもよい。
【００１６】
コンピュータシステムによって実行されると、コンピュータシステムに上記の方法を実行させるコンピュータソフトウェア。
【００１７】
プロセスを監視するためのコンピュータシステムであって、
複数のプロセスパラメータと、複数のプロセスパラメータをリテラルとして使用する複数の規定とを格納するためのコンピュータメモリと、
プロセッサであって、
規定を複数の規定サブセットに分ける区分を決定することであって、それぞれの規定サブセットが、それぞれの規定で使用されるリテラルに関して、他の規定サブセットから独立している、決定することと、
プロセスの複数の簡略化された表現を作成することであって、複数の簡略化された表現のそれぞれが、複数の規定サブセットのうちの対応する１つからの１つ以上のリテラルを含み、他の規定サブセットによって使用されるリテラルを取り除くことによって作成される、作成することと、
現在のプロセス実行のリテラルの値を、複数の簡略化された表現のリテラルの値と比較することにより、製造プロセスの複数の簡略化された表現に基づいて、製造プロセスの適合性を確認することとを行うように構成されている、プロセッサと、
適合性の確認の表示をユーザに提供するための出力ポートとを備える、コンピュータシステム。
【００１８】
方法、コンピュータ可読媒体、またはコンピュータシステムの任意の態様について記載される任意選択の特徴は、適切な場合には、ここに記載された他の態様にも同様に適用される。
【００１９】
次に、以下の図面を参照して実施例を説明する。
【図面の簡単な説明】
【００２０】
【図１】製造プロセスを監視するための方法を説明する。
【図２】ビジネスプロセスモデリング表記法（ＢＰＭＮ）の形式のプロセスの実施例を説明する。「ビジネス」プロセスという名前に関わらず、ＢＰＭＮは、航空機などの機械の製造または制御など、技術的プロセスの表現にも同様に使用できることに留意されたい。
【図３】図２のＢＰＭＮモデルからペトリネットへのその結果生じた変換の結果を説明する。
【図４】図３のペトリネットにＲ１を適用した結果の規定固有のペトリネットを示す。
【図５ａ】プライム事象構造（ＰＥＳ）の実施例を示す。
【図５ｂ】縮小を伴わないＰＥＳプレフィックス展開を示す。
【図６】ａ及びｂは、Ｒ１に固有のＰＥＳプレフィックス展開を説明する。
【図７】図６ｂの規定固有のペトリネットから作成された検証可能なモデルを説明する。
【図８】元のクリプキ構造を示す。
【図９】同じ規定に基づく線形化されたクリプキ構造と図８のクリプキ構造とを示す。
【図１０】プロセスを監視するためのコンピュータシステムを説明する。
【図１１】図１の方法のコンピュータによる実施のデータフロー表現を説明する。
【発明を実施するための形態】
【００２１】
以下の開示は、上記の複雑さの問題に対処する、プロセスの現在の操作を実行しまたは監視するための方法及びシステムに関する。本明細書に開示される方法を使用すると、それ以外の場合は既存のコンピュータシステムには複雑すぎるであろうプロセスを監視することができる。一実施例では、本開示は、さらなるプロセスステップ及びさらなるパラメータに加えて、上記のパラメータ及びシーケンスを有する医薬品製造プロセスに適用される。これらの実施例では、「公称操作」という用語は、医薬品製造プロセスに規定されているプロセス変数／パラメータ及びステップのシーケンスを指す。また一方、本開示は、コンピュータシステムまたは他のプロセスの侵入検知などの他の領域にも同様に適用可能である。
【００２２】
より具体的には、本開示は、技術的プロセス（例えば、製造、化学、サーバ）が、規定セットに適合しているかどうかを確認することに関する。規定には、温度の閾値（例えば、３６．０＜Ｔ＜３７．０）またはその他のプロセスパラメータ、及びシーケンス（例えば、粉砕の後に造粒）が含まれ得る。以下の開示は、厳密な数学的定式化を提供するが、実際にこの定式化に従うことの意味合いは、既存のハードウェアを使用して、複雑なプロセスの適合性確認を最終的に可能にする、大幅な複雑さの減少であることに留意されたい。この意味で、本開示は、ビジネスプロセスに適用可能であり得るが、本開示の真価及び実質は、処理時間の短縮及び必要なコンピュータメモリの量の削減という技術的な効果及び貢献に向けられている。
【００２３】
図１は、製造プロセスを監視するための方法１００を説明する。製造プロセスは、複数のプロセスパラメータと、複数のプロセスパラメータをリテラルとして使用する複数の規定とを含む。例えば、温度はプロセスパラメータであり、閾値を適用することでブールリテラルとして表現することができるので、（温度の）リテラルＴは、温度が必要な範囲内にあれば、「１」または真となり、温度がその範囲外であれば、「０」または偽となる。その場合、この規定は単純にＴ＝１となる。また一方、温度が、規定Ｔ  ＡＮＤ  ＮＯＴ  Ｃ＝１に通じる範囲内にある場合は、クーラントの流れを止めなければならない場合もある。以上のように、ただ２つのみのリテラルに対し、すでに４つの異なる組み合わせが存在している。この組み合わせは、リテラルの数に伴って指数関数的に増加する。したがって、プロセス全体に２０個のパラメータがある場合、組み合わせ可能な組み合わせは１００万通り以上になる。
【００２４】
この指数関数的な増大に対処するために、方法１００は、規定を複数の規定サブセットに分ける区分を決定する（１０１）ステップを含む。各規定サブセットは、それぞれの規定で使用されるリテラルに関して、他の規定サブセットから独立している。換言すれば、各区分には、相互に（潜在的に推移的である）依存関係を持つ規定サブセットが含まれている。異なる区分内の規定は、それらが、互いに素なリテラルセットを持つという意味で、互いに独立している。例えば、次の規定を検討してみる。
・Ｒ１：Ｌ１→Ｌ２
・Ｒ２：Ｌ１→Ｌ３
・Ｒ３：Ｌ４→Ｌ５
・Ｒ４：Ｌ５→Ｌ６，Ｌ７
【数１】
2022501701.tif 000003
【００２５】
この規定セットから、次の区分、すなわち、｛Ｒ１，Ｒ２｝、｛Ｒ３，Ｒ４，Ｒ５｝及び｛Ｒ６｝が得られる。全ての規定に共通のリテラルには例外がある可能性があるため、それらのリテラルを全ての区分に複製しなければ、区分化は不可能であることに留意されたい。
【００２６】
一実施例では、区分を見つけることは、各ノードがリテラルを表し、２つの接続されたリテラルが同じ規定内にある場合にエッジが作成されるグラフを作ることを含む。その場合、Ｂｒｏｎ及びＫｅｒｂｏｓｃｈなどのクリーク抽出アルゴリズムをグラフに適用してクリークを見つけ、その結果、それが区分を形成することができる（Ｃｏｅｎ  Ｂｒｏｎ及びＪｏｅｐ  Ｋｅｒｂｏｓｃｈ（１９７３）：Ａｌｇｏｒｉｔｈｍ  ４５７：Ｆｉｎｄｉｎｇ  Ａｌｌ  Ｃｌｉｑｕｅｓ  ｏｆ  ａｎ  Ｕｎｄｉｒｅｃｔｅｄ  Ｇｒａｐｈ．Ｃｏｍｍｕｎｉｃａｔｉｏｎｓ  ｏｆ  ｔｈｅ  ＡＣＭ  Ｖｏｌ．１６，Ｉｓｓｕｅ  ９．ＡＣＭ  Ｐｒｅｓｓ：Ｎｅｗ  Ｙｏｒｋ，ＵＳＡを参照）。
【００２７】
規定セットを区分化した後、方法１００の次のステップは、規定サブセットごとにプロセスの複数の簡略化された表現を作成する（１０２）ことである。複数の簡略化された表現のそれぞれは、複数の規定サブセットのうちの対応する１つのサブセットからの１つ以上のリテラルを含むが、他のサブセットで使用されるリテラルは、以下に説明するように取り除かれる。一実施例では、この簡略化された表現は、ペトリネット、プライム事象構造、及びクリプキ構造を含む。
【００２８】
図２は、後で適合性の規定において使用されるリテラルで注釈が付けられたビジネスプロセスモデリング表記法（ＢＰＭＮ）の形式のプロセスの実施例を説明する。ＢＰＭＮは、ビジネスプロセスモデルにおいてビジネスプロセスを指定するためのグラフ表示である。ＢＰＭＮ仕様の詳細については、ｈｔｔｐ：／／ｗｗｗ．ｂｐｍｎ．ｏｒｇ／で確認できる。ＢＰＭＮは、一般に、企業の内部業務手続きをグラフィカルな表記法で理解する能力を企業に提供することを目的としているが、ここでは、計算効率の良い方法で所望の結果を達成するために、グラフベースコンピュータプロセスに対する先行データ構造として使用される。ただし、他の開始点を同様に選択してもよい。
【００２９】
技術的プロセスは、様々な表記法を使用してモデル化することができる。多くの場合、これらの表記法では、形式的検証が適用され得る前に、さらに形式化する必要がある。例えば、ＢＰＭＮは、技術的プロセスをモデル化するのに使用される。しかし、ＢＰＭＮモデルは、形式的検証を可能にするために形式化を用いている。
【００３０】
ペトリネット（ＰＮ）は、技術的プロセスを形式化するために使用されるモデリング言語である。ペトリネット、すなわちプレース／トランジションネットは、分散システムを記述するための数学モデルである。ペトリネットは、プレースとトランジションとで構成されるノードを持つ有向バイグラフである。ペトリネット内のトランジションは事象を表し、プレースは条件を表す。アークは、プレースとトランジションとのペアの間に有向エッジを形成する。プレースは、トークンを含むことがある。トークンをプレース上に分配することをマーキングという。全ての入力プレースが少なくとも１つのトークンを持つ場合に、トランジションが有効になり、「発火」することができる。トランジションが発火すると、各入力プレースから１つのトークンが取り去られ、各出力プレースに１つのトークンが配置される。
【００３１】
ＢＰＭＮプロセスモデルから対応するペトリネットへの変換では、並列ゲートウェイと排他的ブランチとによって定義される挙動を実現するために、ラベル無しトランジション（サイレントトランジションまたはτトランジションと呼ばれる）の概念を使用する。これらのラベル無しトランジションは、後で説明するように、事象構造の構築中に取り除かれる。
【００３２】
図３は、図２のＢＰＭＮモデルからペトリネットへのその結果生じた変換の結果を説明する。
【００３３】
規定固有のペトリネット
この実施例では、簡単にするために、規定Ｒ１：Ｌ１→Ｌ２（規定Ｒ１）のみを考慮している。規定Ｒ１を削減する場合、Ｌ１またはＬ２を含まない全てのトランジション（すなわち、他のサブセットのリテラル）は、ペトリネットにおいてサイレントにされる（すなわち、取り除かれる）。足踏同値を維持するために、リテラルの変更を全く含まないアクティビティがモデルに含まれているが、後でクリプキ構造に変換する際には（詳細に後述するように）異なった処理を受ける。
【００３４】
図４は、図３のペトリネットにＲ１を適用した結果の規定固有のペトリネットを示す。τでラベル付けされたトランジションはサイレントであり、一方、
【数２】
2022501701.tif 000004
でラベル付けされたトランジションは足踏同値を維持するために使用される（したがって、サイレントにすることはできない）。例えば、トランジションｔ６は、調査対象の式の一部ではない（すなわち、他のサブセットのリテラルのみである）ために、関連するリテラルを持たない。しかし、ｔ６は（足踏同値のために）非表示にすることはできないが、そのリテラルはクリプキでは無視されることになり、それゆえに
【数３】
2022501701.tif 000005
というラベルが付けられている。それによって、プロセスの挙動が確実に保持される。
【００３５】
プライム事象構造及びＰＥＳプレフィックス展開
分岐プロセスは、元のネットの全ての半順序実行を単一のツリーのような構造で明示的に表現する、ペトリネットの代替クラスである。ネットの実行とは、そのネットの１回の実行で発生する可能性のある半順序の事象のセットである。分岐プロセスは、発生する事象のペア間の挙動関係のセットを含む。分岐プロセスから生じる挙動関係は、プライム事象構造（ＰＥＳ）を生成する。ＰＥＳの詳細は、参照により本明細書に組み込まれる、Ｐｒｏｃｅｅｄｉｎｇ  Ｌｉｎｅａｒ  Ｔｉｍｅ，Ｂｒａｎｃｈｉｎｇ  Ｔｉｍｅ  ａｎｄ  Ｐａｒｔｉａｌ  Ｏｒｄｅｒ  ｉｎ  Ｌｏｇｉｃｓ  ａｎｄ  Ｍｏｄｅｌｓ  ｆｏｒ  Ｃｏｎｃｕｒｒｅｎｃｙ，Ｓｃｈｏｏｌ／Ｗｏｒｋｓｈｏｐ．Ｓｐｒｉｎｇｅｒ，１９８９にあるＧｌｙｎｎ  Ｗｉｎｓｋｅｌ，Ａｎ  ｉｎｔｒｏｄｕｃｔｉｏｎ  ｔｏ  ｅｖｅｎｔ  ｓｔｒｕｃｔｕｒｅｓ．に見つけられる。具体的には、事象構造は計算プロセスのモデルである。これらは、事象が他の事象にどのように因果的に依存しているかを表現する事象発生のセットとしてプロセスを表す。
【００３６】
ＰＥＳは事象のグラフであり、各事象ｅはビジネスプロセスにおけるタスクまたはアクティビティの発生を表す。そのため、同じアクティビティの複数の発生が、異なる事象によって表される。事象は、以下のバイナリ動作関係を有し得る。
１．因果関係（
【数４】
2022501701.tif 000006
）は、事象
【数５】
2022501701.tif 000007
が
【数６】
2022501701.tif 000008
の必要条件であることを示す、
２．競合（
【数７】
2022501701.tif 000009
）は、
【数８】
2022501701.tif 000010
と
【数９】
2022501701.tif 000011
とが同じ実行で発生できないことを意味する、
３．同時並行性（
【数１０】
2022501701.tif 000012
）は、
【数１１】
2022501701.tif 000013
と
【数１２】
2022501701.tif 000014
との間に順序を確立できないことを示す。
【００３７】
分岐プロセスのトランジションは、ＰＥＳの事象に対応する。サイレント（またはτ）事象は、挙動を維持するようにして取り去ることができる。この方法では、事象構造内の全てのシンク事象が可視事象である場合に保持される。ループを持つペトリネットの分岐プロセスは、潜在的に無限である。ただし、安全なネットの場合は、分岐プロセスのプレフィックスが元のネットの挙動を完全に記号化する。このようなプレフィックスは、ネットの完全なプレフィックス展開と呼ばれている。ＢＰＭＮプロセスモデルによって指定された挙動を表すために、本明細書に開示された方法は、対応するペトリネットの完全なプレフィックス展開から導出されたＰＥＳを使用することができ、これはモデルのＰＥＳプレフィックス展開と呼ばれる。
【００３８】
ＰＥＳプレフィックス展開では、２つの事象が同じ「未来」を（例えば、ｔ２：Ｂとｔ３：Ｃとのように）共有している場合、プロセスの挙動を記述するために１つの「未来」のみが使用される。したがって、１つの事象をカットオフ事象と呼ぶ。カットオフ事象後の残りの事象はＰＥＳから取り去ることができ、カットオフ事象はその対応する事象を参照する。図５ａはＰＥＳの実施例を示し、図５ｂはＰＥＳプレフィックス展開を示す。因果関係は実線の矢印で示され、競合関係は点線で示される。この実施例では、ｔ３：Ｃはカットオフ事象であり、ｔ２：Ｂは対応する事象である。カットオフ事象及び対応する事象はまとめてｃｃペアと呼ばれ、これは破線の矢印５０１で示されている。言い換えれば、全面的な分岐プロセス／ツリーの展開は、知られた状態に遭遇するとすぐに停止され、重複する後続の事象を必要とせずに、カットオフ及び対応する事象が、カットオフ事象の「未来」を表すように作成される。これにより、構造の複雑さ（ノード及びエッジの数）が軽減されるので、この方法のパフォーマンスが大幅に向上することになる。
【００３９】
ＰＥＳプレフィックス展開の計算は、本方法が、ｃｃペア（ｔ２：Ｂ及びｔ３：Ｃ）を追跡し、そのような事象が、カットオフまたは対応する事象のいずれかである場合には、サイレント事象を抽象化しないことを除いては、通常のＰＥＳの計算と同じであると見ることができる。
【００４０】
図４のペトリネットのＰＥＳプレフィックス展開を生成する際に、τトランジションは、カットオフまたは対応する事象を表していない限り、取り除いてもよい。図６ａは、直接プレフィックス展開を示す。ただし、ｔ３：Ｃを置き換えるτトランジションは、カットオフ事象であるために、取り去ることはできない。その結果、ＰＥＳプレフィックス展開は、相互に排他的であるがリテラルを表していない２つのサイレント事象（τ及び
【数１３】
2022501701.tif 000015
）を示している。したがって、図６ｂに示すように、それらを単一の
【数１４】
2022501701.tif 000016
事象に置き換えて、足踏同値を維持することができる。アプリケーションと足踏同値が重要であるかどうかとに応じて、図５ｂ及び図６ｂのいずれかの表現を、方法１００のステップ１０２で作成されるプロセスの簡略化された表現として使用してもよい。ここで、図５ｂ及び図６ｂの複数の簡略化された表現のそれぞれが、対応する規定サブセットからのリテラルを含むことに留意されたい。したがって、それらの表現が複数存在し、規定サブセットごとに１つの表現を持つ。
【００４１】
クリプキ構造への変換
図１の方法１００の次のステップは、製造プロセスの複数の簡略化された表現に基づいて、プロセスの適合性を確認する（１０３）ことである。各状態でのプロセスモデルの適合性（すなわち、プロセスモデルが規定に適合していない状態が存在しないこと）を確認するために、モデルの可能な状態とそれらの状態間のトランジションとがモデルに取り込まれる。
【００４２】
一般的には、適合性確認１０３は、Ｓ×Ｓのサブセットとして定義されたトランジション関係を伴う（ラベル付けされた）トランジションシステムに基づいてもよく、これは、原子命題のセットと、その上、状態のラベル付け関数（Ｌ）とを含むようにさらに拡張されてもよい。このアプローチでは、アクションラベルを抽象化して得られる２項関係を状態グラフと呼ぶことがある。
【００４３】
より具体的には、その状態に対するラベル付け関数を有し、モデル検査のためのシステムモデルとして使用できる状態ベースのラベル付きトランジションシステムでもあるクリプキ構造を使用することができる。ＡＰを原子命題のセット、すなわち変数、定数、及び述語記号に対するブール式とする。クリプキ構造は、ＡＰ上で、
・有限の状態セットＳ、
・初期状態のセットＩ⊆Ｓ、
・Ｒが左全域的であるようなトランジション関係Ｒ⊆Ｓ×Ｓ、すなわち、（ｓ，ｓ′）∈Ｒであるような∀ｓ∈Ｓ∃ｓ′∈Ｓ、
・ラベル付け（または解釈）関数Ｌ：Ｓ→２ＡＰ、で構成される４タプルＭ＝（Ｓ，Ｉ，Ｒ，Ｌ）として定義され得る。
【００４４】
Ｒは左全域的であるため、クリプキ構造を通る無限のパスを構築することが常に可能である。デッドロック状態は、それ自体に戻る単一の発信エッジによってモデル化され得る。ラベル付け関数Ｌは、各状態ｓ∈Ｓに対して、ｓで有効な全ての原子命題のセットＬ（ｓ）を定義する。
【００４５】
構造Ｍのパスは、各ｉ＞０に対してＲ（ｓｉ，ｓｉ＋１）が保持されるような状態のシーケンスρ＝ｓ１，ｓ２，ｓ３，・・・である。パスρ上の単語は、アルファベット２ＡＰ上のω単語である原子命題ｗ＝Ｌ（ｓ１），Ｌ（ｓ２），Ｌ（ｓ３），・・・のセットのシーケンスである。
【００４６】
この定義では、クリプキ構造（例えば、１つの初期状態ｉ∈Ｉしか持たない）は、シングルトン入力アルファベットを備えたムーアマシンで識別でき、出力関数はそのラベル付け関数である。
【００４７】
図６ｂの縮小されたＰＥＳプレフィックス展開は、クリプキ構造に変換され得る。クリプキ構造の全ての状態は、原子命題（ＡＰ）のセットを表す。各ＡＰは、その状態で有効になっている（すなわち、発火／実行することができる）トランジションのリテラルを表す。図７は、図６ｂの縮小されたＰＥＳプレフィックス展開から生成されたクリプキを示す。
【００４８】
独立した並行ブランチの線形化
図３に示すペトリネットについて検討してみる。２つの規定Ｒ１：Ｌ１→Ｌ２及びＲ２：Ｌ１→Ｌ３がある場合、縮小モデルでは両方の並行ブランチが必要であるが、ブランチには相互の依存関係がない。提示した方法を使用して、Ｒ１及びＲ２に基づいて得られたクリプキ構造を、図８にグラフを使って示す。
【００４９】
そのように、各インターリーブは同じ結果をもたらすので、適合性の解析中にインターリーブの計算を行う必要はない。したがって、独立した並行ブランチを線形化し得る追加の縮小ステップが提案されている。その結果として、１つのインターリーブのみが作成され、それが規定に対する適合性を評価するために用いられる。結果として生じる線形化されたクリプキ構造を図９に示す。
【００５０】
結果的に、製造プロセスの複数の簡略化された表現に基づいて、製造プロセスの適合性を確認する（１０３）ことにより、製造プロセスを規定と照らし合わせることができる。このことは、現在のプロセス実行のリテラルの値（例えば、現在の温度）を、複数の簡略化された表現（すなわち、クリプキ構造、他の状態モデルまたは状態グラフ）のリテラルの値と比較することによって実行される。このようにして、プロセスのリテラルが確認されて、それらがクリプキ構造における有効なトランジションを表していることを保証する。これは、全ての規定サブセットに対して並行して実行することができる。
【００５１】
例えば、図９に示す簡略化された表現では、プロセスの開始時に、第１のノード９０１はＬ１とラベル付けされ、それによって、第１のリテラルが（温度が公称範囲内にあるなど）真の場合に、プロセスが適合していることを意味する。残りのリテラルはこの段階では無関係であり、同じことが第２の状態９０２にも当てはまる。ただし、第３の状態９０３では、リテラルＬ１及びＬ２の両方が真でなければならず、第４の状態９０４では、４つのリテラルＬ１、Ｌ２、Ｌ３全てが真でなければならず、そうでなければプロセスは適合していないことになる。第５の状態９０５への遷移時に、第１のリテラルＬ１は偽に切り替えなければならず、残りの２つのリテラルＬ２及びＬ３は真のままでなければならない。
【００５２】
これは、規定ごとの簡略化が法外なものになることなく、可能な組み合わせの総数にもかかわらず、ノード数の少ないモデルで同時に操作しながら、プロセスを確認する方法を示している。
【００５３】
クリプキ構造のリテラル値とプロセスパラメータ値との間に差異があれば、製造プロセスを調整することができる。これには、プロセスパラメータを直接制御するために、またはプロセスに入る材料の量を調整するために、バルブ、ヒータまたはクーラなどのアクチュエータを制御することが含まれ得る。次に、ステップ１０３の適合性確認及び調整は、差異が識別されなくなるまで、すなわち、プロセスが適合するまで繰り返され得る。ステップ１０３は、逸脱または不適合が早期に検出されて、タイムリーな介入を提供することを確実にするために、プロセスの操作全体を通して調整せずに繰り返されてもよい。
【００５４】
要約すると、プロセスが、ＢＰＭＮまたはペトリネットなどのプロセスモデルによって表される。これらのモデルは、例えば、それらが並列実行を効率的に表すため、通常は状態ベースではない。プロセスモデルは、独立した規定サブセットごとに複製され、各複製は、どのリテラルがその対応する規定内にあるかと、適切な場合はＰＥＳプレフィックス展開とに基づいて簡略化される。簡略化された表現は、現在は状態ベースの表現であるプライム事象構造の形式であってもよい。最後に、結果として生じる表現は、各状態にあるリテラルの効率的な確認を可能にするクリプキ構造に変換される。これに関連して、簡略化された表現は、ＢＰＭＮなどのプロセスモデル表現の元の形式には変換されないことに注意が必要である。ただし、簡略化されたクリプキ構造は、プロセスのこのコピーを簡略化するために使用された規定セットに照らして製造プロセスを表すので、製造プロセスの簡略化された表現と呼ばれる。
【００５５】
図１０は、プロセスを監視するためのコンピュータシステム１０００を説明する。コンピュータシステム１０００は、プログラムメモリ１００４、データメモリ１００６、通信ポート１００８、及びユーザポート１０１０に接続されたプロセッサ１００２を備える。プログラムメモリ１００４は、ハードドライブ、ソリッドステートディスクまたはＣＤ−ＲＯＭなどの非一時的コンピュータ可読媒体である。ソフトウェア、すなわち、プログラムメモリ１００４に格納された実行可能プログラムにより、プロセッサ１００２は、図１の方法を実行する、すなわち、プロセッサ１００２は、規定サブセットに分ける区分を決定し、サブセットごとにプロセスの簡略化された表現を作成し、そのサブセット内のリテラルに基づいて適合性を確認する。用語「区分の決定」または「表現の作成」は、区分または表現を示すパラメータ値を計算することを指す。このことは関連した用語にも当てはまる。表現及び／または区分は、テキストファイル、リレーショナルデータベースとして格納され得、または好ましくはより効率的な操作のために、グラフベースのデータベースに格納され得る。
【００５６】
次に、プロセッサ１００２は、ＲＡＭまたはプロセッサレジスタなどのデータストア１００６に表現を格納することができる。プロセッサ１００２は、データメモリ１００６から、さらには通信ポート１００８及びユーザポート１０１０から、現在のプロセスパラメータ（すなわち、リテラル値）などのデータを受信し得る。ユーザポート１０１０は、プロセスの現在の操作の視覚的表現をユーザに示すディスプレイに接続されている。
【００５７】
一実施例では、ユーザポート１０１０は、テキストメッセージ、ウェブサイト（ウェブアクセス可能なＨＴＭＬを書いたもの）の形式で、またはコンピュータディスプレイ上に、適合性の確認の表示をユーザに提供する出力ポートとして機能してもよい。ユーザポート１０１０はまた、ブザーまたは警報灯などの警報機構に接続されて、時間／安全性が重要なプロセスの規制に従っていないことを表示してもよい。また、規定の区分のそれぞれには、その区分の高レベルの機能を表すラベルが設けられてもよい。このようにして、ユーザへの表示には、不適合の原因となったリテラルの潜在的に長いリストの代わりに、高レベルのラベルを含めることができる。
【００５８】
一実施例では、プロセッサ１００２は、ＩＥＥＥ８０２．１１に従ってＷｉ−Ｆｉネットワークを使用するなどによって、通信ポート１００８を介してセンサから現在のプロセスパラメータを受信する。Ｗｉ−Ｆｉネットワークは、ルータなどの専用の管理インフラストラクチャが不要な分散型アドホックネットワーク、またはネットワークを管理するルータまたはアクセスポイントを備えた集中型ネットワークの場合がある。センサは、衛星通信と独立した電源とを介して接続されたリモートセンサであってもよい。
【００５９】
一実施例では、プロセッサ１００２は、現在のプロセスパラメータをリアルタイムで受信して処理する。このことは、プロセッサ１００２は、現在のプロセスデータがセンサから受信されるたびにプロセスの適合性を確認し、センサが次のセンサデータ更新を送信する前に、この計算を完了することを意味している。
【００６０】
通信ポート１００８及びユーザポート１０１０は、別個のエンティティとして示しているが、ネットワーク接続、メモリインタフェース、プロセッサ１００２のチップパッケージのピン、またはＩＰソケットもしくはプログラムメモリ１００４に格納され、プロセッサ１００２によって実行される機能のパラメータなどの論理ポートなど、データを受信するために任意の種類のデータポートが使用されてもよいことが理解されよう。これらのパラメータは、データメモリ１００６に格納されていてもよく、ソースコード中では、値または参照によって、すなわち、ポインタとして扱われてもよい。
【００６１】
プロセッサ１００２は、キャッシュもしくはＲＡＭなどの揮発性メモリ、または光ディスクドライブ、ハードディスクドライブ、ストレージサーバ、もしくはクラウドストレージなどの不揮発性メモリのメモリアクセスを含む、これら全てのインタフェースを介してデータを受信し得る。コンピュータシステム１０００は、動的な数の仮想マシンをホストする相互接続されたサーバの管理されたグループなど、クラウドコンピューティング環境内でさらに実装されてもよい。
【００６２】
任意の受信ステップに先立って、プロセッサ１００２が、後で受信されるデータを決定し、または計算することができることを理解されたい。例えば、プロセッサ１００２は、現在のプロセスパラメータを決定し、それをＲＡＭまたはプロセッサレジスタなどのデータメモリ１００６に格納する。次に、プロセッサ１００２は、メモリアドレスと共に読み出し信号を提供するなどして、データメモリ１００６にデータを要求する。データメモリ１００６は、物理ビットライン上の電圧信号としてデータを提供し、プロセッサ１００２は、メモリインタフェースを介してパラメータ値を受信する。
【００６３】
本開示全体を通して、特に断りのない限り、ノード、エッジ、グラフ、解、変数、モデル、及びこれらに類するものは、データメモリ１００６に物理的に格納されているか、またはプロセッサ１００２によって処理されるデータ構造を指すことを理解されたい。さらに、簡潔さのために、「期間」または「適合性」などの特定の変数名を参照する場合、これは、コンピュータシステム１０００内の物理データとして格納されている変数の値を参照するものと理解されるべきである。
【００６４】
さらに、図１は、ソフトウェアプログラムの青写真として理解されるべきであり、図１の各ステップが、Ｃ＋＋またはＪａｖａ（登録商標）などのプログラミング言語の関数によって表されるように、段階的に実施されてもよい。その後、結果として生じるソースコードがコンパイルされ、コンピュータ実行可能命令としてプログラムメモリ１００４に格納される。
【００６５】
さらなる例では、プロセッサ１００２は、本明細書で説明されたペトリネットまたはＢＰＭＮの視覚的表現など、プロセスモデルの視覚的表現を生成してもよい。さらに、プロセッサ１００２は、プロセスが現在適合していることを示すグラフィカルユーザインタフェースを生成してもよい。プロセッサ１００２は、プロセスが適合していない（すなわち、簡略化された表現のリテラルが現在のプロセスパラメータと一致しない）ことを判定すると、不適合を表示するようにグラフィカルユーザインタフェースを変更する。
【００６６】
例えば、プロセッサ１００２は、不適合が発生したプロセスの簡略化された表現の視覚的表現を生成してもよい。ユーザにとっては、これにより規定セットが大幅に絞り込まれ、ユーザによる迅速な介入が可能になる。これは、技術的に複雑なシステムを制御するためのユーザインタフェースにおいて特に有利である。例えば、現代の航空機のパイロットは、常に多数の異なるパラメータを監視する必要がある。不適合が発生した場合、相互に関連のある技術システムに起因して、多数のエラーメッセージが表示され得る。これは、パイロットの認知能力をすぐに超える可能性がある。しかしながら、提案したシステムでは、独立した規定セットは分離されているので、多くの場合、それらのセットのうちの１つだけが影響を受け得ることを意味している。結果として、何百ものエラーメッセージを表示する代わりに、機内システムは、例えば左エンジンなど、不適合である概略の領域をパイロットに示すように、不適合が発生した独立した規定セットの記述子のみを表示してもよい。
【００６７】
図１１は、データフロー表現１１００における図１の方法１００を説明する。この意味で、図１１は、図１１の各破線のボックスがデータオブジェクトを示し、図１の方法ステップが次のデータオブジェクトを作成する矢印（左から右へ）を示すようなオブジェクト指向の方法で実装することができる。また、データオブジェクトは、モジュールまたはクラウドコンピューティングプラットフォーム上の仮想マシンなどの別個のコンピュータインスタンスとして記述されてもよい。入力データオブジェクト１１０１は、ＢＰＭＮ表記のモデルなどのプロセスモデル１１０２を備える。プロセッサ１１０２は、複数のリテラル１１０３を自動的に抽出してもよく、またはリテラルは、プロセスモデルと共に提供されてもよい。プロセスモデルは、データファイルとして提供されてもよく、ユーザが入力してもよい。
【００６８】
次に、プロセッサ１００２は、規定セット１１０５を保持するグローバル規定データオブジェクト１１０４を作成する。この意味でのグローバルとは、規定がプロセス全体にわたって適用可能であるか、またはプロセス全体にわたる範囲を有することを意味する。プロセッサ１００２はまた、リテラル１１０７のセットを維持しながら、プロセスモデル１１０２をペトリネット１１０６に変換する。この段階でグローバルである規定１１０５に基づいて、プロセッサ１００２は、リテラルのサブセットを意味する規定サブセットによって表される複数の区分１１０９、１１１０を保持する区分データオブジェクト１１０８を作成する。図１１には、２つの例示的な区分１１０９、１１１０を示しているが、実際には、ドット及びインデックスｎによって示されるように、区分の数は２つよりも大きくなることに留意されたい。
【００６９】
ペトリネットコレクションデータオブジェクト１１１１には、プロセッサ１００２が、その特定の規定についてのグローバル規定データオブジェクト１１０５からペトリネット１１０６を簡略化することにより、各規定の区分に対して作成する規定固有のペトリネット１１１２、１１１３が存在する。これは、上記のように、ノードのリテラルが他の規定に含まれているが、その規定固有のペトリネットの現在の規定には含まれていないノードをサイレントにすることによって実現される。
【００７０】
ペトリネットコレクションデータオブジェクト１１１１内のペトリネットが簡略化されると、プロセッサ１００２は、各規定固有のペトリネットについて、その規定１１０９、１１１０のそれぞれのプライム事象構造１１１５、１１１６を含む事象構造コレクションデータオブジェクト１１１４を生成する。コレクション１１１５内の事象構造のプライム事象構造及び／またはプレフィックス展開は、上記のようにさらに簡略化されている。最後に、プロセッサ１００２は、規定固有のプライム事象構造１１１５、１１１６ごとに、クリプキ構造などの状態ベースの表現１１１８、１１１９をそれぞれ作成することによって、適合性コレクションデータオブジェクト１１１７を作成する。これで、プロセッサ１００２は、１１１８において各クリプキ構造をステップスルーし、クリプキ構造の各状態の条件が現在のプロセスパラメータ（製造プロセスのセンサからのものなど）と同じであるかどうかを判定することができる。
【００７１】
図１１では、区分データオブジェクト１１０８から開始して、各規定区分の処理が並行して行われることに留意されたい。つまり、図１１は、この段階で複数の水平行に分割でき、その各行を並行して処理することができる。このことは、適合性確認を高速化するために、規定区分ごとに個別の処理インスタンスを作成できるクラウドコンピューティング環境での実装に適している。これらの処理インスタンスは、次の確認を実行する前に、他のインスタンスが終了するのを待つという意味で、同期され得る。他の実施例では、インスタンスの１つが不適合のフラグを立てると、不適合が検出されるために、各処理インスタンスは非同期になる。したがって、各インスタンス／区分が、異なる時間にサンプリングされたプロセスパラメータのセットに対して実行されるかどうかは重要ではない。これらの区分のうちの１つの不適合の出力は、適合性確認に対して引き続き正確である。同時に、並列処理は、全体的な処理時間の短縮というさらなる重要な技術的利点を提供する。リテラルのセットは互いに独立しているので、個々の並列ブランチを同期する必要がないとき、並列化が簡略化され、さらに高速化されることになる。
【００７２】
本開示の広範な一般的範囲から逸脱することなく、多数の変形及び／または修正が、上記の実施形態に行われ得ることは、当業者には理解されよう。したがって、本実施形態は、全ての点で例示的であり、限定的ではないと見なされるべきである。
【図１】
2022501701.tif 000017
【図２】
2022501701.tif 000018
【図３】
2022501701.tif 000019
【図４】
2022501701.tif 000020
【図５ａ】
2022501701.tif 000021
【図５ｂ】
2022501701.tif 000022
【図６】
2022501701.tif 000023
【図７】
2022501701.tif 000024
【図８】
2022501701.tif 000025
【図９】
2022501701.tif 000026
【図１０】
2022501701.tif 000027
【図１１】
2022501701.tif 000028
【国際調査報告】
2022501701.tif 000029
2022501701.tif 000030
2022501701.tif 000031