論文の概要: Animation, Verification and Visualisation of Prolog Transition Systems with ProB

• arxiv url: http://arxiv.org/abs/2607.21192v1
• Date: Thu, 23 Jul 2026 11:16:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-24 18:26:25.384365
• Title: Animation, Verification and Visualisation of Prolog Transition Systems with ProB
• Title（参考訳）: ProBを用いたプロログ遷移システムのアニメーション・検証・可視化
• Abstract要約: 本稿ではProBのPrologアニメーションモードの既存機能と最近の拡張について述べる。 拡張された機能には、統計チェックのシミュレーション、より信頼性の高いトレースリプレイ、ユーザ入力によるトランジション、状態可視化の改善などがある。
• 参考スコア（独自算出の注目度）: 0.2449909275410287
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB's Prolog animation mode and its recent extensions. The extended capabilities include simulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB's new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.
• Abstract（参考訳）: ProBはPrologベースのモデルチェッカー、アニメーター、高レベルの形式仕様のための制約解決器である。 ProBを使用して、Prologの述語で定義された遷移系をアニメーション化して、さまざまなバリデーション技術を適用することもできる。 本稿ではProBのPrologアニメーションモードの既存機能と最近の拡張について述べる。 拡張された機能には、統計チェックのシミュレーション、より信頼性の高いトレースリプレイ、ユーザ入力によるトランジション、状態可視化の改善などがある。 ケーススタディ、特にConnect Fourのようなゲームプレイにおけるさまざまな戦略を評価するために、これらの新機能をケーススタディに適用する。 この機能は、他の多くのアプリケーション、特にProBのEvent-B証明義務のシーケント証明や、インタラクティブな視覚化と組み合わせて教えるデモモデルに有用である。

関連論文リスト

• Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB [0.2676349883103403]
  Event-B は述語論理と集合論に根ざした形式的な方法である。 我々は600以上の証明ルールをPrologにエンコードし、体系的で理解可能な証明分析と構築を可能にした。 証明ルールを Prolog ベースの検証ツール ProB に統合することにより,証明木を視覚化した対話型証明システムを得る。
  論文  参考訳（メタデータ） (2026-07-23T11:16:32Z)
• Self-Prophetic Decoding to Unlock Visual Search in LVLMs [108.77389957341586]
  LVLM(Large Vision-Language Models)は、真のマルチモーダル推論に向けて急速に進化している。 LVLMビジュアルサーチは、訓練後の本質的能力の非互換性と、長い多段階推論コンテキストにおける干渉の2つの主要な課題に直面している。 固有単一ステップ機能を活用してコヒーレントな多ステップ推論を可能にする自己プロヒーレントデコーディングフレームワークであるSeProDを紹介する。
  論文  参考訳（メタデータ） (2026-05-27T17:01:39Z)
• From Prompt to Progression: Taming Video Diffusion Models for Seamless Attribute Transition [57.809291244375345]
  本研究では,スムーズかつ一貫した属性遷移に対する既存モデルの拡張をシンプルかつ効果的に行う手法を提案する。 提案手法は,初期属性フレームから最終属性フレームへの段階的なシフトをフレーム単位に導くことで,各雑音の遅延に対してデータ固有の遷移方向を構築する。 また、属性と動きのダイナミクスを統合した制御属性遷移ベンチマーク(CAT-Bench)を提案する。
  論文  参考訳（メタデータ） (2025-09-24T01:58:22Z)
• XR-VLM: Cross-Relationship Modeling with Multi-part Prompts and Visual Features for Fine-Grained Recognition [20.989787824067143]
  XR-VLMは、相互関係をモデル化することによって微妙な違いを発見する新しいメカニズムである。 マルチパースペクティブな記述をキャプチャするマルチパート・プロンプト学習モジュールを開発した。 提案手法は,現在の最先端手法と比較して,大幅な改善を実現している。
  論文  参考訳（メタデータ） (2025-03-10T08:58:05Z)
• Unsupervised Generative Feature Transformation via Graph Contrastive Pre-training and Multi-objective Fine-tuning [28.673952870674146]
  教師なし特徴変換学習のための測定-事前訓練-ファネチューンパラダイムを開発した。 教師なし特徴集合の実用性測定のために,特徴値の整合性維持の観点から提案する。 生成的変換ファインタニングでは,特徴集合を特徴クロスシーケンス,特徴変換を逐次生成とみなす。
  論文  参考訳（メタデータ） (2024-05-27T06:50:00Z)
• A Transformer Model for Boundary Detection in Continuous Sign Language [55.05986614979846]
  Transformerモデルは、分離された手話認識と連続手話認識の両方に使用される。 トレーニングプロセスは、入力されたビデオから抽出された手指キーポイントの特徴を豊かにする、孤立した手指ビデオを使用する。 トレーニングされたモデルと後処理の手法が組み合わさって、連続した手話ビデオ内の孤立した手話境界を検出する。
  論文  参考訳（メタデータ） (2024-02-22T17:25:01Z)
• TOD-Flow: Modeling the Structure of Task-Oriented Dialogues [77.15457469745364]
  ダイアログを付加した対話データからTOD-Flowグラフを推定する手法を提案する。 推定されたTOD-Flowグラフは、任意の対話モデルと容易に統合することができ、予測性能、透明性、制御性を改善することができる。
  論文  参考訳（メタデータ） (2023-12-07T20:06:23Z)
• Improving Input-label Mapping with Demonstration Replay for In-context Learning [67.57288926736923]
  In-context Learning (ICL)は、大規模な自己回帰言語モデルの出現する能力である。 Sliding Causal Attention (RdSca) と呼ばれる新しいICL法を提案する。 ICL実験において,本手法は入力ラベルマッピングを大幅に改善することを示す。
  論文  参考訳（メタデータ） (2023-10-30T14:29:41Z)
• End-to-End Training of a Neural HMM with Label and Transition Probabilities [36.32865468394113]
  隠れマルコフモデル(HMM)を用いたエンドツーエンドニューラルネットワークトレーニングのための新しいモデリング手法について検討する。 提案手法では,時間統計を暗黙的にエンコードするブランクラベルとは対照的に,セグメント間の遷移に関する明示的で学習可能な確率が存在する。 トランジションモデルトレーニングでは認識性能は向上しないが,アライメント品質に肯定的な影響を与えることがわかった。
  論文  参考訳（メタデータ） (2023-10-04T10:56:00Z)
• On Conditional and Compositional Language Model Differentiable Prompting [75.76546041094436]
  プロンプトは、下流タスクでうまく機能するために、凍結した事前訓練言語モデル(PLM)を適応するための効果的な方法であることが示されている。 タスク命令や入力メタデータを連続的なプロンプトに変換することを学習する新しいモデル Prompt Production System (PRopS) を提案する。
  論文  参考訳（メタデータ） (2023-07-04T02:47:42Z)
• CoReS: Compatible Representations via Stationarity [20.607894099896214]
  ビジュアルサーチシステムでは、互換性のある機能により、古い機能と新しい機能を直接比較することができ、時間とともに相互に使用することができる。 従来学習されていた表現とテキスト互換の表現を学習するための新しい訓練手法であるCoReSを提案する。 トレーニングセットの更新を複数行う場合,我々のトレーニング手順が現在の技術よりも優れており,特に有効であることを示す。
  論文  参考訳（メタデータ） (2021-11-15T09:35:54Z)
• End-to-end Semantic Role Labeling with Neural Transition-based Model [25.921541005563856]
  エンドツーエンドのセマンティックロールラベリング(SRL)が注目されています。 最近の研究は主にグラフベースのニューラルモデルに焦点を当てている。 本稿では,エンドツーエンドSRLのための遷移型ニューラルモデルについて紹介する。
  論文  参考訳（メタデータ） (2021-01-02T07:35:54Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。