Authors: Guo-Qiang Zhang
Abstract: 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.
Source: http://arxiv.org/abs/2408.14443v1
