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. Existing logical frameworks such as linear temporal logic are too restrictive to express temporal and sequential properties in biomedicine, or too permissive in semantic constructs, such as in Halpern-Shoham logic, to serve this purpose. 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 include initial results on expressiveness and decidability fragments for ${\rm TEL}_{\mathbb{N}^+}$, followed by application outlook and discussions.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google