Journal of Artificial Intelligence Resarch: Volume 62の論文一覧

Journal of Artificial Intelligence Resarch Vol. 62 (2018)に記載されている内容を一覧にまとめ、機械翻訳を交えて日本語化し掲載します。

目次

論文

An Exhaustive DPLL Algorithm for Model Counting

An Exhaustive DPLL Algorithm for Model Counting / モデルカウントのための網羅的DPLLアルゴリズム

State-of-the-art model counters are based on exhaustive DPLL algorithms, and have been successfully used in probabilistic reasoning, one of the key problems in AI. In this article, we present a new exhaustive DPLL algorithm with a formal semantics, a proof of correctness, and a modular design. The modular design is based on the separation of the core model counting algorithm from SAT solving techniques. We also show that the trace of our algorithm belongs to the language of Sentential Decision Diagrams (SDDs), which is a subset of Decision-DNNFs, the trace of existing state-of-the-art model counters. Still, our experimental analysis shows comparable results against state-of-the-art model counters. Furthermore, we obtain the first top-down SDD compiler, and show orders-of-magnitude improvements in SDD construction time against the existing bottom-up SDD compiler.



最先端のモデルカウンタは、網羅的なDPLLアルゴリズムに基づいており、AIの主要課題の一つである確率的推論において効果的に利用されてきました。本稿では、形式意味論、正しさの証明、モジュール設計を備えた新しい網羅的なDPLLアルゴリズムを紹介します。モジュール設計は、コアとなるモデルカウントアルゴリズムをSAT解決手法から分離することを基本としています。また、本アルゴリズムの軌跡は、既存の最先端のモデルカウンタの軌跡であるDecision-DNNFのサブセットであるSentential Decision Diagrams(SDD)の言語に属していることを示します。それでもなお、実験分析は最先端のモデルカウンタと同等の結果を示しています。さらに、私たちは初めてのトップダウンSDDコンパイラを取得し、既存のボトムアップSDDコンパイラと比較して、SDD構築時間が桁違いに改善されることを示しています。

Verification of Distributed Epistemic Gossip Protocols

Verification of Distributed Epistemic Gossip Protocols / 分散認識ゴシッププロトコルの検証

Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols use as guards formulas from a simple epistemic logic and as statements calls between the agents. They are natural examples of knowledge based programs.We prove here that these protocols are implementable, that their partial correctness is decidable and that termination and two forms of fair termination of these protocols are decidable, as well. To establish these results we show that the definition of semantics and of truth of the underlying logic are decidable.



ゴシッププロトコルは、ポイントツーポイントまたはグループ通信によって、すべてのエージェントが互いの秘密を知っている状況に到達することを目指します。分散認識論的ゴシッププロトコルは、単純な認識論的論理からの式をガードとして、またエージェント間の呼び出し文として用います。これらは知識ベースプログラムの自然な例です。本稿では、これらのプロトコルが実装可能であり、部分的な正しさが決定可能であり、これらのプロトコルの終了と2種類の公正な終了も決定可能であることを証明します。これらの結果を確立するために、基礎となる論理の意味と真理の定義が決定可能であることを示します。

A COP Model For Graph-Constrained Coalition Formation

A COP Model For Graph-Constrained Coalition Formation / グラフ制約付き提携形成のためのCOPモデル

We consider Graph-Constrained Coalition Formation (GCCF), a widely studied subproblem of coalition formation in which the set of valid coalitions is restricted by a graph. We propose COP-GCCF, a novel approach that models GCCF as a COP, and we solve such COP with a highly-parallel approach based on Bucket Elimination executed on the GPU, which is able to exploit the high constraint tightness of COP-GCCF. Results show that our approach outperforms state of the art algorithms (i.e., DyCE and IDPG) by at least one order of magnitude on realistic graphs, i.e., a crawl of the Twitter social graph, both in terms of runtime and memory.



有効な提携の集合がグラフによって制限される、広く研究されている提携形成の部分問題であるグラフ制約付き提携形成(GCCF)を考察します。我々は、GCCFをCOPとしてモデル化する新しいアプローチであるCOP-GCCFを提案します。そして、GPU上で実行されるバケット消去に基づく高度に並列化されたアプローチを用いて、COP-GCCFの高い制約厳密性を活用することで、そのようなCOPを解く。結果は、我々のアプローチが、Twitterソーシャルグラフのクロールといった現実的なグラフにおいて、実行時間とメモリの両方において、最先端のアルゴリズム(すなわち、DyCEおよびIDPG)を少なくとも1桁上回ることを示す。

Resource-bounded Norm Monitoring In Multi-agent Systems

Resource-bounded Norm Monitoring In Multi-agent Systems / マルチエージェントシステムにおけるリソース制約付きノルムモニタリング

Norms allow system designers to specify the desired behaviour of a sociotechnical system. In this way, norms regulate what the social and technical agents in a sociotechnical system should (not) do. In this context, a vitally important question is the development of mechanisms for monitoring whether these agents comply with norms. Proposals on norm monitoring often assume that monitoring has no costs and/or that monitors have unlimited resources to observe the environment and the actions performed by agents. In this paper, we challenge this assumption and propose the first practical resource-bounded norm monitor. Our monitor is capable of selecting the resources to be deployed and use them to check norm compliance with incomplete information about the actions performed and the state of the world. We formally demonstrate the correctness and soundness of our norm monitor and study its complexity. We also demonstrate in randomised simulations and benchmark experiments that our monitor can select monitored resources effectively and efficiently, detecting more norm violations and fulfilments than other tractable optimization approaches and obtaining slightly worse results than intractable optimal approaches.



規範は、システム設計者が社会技術システムの望ましい動作を指定することを可能にします。このように、規範は、社会技術システムにおける社会的エージェントと技術的エージェントが何をすべきか(すべきでないか)を規制します。この文脈において、極めて重要な問題は、これらのエージェントが規範を遵守しているかどうかを監視するメカニズムの開発です。規範監視に関する提案は、監視にはコストがかからない、または監視者が環境とエージェントによって実行される行動を観察するための無制限のリソースを持っていると仮定することが多い。本論文では、この仮定に異議を唱え、初めて実用的なリソース制約型規範モニターを提案します。このモニターは、配備すべきリソースを選択し、実行されたアクションと世界の状態に関する不完全な情報に基づいて、それらを用いて規範の遵守を確認することができます。この規範モニターの正しさと健全性を正式に実証し、その複雑性について検証します。さらに、ランダム化シミュレーションとベンチマーク実験により、このモニターが監視対象リソースを効果的かつ効率的に選択し、他の扱いやすい最適化手法よりも多くの規範違反と規範充足を検出し、扱いにくい最適化手法よりもわずかに劣る結果を得ることを実証します。

MCTS-Minimax Hybrids with State Evaluations

MCTS-Minimax Hybrids with State Evaluations / 状態評価を伴うMCTS-ミニマックスハイブリッド

Monte-Carlo Tree Search (MCTS) has been found to show weaker play than minimax-based search in some tactical game domains. This is partly due to its highly selective search and averaging value backups, which make it susceptible to traps. In order to combine the strategic strength of MCTS and the tactical strength of minimax, MCTS-minimax hybrids have been introduced, embedding shallow minimax searches into the MCTS framework. Their results have been promising even without making use of domain knowledge such as heuristic evaluation functions. This article continues this line of research for the case where evaluation functions are available. Three different approaches are considered, employing minimax with an evaluation function in the rollout phase of MCTS, as a replacement for the rollout phase, and as a node prior to bias move selection. The latter two approaches are newly proposed. Furthermore, all three hybrids are enhanced with the help of move ordering and k-best pruning for minimax. Results show that the use of enhanced minimax for computing node priors results in the strongest MCTS-minimax hybrid investigated in the three test domains of Othello, Breakthrough, and Catch the Lion. This hybrid, called MCTS-IP-M-k, also outperforms enhanced minimax as a standalone player in Breakthrough, demonstrating that at least in this domain, MCTS and minimax can be combined to an algorithm stronger than its parts. Using enhanced minimax for computing node priors is therefore a promising new technique for integrating domain knowledge into an MCTS framework.



モンテカルロ木探索(MCTS)は、一部の戦術ゲーム分野において、ミニマックスベースの探索よりも弱いプレイを示すことが分かっています。これは、MCTSの高度に選択的な探索と平均値のバックアップが罠にかかりやすいことに一因があります。MCTSの戦略的強みとミニマックスの戦術的強みを組み合わせるために、MCTSフレームワークに浅いミニマックス探索を組み込んだMCTS-ミニマックスハイブリッドが導入されました。その結果は、ヒューリスティック評価関数などのドメイン知識を利用しなくても有望です。本稿では、評価関数が利用可能なケースについて、この研究の流れを継続します。評価関数付きミニマックスをMCTSのロールアウトフェーズで使用する方法、ロールアウトフェーズの代替として使用する方法、バイアス移動選択前のノードとして使用する方法の3つの異なるアプローチが検討されます。最後の2つのアプローチは新たに提案されたものです。さらに、これら3つのハイブリッドはすべて、移動順序付けとミニマックスのk-best枝刈りによって強化されています。結果は、ノード事前確率の計算に拡張ミニマックスを用いることで、オセロ、ブレイクスルー、キャッチ・ザ・ライオンの3つのテストドメインにおいて調査された中で最も強力なMCTS-ミニマックスハイブリッドが得られることを示しています。MCTS-IP-M-kと呼ばれるこのハイブリッドは、ブレイクスルーにおいてスタンドアロンプ​​レイヤーとしても拡張ミニマックスを凌駕しており、少なくともこのドメインにおいては、MCTSとミニマックスを組み合わせることで、個々の要素よりも強力なアルゴリズムを実現できることを示しています。したがって、ノード事前確率の計算に拡張ミニマックスを用いることは、ドメイン知識をMCTSフレームワークに統合するための有望な新技術です。

Solving Large Problems with Heuristic Search: General-Purpose Parallel External-Memory Search

Solving Large Problems with Heuristic Search: General-Purpose Parallel External-Memory Search / ヒューリスティック探索による大規模問題の解決:汎用並列外部メモリ探索

Classic best-first heuristic search algorithms, like A*, record every unique state they encounter in RAM, making them infeasible for solving large problems. In this paper, we demonstrate how best-first search can be scaled to solve much larger problems by exploiting disk storage and parallel processing and, in some cases, slightly relaxing the strict best-first node expansion order. Some previous disk-based search algorithms abandon best-first search order in an attempt to increase efficiency. We present two case studies showing that A*, when augmented with Delayed Duplicate Detection, can actually be more efficient than these non-best-first search orders. First, we present a straightforward external variant of A*, called PEDAL, that slightly relaxes best-first order in order to be I/O efficient in both theory and practice, even on problems featuring real-valued node costs. Because it is easy to parallelize, PEDAL can be faster than in-memory IDA* even on domains with few duplicate states, such as the sliding-tile puzzle. Second, we present a variant of PEDAL, called PE2A*, that uses partial expansion to handle problems that have large branching factors. When tested on the problem of Multiple Sequence Alignment, PE2A* is the first algorithm capable of solving the entire Reference Set 1 of the standard BAliBASE benchmark using a biologically accurate cost function. This work shows that classic best-first algorithms like A* can be applied to large real-world problems. We also provide a detailed implementation guide with source code both for generic parallel disk-based best-first search and for Multiple Sequence Alignment with a biologically accurate cost function. Given its effectiveness as a general-purpose problem-solving method, we hope that this makes parallel and disk-based search accessible to a wider audience.



A*のような従来のベストファースト・ヒューリスティック探索アルゴリズムは、遭遇するすべての一意の状態をRAMに記録するため、大規模な問題の解決には適していません。本稿では、ディスクストレージと並列処理を活用し、場合によっては厳格なベストファースト・ノード拡張順序をわずかに緩和することで、ベストファースト探索をスケールアップし、はるかに大規模な問題を解決できることを示します。従来のディスクベースの探索アルゴリズムの中には、効率性を高めるためにベストファースト探索順序を放棄しているものもあります。本稿では、遅延重複検出機能を追加したA*が、実際にはこれらの非ベストファースト探索順序よりも効率的であることを示す2つのケーススタディを紹介します。まず、実数値ノードコストを伴う問題でも、理論と実践の両方でI/O効率を高めるためにベストファースト順序をわずかに緩和した、A*の単純な外部バリアントであるPEDALを紹介します。並列化が容易なため、PEDALは、スライディングタイルパズルのように重複状態が少ない領域でも、インメモリIDA*よりも高速です。次に、大きな分岐因子を持つ問題を処理するために部分拡張を使用するPEDALのバリアントであるPE2A*を紹介します。多重配列アライメントの問題でテストしたところ、PE2A*は、生物学的に正確なコスト関数を使用して標準BAliBASEベンチマークのReference Set 1全体を解くことができる最初のアルゴリズムです。本研究は、A*のような古典的なベストファーストアルゴリズムが、実際の大規模な問題に適用できることを示しています。また、汎用的な並列ディスクベースのベストファーストサーチと、生物学的に正確なコスト関数を用いたマルチプルシーケンスアライメントの両方について、ソースコードを含む詳細な実装ガイドも提供しています。汎用的な問題解決手法としての有効性を考慮すると、これにより並列およびディスクベースのサーチがより幅広いユーザーに利用可能になることを期待しています。

Viewpoint: Artificial Intelligence Government (Gov. 3.0): The UAE Leading Model

Viewpoint: Artificial Intelligence Government (Gov. 3.0): The UAE Leading Model / 視点:人工知能政府(Gov. 3.0):UAEの主要モデル

The United Arab Emirates (UAE) is the first country in the world to appoint a State Minister for Artificial Intelligence (AI). The UAE is embracing AI in society at the governmental level, which is leading to a new generations of digital government (which we are labeling Gov. 3.0). This paper argues that the decision to embrace AI will lead to positive impacts on society, including businesses, organizations and individuals, as well as on the AI industry itself. This paper discusses the societal impacts of AI at a macro (country-wide) level.This article is part of the special track on AI and Society.



アラブ首長国連邦(UAE)は、世界で初めて人工知能(AI)担当国務大臣を任命した国です。UAEは政府レベルで社会にAIを導入しており、これは新世代のデジタル政府(Gov. 3.0と名付けています)へとつながっています。本稿では、AIを採用するという決定が、企業、組織、個人を含む社会、そしてAI業界自体にプラスの影響を与えると主張しています。本稿では、マクロレベル(国全体)でのAIの社会的影響について議論します。本稿は、「AIと社会」に関する特別トラックの一部です。

Solving Multi-agent Path Finding on Strongly Biconnected Digraphs

Solving Multi-agent Path Finding on Strongly Biconnected Digraphs / 強2連結有向グラフにおけるマルチエージェント経路探索の解決

Much of the literature on suboptimal, polynomial-time algorithms for multi-agent path finding focuses on undirected graphs, where motion is permitted in both directions along a graph edge. Despite this, traveling on directed graphs is relevant in navigation domains, such as path finding in games, and asymmetric communication networks.We consider multi-agent path finding on strongly biconnected directed graphs. We show that all instances with at least two unoccupied positions have a solution, except for a particular, degenerate subclass where the graph has a cyclic shape. We present diBOX, an algorithm for multi-agent path finding on strongly biconnected directed graphs. diBOX runs in polynomial time, computes suboptimal solutions and is complete for instances on strongly biconnected digraphs with at least two unoccupied positions. We theoretically analyze properties of the algorithm and properties of strongly biconnected directed graphs that are relevant to our approach. We perform a detailed empirical analysis of diBOX, showing a good scalability. To our knowledge, our work is the first study of multi-agent path finding focused on directed graphs.



マルチエージェント経路探索における準最適な多項式時間アルゴリズムに関する文献の多くは、グラフのエッジに沿って双方向の移動が許容される無向グラフに焦点を当てています。しかしながら、有向グラフ上の移動は、ゲームにおける経路探索や非対称通信ネットワークなどのナビゲーション分野において重要です。本稿では、強2連結有向グラフ上のマルチエージェント経路探索について考察します。グラフが循環形状を持つ特定の退化したサブクラスを除き、少なくとも2つの空き位置を持つすべてのインスタンスには解が存在することを示します。本稿では、強2連結有向グラフ上のマルチエージェント経路探索アルゴリズムdiBOXを紹介します。diBOXは多項式時間で実行され、準最適な解を計算し、少なくとも2つの空き位置を持つ強2連結有向グラフ上のインスタンスに対して完全です。本稿では、本アルゴリズムの特性と、本手法に関連する強2連結有向グラフの特性を理論的に分析します。diBOXの詳細な実証分析を行い、良好なスケーラビリティを示します。我々の知る限り、本研究は有向グラフに焦点を当てたマルチエージェント経路探索の研究としては初めてのものです。

Nash Stable Outcomes in Fractional Hedonic Games: Existence, Efficiency and Computation

Nash Stable Outcomes in Fractional Hedonic Games: Existence, Efficiency and Computation / 分数ヘドニックゲームにおけるナッシュ安定結果:存在、効率、計算

We consider fractional hedonic games, a subclass of coalition formation games that can be succinctly modeled by means of a graph in which nodes represent agents and edge weights the degree of preference of the corresponding endpoints. The happiness or utility of an agent for being in a coalition is the average value she ascribes to its members. We adopt Nash stable outcomes as the target solution concept; that is we focus on states in which no agent can improve her utility by unilaterally changing her own group. We provide existence, efficiency and complexity results for games played on both general and specific graph topologies. As to the efficiency results, we mainly study the quality of the best Nash stable outcome and refer to the ratio between the social welfare of an optimal coalition structure and the one of such an equilibrium as to the price of stability. In this respect, we remark that a best Nash stable outcome has a natural meaning of stability, since it is the optimal solution among the ones which can be accepted by selfish agents. We provide upper and lower bounds on the price of stability for different topologies, both in case of weighted and unweighted edges. Beside the results for general graphs, we give refined bounds for various specific cases, such as triangle-free, bipartite graphs and tree graphs. For these families, we also show how to efficiently compute Nash stable outcomes with provable good social welfare.



我々は、分数ヘドニックゲーム(分数ヘドニックゲーム)を考察します。これは、ノードがエージェントを表し、エッジが対応するエンドポイントの選好度を表すグラフによって簡潔にモデル化できる、提携形成ゲームのサブクラスです。エージェントが提携に参加することによる幸福度または効用は、そのエージェントがメンバーに与える平均値です。目標解の概念として、ナッシュ安定結果を採用します。すなわち、どのエージェントも自身のグループを一方的に変更することで効用を向上させることができない状態に焦点を当てる。我々は、一般グラフトポロジと特定グラフトポロジの両方でプレイされるゲームについて、存在性、効率性、および複雑性の結果を提供します。効率性の結果については、主に最良のナッシュ安定結果の質を研究し、最適な提携構造の社会福祉と、安定性の価格に関する均衡の社会福祉との比を参照します。この点において、最良のナッシュ安定結果は、利己的なエージェントが受け入れることができる解の中で最適な解であるため、安定性という自然な意味を持つことを指摘します。我々は、重み付きエッジと重みなしエッジの両方において、様々なトポロジーの安定性の価格の上限と下限を与える。一般的なグラフの結果に加えて、三角形のないグラフ、二部グラフ、木グラフなど、様々な特定のケースに対する洗練された境界を与える。これらのファミリーに対して、証明可能な良好な社会的厚生を持つナッシュ安定な結果を効率的に計算する方法も示す。

Axiomatic Characterization of Game-Theoretic Centrality

Axiomatic Characterization of Game-Theoretic Centrality / ゲーム理論的中心性の公理的特徴付け

One of the fundamental research challenges in network science is centrality analysis, i.e., identifying the nodes that play the most important roles in the network. In this article, we focus on the game-theoretic approach to centrality analysis. While various centrality indices have been recently proposed based on this approach, it is still unknown how general is the game-theoretic approach to centrality and what distinguishes some game-theoretic centralities from others. In this article, we attempt to answer this question by providing the first axiomatic characterization of game-theoretic centralities. Specifically, we show that every possible centrality measure can be obtained following the game-theoretic approach. Furthermore, we study three natural classes of game-theoretic centrality, and prove that they can be characterized by certain intuitive properties pertaining to the well-known notion of Fairness due to Myerson.



ネットワーク科学における基本的な研究課題の一つは中心性分析、すなわちネットワークで最も重要な役割を果たすノードを特定することです。本稿では、中心性分析に対するゲーム理論的アプローチに焦点を当てる。このアプローチに基づいて最近様々な中心性指標が提案されているが、中心性に対するゲーム理論的アプローチがどれほど一般的なのか、また、あるゲーム理論的中心性と他の中心性との違いは何かは未だ不明です。本稿では、ゲーム理論的中心性の初めての公理的特徴付けを提供することで、この疑問への答えを試みる。具体的には、ゲーム理論的アプローチに従って、あらゆる可能な中心性尺度を得ることができることを示す。さらに、我々はゲーム理論的中心性の3つの自然なクラスを研究し、それらがMyersonによる公平性のよく知られた概念に関連する特定の直感的な特性によって特徴付けられることを証明します。

Extending Classical Planning with State Constraints: Heuristics and Search for Optimal Planning

Extending Classical Planning with State Constraints: Heuristics and Search for Optimal Planning / 状態制約を伴う古典的計画の拡張:ヒューリスティックと最適計画の探索

We present a principled way of extending a classical AI planning formalism with systems of state constraints, which relate – sometimes determine – the values of variables in each state traversed by the plan. This extension occupies an attractive middle ground between expressivity and complexity. It enables modelling a new range of problems, as well as formulating more efficient models of classical planning problems. An example of the former is planning-based control of networked physical systems – power networks, for example – in which a local, discrete control action can have global effects on continuous quantities, such as altering flows across the entire network. At the same time, our extension remains decidable as long as the satisfiability of sets of state constraints is decidable, including in the presence of numeric state variables, and we demonstrate that effective techniques for cost-optimal planning known in the classical setting – in particular, relaxation-based admissible heuristics – can be adapted to the extended formalism. In this paper, we apply our approach to constraints in the form of linear or non-linear equations over numeric state variables, but the approach is independent of the type of state constraints, as long as there exists a procedure that decides their consistency. The planner and the constraint solver interact through a well-defined, narrow interface, in which the solver requires no specialisation to the planning context.



我々は、古典的なAI計画形式主義を、計画が通過する各状態における変数の値を関連付ける(場合によっては決定する)状態制約システムを用いて拡張する、原理的な方法を提示します。この拡張は、表現力と複雑性の間の魅力的な中間点を占める。これにより、新しい範囲の問題のモデリングが可能になるだけでなく、古典的な計画問題のより効率的なモデル化も可能になります。前者の例としては、ネットワーク化された物理システム(例えば電力網)の計画ベース制御が挙げられます。このシステムでは、局所的な離散制御アクションが、ネットワーク全体の流れを変えるなど、連続量に対してグローバルな影響を及ぼす可能性があります。同時に、数値状態変数の存在を含め、状態制約セットの充足可能性が決定可能である限り、我々の拡張は決定可能であり、古典的な設定で知られているコスト最適計画のための効果的な手法、特に緩和ベースの許容ヒューリスティックが、拡張された形式主義に適用できることを示す。本稿では、数値状態変数に対する線形または非線形方程式の形の制約に我々のアプローチを適用するが、整合性を決定する手順が存在する限り、このアプローチは状態制約の種類に依存しない。プランナーと制約ソルバーは、明確に定義された狭いインターフェースを介して相互作用し、ソルバーはプランニングコンテキストへの特化を必要としない。

Incentive-Compatible Mechanisms for Norm Monitoring in Open Multi-Agent Systems

Incentive-Compatible Mechanisms for Norm Monitoring in Open Multi-Agent Systems / インセンティブ適合メカニズムオープンマルチエージェントシステムにおける規範監視

We consider the problem of detecting norm violations in open multi-agent systems (MAS). We show how, using ideas from scrip systems, we can design mechanisms where the agents comprising the MAS are incentivised to monitor the actions of other agents for norm violations. The cost of providing the incentives is not borne by the MAS and does not come from fines charged for norm violations (fines may be impossible to levy in a system where agents are free to leave and rejoin again under a different identity). Instead, monitoring incentives come from (scrip) fees for accessing the services provided by the MAS. In some cases, perfect monitoring (and hence enforcement) can be achieved: no norms will be violated in equilibrium. In other cases, we show that, while it is impossible to achieve perfect enforcement, we can get arbitrarily close; we can make the probability of a norm violation in equilibrium arbitrarily small. We show using simulations that our theoretical results, which apply to systems with a large number of agents, hold for multi-agent systems with as few as 1000 agents–the system rapidly converges to the steady-state distribution of scrip tokens necessary to ensure monitoring and then remains close to the steady state.



我々は、オープンマルチエージェントシステム(MAS)における規範違反の検出問題について考察します。スクリプシステムのアイデアを用いて、MASを構成するエージェントが他のエージェントの行動における規範違反を監視するインセンティブを付与するメカニズムを設計する方法を示す。インセンティブ提供のコストはMASが負担するものではなく、規範違反に対して課される罰金からも生じることはない(エージェントが自由に離脱し、別のアイデンティティで再加入できるシステムでは、罰金を課すことは不可能かもしれない)。その代わりに、監視インセンティブはMASが提供するサービスへのアクセスに対する(スクリプ)料金から生じる。場合によっては、完全な監視(ひいては執行)が達成可能であり、均衡状態において規範違反は発生しません。また、完全な執行は不可能であるものの、それに任意に近づくことができること、すなわち均衡状態における規範違反の確率を任意に小さくすることができることを示します。シミュレーションを用いて、多数のエージェントを含むシステムに適用される理論的結果が、わずか1000エージェントのマルチエージェントシステムにも当てはまることを示します。システムは、監視を保証するために必要なスクリップトークンの定常分布に急速に収束し、その後は定常状態に近い状態を維持します。

The Power of Verification for Greedy Mechanism Design

The Power of Verification for Greedy Mechanism Design / 貪欲メカニズム設計における検証の威力

Greedy algorithms are known to provide, in polynomial time, near optimal approximation guarantees for Combinatorial Auctions (CAs) with multidimensional bidders. It is known that truthful greedy-like mechanisms for CAs with multi-minded bidders do not achieve good approximation guarantees.In this work, we seek a deeper understanding of greedy mechanism design and investigate under which general assumptions, we can have efficient and truthful greedy mechanisms for CAs. Towards this goal, we use the framework of priority algorithms and weak and strong verification, where the bidders are not allowed to overbid on their winning set or on any subset of this set, respectively. We provide a complete characterization of the power of weak verification showing that it is sufficient and necessary for any greedy fixed priority algorithm to become truthful with the use of money or not, depending on the ordering of the bids. Moreover, we show that strong verification is sufficient and necessary to obtain a 2-approximate truthful mechanism with money, based on a known greedy algorithm, for the problem of submodular CAs in finite bidding domains. Our proof is based on an interesting structural analysis of the strongly connected components of the declaration graph.



貪欲アルゴリズムは、多次元入札者による組み合わせオークション(CA)に対して、多項式時間でほぼ最適な近似保証を提供することが知られています。複数の入札者を持つCAの誠実な貪欲的メカニズムは、良好な近似保証を達成しないことが知られています。本研究では、貪欲メカニズムの設計をより深く理解し、どのような一般的な仮定の下で、CAに効率的かつ誠実な貪欲メカニズムを実装できるかを調査します。この目標達成に向けて、入札者が自身の落札セットまたはそのサブセットに対してそれぞれ過剰入札を許さない、優先度アルゴリズムと弱い検証および強い検証の枠組みを用います。我々は弱い検証の有効性を完全に特徴付け、任意の貪欲な固定優先度アルゴリズムが、入札の順序に応じて、金銭の使用の有無に応じて誠実になるかそうでないかが十分かつ必要であることを示す。さらに、有限入札領域における劣モジュラCAの問題に対して、既知の貪欲アルゴリズムに基づく、金銭を用いた2近似の誠実メカニズムを得るためには、強い検証が十分かつ必要であることを示す。我々の証明は、宣言グラフの強連結成分の興味深い構造分析に基づいています。

Column Generation Algorithms for Constrained POMDPs

Column Generation Algorithms for Constrained POMDPs / 制約付きPOMDPのための列生成アルゴリズム

In several real-world domains it is required to plan ahead while there are finite resources available for executing the plan. The limited availability of resources imposes constraints on the plans that can be executed, which need to be taken into account while computing a plan. A Constrained Partially Observable Markov Decision Process (Constrained POMDP) can be used to model resource-constrained planning problems which include uncertainty and partial observability. Constrained POMDPs provide a framework for computing policies which maximize expected reward, while respecting constraints on a secondary objective such as cost or resource consumption. Column generation for linear programming can be used to obtain Constrained POMDP solutions. This method incrementally adds columns to a linear program, in which each column corresponds to a POMDP policy obtained by solving an unconstrained subproblem. Column generation requires solving a potentially large number of POMDPs, as well as exact evaluation of the resulting policies, which is computationally difficult. We propose a method to solve subproblems in a two-stage fashion using approximation algorithms. First, we use a tailored point-based POMDP algorithm to obtain an approximate subproblem solution. Next, we convert this approximate solution into a policy graph, which we can evaluate efficiently. The resulting algorithm is a new approximate method for Constrained POMDPs in single-agent settings, but also in settings in which multiple independent agents share a global constraint. Experiments based on several domains show that our method outperforms the current state of the art.



現実世界の多くの分野では、計画実行に利用できるリソースが限られている中で、事前に計画を立てる必要があります。利用可能なリソースが限られているため、実行可能な計画に制約が課せられ、計画の計算時にはこれを考慮する必要があります。制約付き部分観測マルコフ決定過程(制約付きPOMDP)は、不確実性と部分観測性を含むリソース制約付き計画問題をモデル化するために使用できます。制約付きPOMDPは、コストやリソース消費などの二次目的に対する制約を尊重しながら、期待報酬を最大化するポリシーを計算するためのフレームワークを提供します。線形計画法の列生成は、制約付きPOMDP解を得るために使用できます。この手法は、線形計画に列を段階的に追加していきます。各列は、制約のない部分問題を解くことで得られるPOMDPポリシーに対応します。列生成では、潜在的に多数のPOMDPを解き、結果として得られるポリシーを正確に評価する必要があり、これは計算的に困難です。近似アルゴリズムを用いて、2段階方式で部分問題を解く手法を提案します。まず、カスタマイズされたポイントベースPOMDPアルゴリズムを用いて、部分問題の近似解を得る。次に、この近似解を効率的に評価できるポリシーグラフに変換します。このアルゴリズムは、単一エージェント設定だけでなく、複数の独立エージェントがグローバル制約を共有する設定においても、制約付きPOMDPに対する新しい近似手法となります。複数のドメインに基づく実験により、本手法が現在の最先端技術よりも優れていることが示されました。

Counterexample-Guided Cartesian Abstraction Refinement for Classical Planning

Counterexample-Guided Cartesian Abstraction Refinement for Classical Planning / 古典的計画のための反例誘導カルティシアン抽象化の洗練

Counterexample-guided abstraction refinement (CEGAR) is a method for incrementally computing abstractions of transition systems. We propose a CEGAR algorithm for computing abstraction heuristics for optimal classical planning. Starting from a coarse abstraction of the planning task, we iteratively compute an optimal abstract solution, check if and why it fails for the concrete planning task and refine the abstraction so that the same failure cannot occur in future iterations. A key ingredient of our approach is a novel class of abstractions for classical planning tasks that admits efficient and very fine-grained refinement. Since a single abstraction usually cannot capture enough details of the planning task, we also introduce two methods for producing diverse sets of heuristics within this framework, one based on goal atoms, the other based on landmarks. In order to sum their heuristic estimates admissibly we introduce a new cost partitioning algorithm called saturated cost partitioning. We show that the resulting heuristics outperform other state-of-the-art abstraction heuristics in many benchmark domains.



反例誘導抽象化改良(CEGAR)は、遷移システムの抽象化を段階的に計算する手法です。本稿では、最適な古典的計画のための抽象化ヒューリスティックを計算するためのCEGARアルゴリズムを提案します。計画タスクの粗い抽象化から始めて、最適な抽象解を反復的に計算し、具体的な計画タスクでそれが失敗するかどうか、また失敗する理由を確認し、将来の反復で同じ失敗が発生しないように抽象化を改良します。我々のアプローチの重要な要素は、従来の計画タスクに対する、効率的かつ非常に細分化された改良を可能にする新たな抽象化クラスです。単一の抽象化では通常、計画タスクの詳細を十分に捉えることができないため、この枠組みの中で多様なヒューリスティックセットを生成するための2つの手法も導入します。1つはゴールアトムに基づく手法、もう1つはランドマークに基づく手法です。これらのヒューリスティック推定値を許容可能な形で合計するために、飽和コスト分割と呼ばれる新しいコスト分割アルゴリズムを導入します。結果として得られたヒューリスティックは、多くのベンチマークドメインにおいて、他の最先端の抽象化ヒューリスティックよりも優れた性能を示す。

ScottyActivity: Mixed Discrete-Continuous Planning with Convex Optimization

ScottyActivity: Mixed Discrete-Continuous Planning with Convex Optimization / ScottyActivity: 凸最適化を用いた離散・連続混合計画

The state of the art practice in robotics planning is to script behaviors manually, where each behavior is typically generated using trajectory optimization. However, in order for robots to be able to act robustly and adapt to novel situations, they need to plan these activity sequences autonomously. Since the conditions and effects of these behaviors are tightly coupled through time, state and control variables, many problems require that the tasks of activity planning and trajectory optimization are considered together. There are two key issues underlying effective hybrid activity and trajectory planning: the sufficiently accurate modeling of robot dynamics and the capability of planning over long horizons. Hybrid activity and trajectory planners that employ mixed integer programming within a discrete time formulation are able to accurately model complex dynamics for robot vehicles, but are often restricted to relatively short horizons. On the other hand, current hybrid activity planners that employ continuous time formulations can handle longer horizons but they only allow actions to have continuous effects with constant rate of change, and restrict the allowed state constraints to linear inequalities. This is insufficient for many robotic applications and it greatly limits the expressivity of the problems that these approaches can solve. In this work we present the ScottyActivity planner, that is able to generate practical hybrid activity and motion plans over long horizons by employing recent methods in convex optimization combined with methods for planning with relaxed plan graphs and heuristic forward search. Unlike other continuous time planners, ScottyActivity can solve a broad class of robotic planning problems by supporting convex quadratic constraints on state variables and control variables that are jointly constrained and that affect multiple state variables simultaneously. In order to support planning over long horizons, ScottyActivity does not resort to time, state or control variable discretization. While straightforward formulations of consistency checks are not convex and do not scale, we present an efficient convex formulation, in the form of a Second Order Cone Program (SOCP), that is very fast to solve. We also introduce several new realistic domains that demonstrate the capabilities and scalability of our approach, and their simplified linear versions, that we use to compare with other state of the art planners. This work demonstrates the power of integrating advanced convex optimization techniques with discrete search methods and paves the way for extensions dealing with non-convex disjoint constraints, such as obstacle avoidance.



ロボット工学における計画の最先端の手法は、行動を手動でスクリプト化することです。各行動は通常、軌道最適化を用いて生成されます。しかし、ロボットがロバストに行動し、新しい状況に適応するためには、これらの行動シーケンスを自律的に計画する必要があります。これらの行動の条件と影響は、時間、状態、制御変数によって密接に結合されているため、多くの問題では、行動計画と軌道最適化のタスクを一緒に考慮する必要があります。効果的なハイブリッド行動計画と軌道計画には、ロボットダイナミクスの十分に正確なモデリングと、長期的な計画能力という2つの重要な課題があります。離散時間定式化において混合整数計画法を用いるハイブリッド行動計画と軌道計画器は、ロボット車両の複雑なダイナミクスを正確にモデル化できますが、比較的短い期間に限定されることがよくあります。一方、連続時間定式化を用いる現在のハイブリッド行動計画器は、より長い期間に対応できますが、一定の変化率を持つ連続的な効果を持つ行動しか許可せず、許容される状態制約は線形不等式に制限されます。これは多くのロボット応用には不十分であり、これらのアプローチが解決できる問題の表現力を大きく制限します。本研究では、ScottyActivityプランナーを紹介します。このプランナーは、最新の凸最適化手法と、緩和プラングラフおよびヒューリスティックフォワードサーチを用いた計画手法を組み合わせることで、長期にわたる実用的なハイブリッドな活動計画と動作計画を生成できます。他の連続時間プランナーとは異なり、ScottyActivityは、状態変数と制御変数に凸二次制約を適用することで、幅広いロボット計画問題を解くことができます。これらの制約は、複数の状態変数に同時に影響を与える共同制約です。長期にわたる計画をサポートするために、ScottyActivityは時間、状態、または制御変数の離散化に頼っていません。一貫性チェックの単純な定式化は凸ではなくスケールしませんが、本研究では、非常に高速に解ける効率的な凸定式化を二次円錐計画(SOCP)の形で提示します。また、本アプローチの能力とスケーラビリティを示すいくつかの新しい現実的な領域と、それらの簡略化された線形バージョンを紹介し、他の最先端のプランナーと比較します。この研究は、高度な凸最適化手法と離散探索手法を統合する威力を実証し、障害物回避などの非凸分離制約を扱う拡張への道を開きます。

Exploiting Partial Assignments for Efficient Evaluation of Answer Set Programs with External Source Access

Exploiting Partial Assignments for Efficient Evaluation of Answer Set Programs with External Source Access / 外部ソースアクセスを備えた解集合プログラムの効率的な評価のための部分割り当ての活用

Answer Set Programming (ASP) is a well-known declarative problem solving approach based on nonmonotonic logic programs, which has been successfully applied to a wide range of applications in artificial intelligence and beyond. To address the needs of modern applications, HEX-programs were introduced as an extension of ASP with external atoms for accessing information outside programs via an API style bi-directional interface mechanism. To evaluate such programs, conflict-driving learning algorithms for SAT and ASP solving have been extended in order to capture the semantics of external atoms. However, a drawback of the state-of-the-art approach is that external atoms are only evaluated under complete assignments (i.e., input to the external source) while in practice, their values often can be determined already based on partial assignments alone (i.e., from incomplete input to the external source). This prevents early backtracking in case of conflicts, and hinders more efficient evaluation of HEX-programs. We thus extend the notion of external atoms to allow for three-valued evaluation under partial assignments, while the two-valued semantics of the overall HEX-formalism remains unchanged. This paves the way for three enhancements: first, to evaluate external sources at any point during model search, which can trigger learning knowledge about the source behavior and/or early backtracking in the spirit of theory propagation in SAT modulo theories (SMT). Second, to optimize the knowledge learned in terms of so-called nogoods, which roughly speaking are impossible input-output configurations. Shrinking nogoods to their relevant input part leads to more effective search space pruning. And third, to make a necessary minimality check of candidate answer sets more efficient by exploiting early external evaluation calls. As this check usually accounts for a large share of the total runtime, optimization is here particularly important. We further present an experimental evaluation of an implementation of a novel HEX-algorithm that incorporates these enhancements using a benchmark suite. Our results demonstrate a clear efficiency gain over the state-of-the-art HEX-solver for the benchmarks, and provide insights regarding the most effective combinations of solver configurations.



解答セットプログラミング(ASP)は、非単調論理プログラムに基づく宣言的な問題解決手法として広く知られており、人工知能をはじめとする幅広いアプリケーションに効果的に適用されてきました。現代のアプリケーションのニーズに応えるため、APIスタイルの双方向インターフェースメカニズムを介してプログラム外部の情報にアクセスするための外部アトムを備えたASPの拡張として、HEXプログラムが導入されました。このようなプログラムを評価するため、SATおよびASP解決のための衝突駆動型学習アルゴリズムが拡張され、外部アトムのセマンティクスを捕捉できるようになりました。しかし、この最先端の手法の欠点は、外部アトムは完全な代入(つまり、外部ソースへの入力)のもとでのみ評価されるのに対し、実際には、その値は部分的な代入(つまり、外部ソースへの不完全な入力)のみに基づいて既に決定できることが多いことです。これにより、衝突が発生した場合の早期のバックトラックが妨げられ、HEXプログラムのより効率的な評価が妨げられます。そこで我々は、外部アトムの概念を拡張し、部分割り当ての下での3値評価を可能にする一方で、HEX形式全体の2値セマンティクスは変更しない。これにより、3つの機能強化が可能になります。第一に、モデル探索中の任意の時点で外部ソースを評価します。これにより、ソースの挙動に関する知識の学習や、SATモジュロ理論(SMT)における理論伝播の精神に基づく早期バックトラッキングをトリガーすることができます。第二に、いわゆるnogoods(大まかに言えば、あり得ない入出力構成)に関して学習した知識を最適化します。nogoodsを関連する入力部分に縮小することで、より効果的な探索空間の枝刈りが可能になります。第三に、早期の外部評価呼び出しを活用することで、候補解集合の必要な最小性チェックをより効率的にします。このチェックは通常、全体の実行時間の大部分を占めるため、ここでは最適化が特に重要になります。さらに、これらの機能強化を組み込んだ新しいHEXアルゴリズムの実装をベンチマークスイートを用いて実験的に評価します。我々の結果は、ベンチマークにおいて最先端のHEXソルバーと比較して明確な効率向上を示し、ソルバー構成の最も効果的な組み合わせに関する知見を提供します。

Lifted Relational Neural Networks: Efficient Learning of Latent Relational Structures

Lifted Relational Neural Networks: Efficient Learning of Latent Relational Structures / Lifted Relational Neural Networks: 潜在的関係構造の効率的な学習

We propose a method to combine the interpretability and expressive power of firstorder logic with the effectiveness of neural network learning. In particular, we introduce a lifted framework in which first-order rules are used to describe the structure of a given problem setting. These rules are then used as a template for constructing a number of neural networks, one for each training and testing example. As the different networks corresponding to different examples share their weights, these weights can be efficiently learned using stochastic gradient descent. Our framework provides a flexible way for implementing and combining a wide variety of modelling constructs. In particular, the use of first-order logic allows for a declarative specification of latent relational structures, which can then be efficiently discovered in a given data set using neural network learning. Experiments on 78 relational learning benchmarks clearly demonstrate the effectiveness of the framework.



我々は、一階述語論理の解釈可能性と表現力を、ニューラルネットワーク学習の有効性と組み合わせる手法を提案します。具体的には、与えられた問題設定の構造を記述するために一階述語規則を用いるリフトフレームワークを導入します。これらの規則は、訓練例とテスト例ごとに1つずつ、複数のニューラルネットワークを構築するためのテンプレートとして用いられます。異なる例に対応する異なるネットワークは重みを共有するため、これらの重みは確率的勾配降下法を用いて効率的に学習できます。我々のフレームワークは、多様なモデリング構成要素を実装および組み合わせるための柔軟な方法を提供します。特に、一階述語論理を用いることで、潜在的な関係構造を宣言的に指定することが可能となり、ニューラルネットワーク学習を用いて、与えられたデータセットから効率的に発見することができます。78の関係学習ベンチマークを用いた実験は、このフレームワークの有効性を明確に実証しています。

Viewpoint: When Will AI Exceed Human Performance? Evidence from AI Experts

Viewpoint: When Will AI Exceed Human Performance? Evidence from AI Experts / 視点: AIはいつ人間のパフォーマンスを超えるのか? AI専門家によるエビデンス

Advances in artificial intelligence (AI) will transform modern life by reshaping transportation, health, science, finance, and the military. To adapt public policy, we need to better anticipate these advances. Here we report the results from a large survey of machine learning researchers on their beliefs about progress in AI. Researchers predict AI will outperform humans in many activities in the next ten years, such as translating languages (by 2024), writing high-school essays (by 2026), driving a truck (by 2027), working in retail (by 2031), writing a bestselling book (by 2049), and working as a surgeon (by 2053). Researchers believe there is a 50% chance of AI outperforming humans in all tasks in 45 years and of automating all human jobs in 120 years, with Asian respondents expecting these dates much sooner than North Americans. These results will inform discussion amongst researchers and policymakers about anticipating and managing trends in AI.This article is part of the special track on AI and Society.



人工知能(AI)の進歩は、交通、健康、科学、金融、軍事を再編することで現代生活を一変させるでしょう。公共政策を適応させるには、これらの進歩をより適切に予測する必要があります。ここでは、機械学習研究者へのAIの進歩に関する見解に関する大規模調査の結果を報告します。研究者たちは、今後10年間でAIが多くの活動で人間を上回ると予測しており、これには言語翻訳(2024年まで)、高校のエッセイ執筆(2026年まで)、トラック運転(2027年まで)、小売業(2031年まで)、ベストセラー本の執筆(2049年まで)、外科医として働くこと(2053年まで)などが含まれます。研究者たちは、45年後にはAIがすべてのタスクで人間を上回り、120年後には人間の仕事がすべて自動化される可能性が50%あると考えています。アジアの回答者は、これらの日付が北米よりもはるかに早いと予想しています。これらの結果は、AIのトレンドを予測し、管理することに関する研究者や政策立案者間の議論に有益な情報となるでしょう。本稿はAIと社会に関する特別トラックの一部です。

Computing Hierarchical Finite State Controllers With Classical Planning

Computing Hierarchical Finite State Controllers With Classical Planning / 古典的計画を用いた階層的有限状態制御器の計算

Finite State Controllers (FSCs) are an effective way to compactly represent sequential plans. By imposing appropriate conditions on transitions, FSCs can also represent generalized plans (plans that solve a range of planning problems from a given domain). In this paper we introduce the concept of hierarchical FSCs for planning by allowing controllers to call other controllers. This call mechanism allows hierarchical FSCs to represent generalized plans more compactly than individual FSCs, to compute controllers in a modular fashion or even more, to compute recursive controllers. The paper introduces a classical planning compilation for computing hierarchical FSCs that solve challenging generalized planning tasks. The compilation takes as input a finite set of classical planning problems from a given domain. The output of the compilation is a single classical planning problem whose solution induces: (1) a hierarchical FSC and (2), the corresponding validation of that controller on the input classical planning problems.



有限状態コントローラ(FSC)は、シーケンシャルプランをコンパクトに表現する効果的な方法です。遷移に適切な条件を課すことで、FSCは一般化プラン(特定のドメインにおける様々な計画問題を解くプラン)も表現できます。本稿では、コントローラが他のコントローラを呼び出すことを可能にする、計画のための階層型FSCの概念を紹介します。この呼び出しメカニズムにより、階層型FSCは個々のFSCよりもコンパクトに一般化プランを表現し、コントローラをモジュール形式で計算したり、さらには再帰的なコントローラを計算したりすることができます。本稿では、困難な一般化プランニングタスクを解決する階層型FSCを計算するための、古典的なプランニングコンパイルを紹介します。このコンパイルは、特定のドメインにおける古典的なプランニング問題の有限集合を入力として受け取ります。コンパイルの出力は単一の古典的計画問題であり、その解は(1)階層的FSCと(2)入力された古典的計画問題に対するその制御器の対応する検証を誘導します。

A Review of Inference Algorithms for Hybrid Bayesian Networks

A Review of Inference Algorithms for Hybrid Bayesian Networks / ハイブリッドベイジアンネットワークの推論アルゴリズムのレビュー

Hybrid Bayesian networks have received an increasing attention during the last years. The difference with respect to standard Bayesian networks is that they can host discrete and continuous variables simultaneously, which extends the applicability of the Bayesian network framework in general. However, this extra feature also comes at a cost: inference in these types of models is computationally more challenging and the underlying models and updating procedures may not even support closed-form solutions. In this paper we provide an overview of the main trends and principled approaches for performing inference in hybrid Bayesian networks. The methods covered in the paper are organized and discussed according to their methodological basis. We consider how the methods have been extended and adapted to also include (hybrid) dynamic Bayesian networks, and we end with an overview of established software systems supporting inference in these types of models.



ハイブリッドベイジアンネットワークは、ここ数年でますます注目を集めています。標準的なベイジアンネットワークとの違いは、離散変数と連続変数を同時に扱えることで、ベイジアンネットワークフレームワークの適用範囲が広くなります。しかし、この追加機能には代償もあります。この種のモデルにおける推論は計算上より困難であり、基盤となるモデルや更新手順が閉形式の解をサポートしていない場合もあります。本稿では、ハイブリッドベイジアンネットワークにおける推論実行の主な動向と原理的なアプローチの概要を示します。本稿で扱う手法は、その方法論的根拠に基づいて整理・考察されています。これらの手法がどのように拡張・適応され、(ハイブリッド)動的ベイジアンネットワークも含まれるようになったかを考察し、最後にこの種のモデルにおける推論をサポートする確立されたソフトウェアシステムの概要を示します。

Querying Log Data with Metric Temporal Logic

Querying Log Data with Metric Temporal Logic / 計量時相論理を用いたログデータのクエリ

We propose a novel framework for ontology-based access to temporal log data using a datalog extension datalogMTL of the Horn fragment of the metric temporal logic MTL. We show that datalogMTL is EXPSPACE-complete even with punctual intervals, in which case full MTL is known to be undecidable. We also prove that nonrecursive datalogMTL is PSPACE-complete for combined complexity and in AC0 for data complexity. We demonstrate by two real-world use cases that nonrecursive datalogMTL programs can express complex temporal concepts from typical user queries and thereby facilitate access to temporal log data. Our experiments with Siemens turbine data and MesoWest weather data show that datalogMTL ontology-mediated queries are efficient and scale on large datasets.



計量時相論理MTLのホーンフラグメントのデータログ拡張datalogMTLを用いて、時相ログデータへのオントロジーベースのアクセスのための新しいフレームワークを提案します。datalogMTLは、完全なMTLが決定不能となることが知られている点において、点間隔を含む場合でもEXPSPACE完全であることを示す。また、非再帰datalogMTLは、複合複雑性に関してPSPACE完全であり、データ複雑性に関してAC0であることも証明します。2つの実際の使用例を用いて、非再帰datalogMTLプログラムが典型的なユーザークエリから複雑な時間概念を表現し、それによって時相ログデータへのアクセスを容易にできることを実証します。SiemensタービンデータとMesoWest気象データを用いた実験により、datalogMTLオントロジーを介したクエリは効率的で、大規模なデータセットでも拡張可能であることが示されました。

参考文献

関連情報