Metric Temporal Equilibrium Logic over Timed Traces

要約

線形時間に基づくアンサーセット・プログラミング(ASP)の時間的拡張では、動的システムの動作は状態のシーケンスによって表現される。この表現は相対的な順序を反映する一方で、各状態に関連する特定の時間を抽象化する。しかし、タイミング制約は、例えば、計画とスケジューリングが両立するような多くのアプリケーションにおいて重要である。我々は、線形時間時間均衡論理のメトリック拡張を開発することで、この問題に対処する。結果として得られるメトリック均衡論理は、定性的・定量的な動的制約を指定するためのASPベースのアプローチの基礎を提供する。この目的のために、我々はメトリック式のモナド一階式への変換を定義し、それぞれメトリック均衡論理とモナド量化均衡論理におけるモデル間の対応を与える。興味深いことに、我々の翻訳は、ASPモジュロ差制約の観点からの実装のためのブループリントを提供する。

要約(オリジナル)

In temporal extensions of Answer Set Programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. However, timing constraints are important in many applications like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium Logic and Monadic Quantified Equilibrium Logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL