私はソフトウェアのモデルの一貫性のチェックに取り組んでいます。これを行うには、UML2.0シーケンス図の線形時相論理を作成する必要があります。体に同じツールが他にある場合は、できるだけ早く対応してください。私はあなたに非常に義務があります。私は魅力的なツールが同じためのプラグインを持っていることを発見しました。魅力的なツール（CHecking ARchitectural ModelconsistentY）のソースコードを持っている人はいますか？彼らのウェブサイトでは利用できません。
前もって感謝します。
シーケンス図モデルは私には使えません。
つまり、シーケンス図を作成できますが、基礎となるモデルは本当に厄介です。シーケンス図は、モデルが実際には再利用できない唯一の UML 図です。この投稿で申し訳ありませんが、メタモデルは UML 仕様で十分に開発されておらず、変更するには遅すぎるため、シーケンス図はグラフィカルなままにする必要があると思います!!
問題を理解しているかどうかわかりません。ウィキペディアの記事によると、シーケンス図にはループがないため、対応する LTL 式にはひし形やボックスなどは含まれず、アトミック イベントのシーケンスになるだけですよね?
シーケンス図と対応する LTL 式の例を教えてください。