Temporal Ensemble Logic

要約

線形時間時相推論のためのモナディック 1 次様相論理である Temporal Ensemble Logic (TEL) を紹介します。
TEL には、「常に $t$ 時間後まで」($\Box_t$)、「将来の $t$ 時間前に時々」($\Diamond_t$)、「$」などの原始的な時間構造が含まれています。
t$-時間後” $\varphi_t$.
TEL は、生物医学における時間的推論を形式化する際のギャップを埋めるために、臨床および集団健康研究におけるコホートの特定と発見のための厳密性と再現性の要件を動機としてきました。
この論文では、まず一般的な設定での TEL を紹介し、特殊な場合として離散時間と密集時間を使用します。
次に、正の整数 $\mathbb{N}^+$ の時間領域における離散 TEL の理論的発展に焦点を当てます。${\rm TEL}_{\mathbb{N}^+}$ として示されます。
${\rm TEL}_{\mathbb{N}^+}$ は、B\'{u}chi オートマトンによって特徴付けられる、標準的なモナド 2 次ロジックよりも厳密には表現力が高くなります。
我々はその形式的意味論、証明システムを提示し、${\rm TEL}_{\mathbb{N}^+}$ の充足可能性の決定不可能性の証明を提供します。
また、${\rm TEL}_{\mathbb{N}^+}$ の表現力と決定可能性の断片についても説明し、続いて応用例についても説明します。

要約(オリジナル)

We introduce Temporal Ensemble Logic (TEL), a monadic, first-order modal logic for linear-time temporal reasoning. TEL includes primitive temporal constructs such as “always up to $t$ time later” ($\Box_t$), “sometimes before $t$ time in the future” ($\Diamond_t$), and “$t$-time later” $\varphi_t$. TEL has been motivated from the requirement for rigor and reproducibility for cohort specification and discovery in clinical and population health research, to fill a gap in formalizing temporal reasoning in biomedicine. In this paper, we first introduce TEL in a general set up, with discrete and dense time as special cases. We then focus on the theoretical development of discrete TEL on the temporal domain of positive integers $\mathbb{N}^+$, denoted as ${\rm TEL}_{\mathbb{N}^+}$. ${\rm TEL}_{\mathbb{N}^+}$ is strictly more expressive than the standard monadic second order logic, characterized by B\'{u}chi automata. We present its formal semantics, a proof system, and provide a proof for the undecidability of the satisfiability of ${\rm TEL}_{\mathbb{N}^+}$. We also discuss expressiveness and decidability fragments for ${\rm TEL}_{\mathbb{N}^+}$, followed by illustrative applications.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google