Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials

In modeling clinical trials, we consider the time domain of positive integers ${\mathbb{N}}^{+}$, which represent days lapsed from the start of a clinical trial.

The basic construct of TEL [48] includes two types of terms: integer terms over ${\mathbb{N}}^{+}$, and logical formulas. Integer terms $s,t,u,v,\mathrm{\dots }$ consist of constants $a,b,c,\mathrm{\dots }$, variables $x,y,z,\mathrm{\dots }$ (from a set Var), and the addition of these terms $(s+t)$. We write $\mathrm{𝖳𝖾𝗋𝗆}$ for the set of all such integer terms. Logical formulas $\phi$ consist of primitive propositions $p$, indexed formulas ${\phi }_t$, Boolean connectors ($\wedge$, $\neg$), time-indexed modalities ${\mathrm{\square }}_t\phi$ and ${\mathrm{◇}}_t\phi$, and first-order quantification over variables in Var.

In Backus–Naur form (BNF) notation, we have $s,t::=a\mid x\mid (s+t),$ where $a$ is an integer constant, $x\in \mathrm{𝖵𝖺𝗋}$, and $(s+t)$ represent the addition of two integer terms.

For TEL formula, we have, with $t$ for integer term and $x$ for variable over ${\mathbb{N}}^{+}$:

Atomic propositions $p$ come from a pre-defined set $\mathrm{𝖯𝗋𝗈𝗉}$, a set of clinical codes and ontological terms according to the conceptual correspondence provided in Table 1.

To specify the semantics of the above formulas, we define an interpretation as a function $\alpha :{\mathbb{N}}^{+}\to 2^{\mathrm{𝖯𝗋𝗈𝗉}}$, which determines, at each time-point $i\in {\mathbb{N}}^{+}$, a subset of atomic propositions that are assigned true. We can use the notation of formal languages to describe such interpretations. The alphabet is $\mathrm{\Sigma }$ (= $2^{\mathrm{𝖯𝗋𝗈𝗉}}$), to account for all possible truth-status of each proposition in Prop at a given time. Following standard formal language convention, ${\mathrm{\Sigma }}^{\ast }$ represents the set of all finite words over $\mathrm{\Sigma }$, ${\mathrm{\Sigma }}^{+}$ represents the set of all no-empty finite words over $\mathrm{\Sigma }$, and ${\mathrm{\Sigma }}^{\omega }$ represents all $\omega$-words over $\mathrm{\Sigma }$. Therefore, we can write $\alpha$ in the form of an $\omega$-word $\sigma [1]\sigma [2]\mathrm{\cdots }$, with $\sigma [i]\in \mathrm{\Sigma }$ being the $i$th letter of $\alpha$ for all $i\ge 1$.

Clinical trials involve complex temporal dependencies between interventions, patient responses, and outcomes, requiring a formal approach to temporal reasoning. Existing logical frameworks in computer science and biomedicine either lack expressiveness for capturing trial dynamics or impose syntactic constraints that limit their applicability to real-world trial scenarios.

To make the technical motivations and design decisions more intuitive, we begin with an illustrative example. This example is intended to highlight the practical needs and conceptual foundations for combining first-order and modal logic primitives in the representation of biological phenotypes. By grounding the discussion in concrete use cases, we aim to clarify the expressive requirements that drive our modeling strategy.

Many existing temporal logics have been developed to express different types of temporal relationships, each with its own strengths and trade-offs. LTL [33] captures linear sequences of states to express event orders. Based on LTL, Metric Temporal Logic (MTL) [29] adds explicit timing bounds to temporal operators. Interval Temporal Logic (ITL) [9, 14] focuses on intervals rather than points, capturing relationships. Despite the extensive development of temporal logic frameworks, their practical application in clinical trial specification remains limited. Giordano et al. modeled stroke guidelines as concurrent processes in LTL and verified them with SPIN [13], while Sanati et al. introduced a MTL-based Description Logics for formulating eligibility criteria for clinical trials [2]. Shankar et al. [39] developed a formal ontology to encode temporal constraints in clinical trials, allowing precise specification of timeline requirements (e.g., “lab test 2 must occur within 7 days after dose 1”) using ITL. CNTRO [42, 43] encodes logical and temporal constraints directly within the structure of the Web Ontology Language (OWL). The Time Event Ontology (TEO) proposed by Li et al. [21] extends CNTRO by harmonizing Allen’s interval algebra with a suite of basic time relations, although it lacks a language of logic for modeling trials.

LTL can express sequential temporal dependencies and comes with mature automated tools, but it has limited expressiveness. It cannot capture complex interval constraints such as “observe within a specified time window”. MTL can express time-bounded constraints such as visit windows or dosing intervals, but cannot directly relate distinct times or intervals. It lacks the ability to express dependencies such as “dose two administered exactly 14 days after dose one, followed by a visit 7 days later.” ITL can model observation windows and treatments with interval-based semantics (e.g., “treatment continues during observation window”) but it becomes overly complex and lacks cross-timeline reference capability without additional constructs. Table 2 summarizes these observations.

The use of TEL for trial modeling brings the following advantages. TEL has already been demonstrated as a natural but minimalistic logical framework with potential as an attractive approach to formalizing phenotypes in biomedicine [48]. Using the model-checking paradigm, TEL can support both point-based and interval-based temporal constructs. TEL is highly expressive in modeling temporal properties, but restricted in aspects not essential to targeted applications. The scope of first-order quantifiers for TEL is limited to unary predicates derived from an existing formula, rather than over independently given predicates. As can be seen in subsequent developments, the specific fragment of TEL used for this study does not involve the $\forall$ quantifier. Although it is beyond the scope of the current paper to address theoretical developments in decidability and algorithmic complexity results for specific fragments of TEL (given its general undecidability [48]), our experimental results show practical feasibility in reasonable settings.

The Self-Controlled Case Series (SCCS) method is a widely used design for evaluating the association between medical interventions and adverse events. By treating individuals as their own controls, SCCS effectively mitigates confounding from fixed patient-level characteristics such as genetics and lifestyle [46]. In this simulation-based framework, longitudinal health records are used to construct individual timelines of intervention exposure and subsequent adverse events. A predefined risk window is specified following the intervention, and the frequency of events during this period is compared to baseline periods within the same individual using statistical modeling.

For example, a recent study investigating thrombosis risk after COVID-19 vaccination applied SCCS by extracting temporal sequences of vaccination dates and thrombotic events from electronic health records [17]. By comparing the incidence of events before and after vaccination within each individual, the study reduced between-subject variability and provided robust evidence of causal relationships.

Patient recruitment is a persistent bottleneck in clinical trial implementation. Eligibility Cohort Building Simulations offer a data-driven strategy to improve recruitment efficiency by leveraging EHR data to model real-world patient populations [36]. In this approach, researchers first define trial eligibility criteria such as age range, treatment history, and comorbidities, and apply them to EHR datasets to construct a virtual cohort. Computational models estimate the number of patients who meet the criteria and allow iterative refinement by adjusting thresholds or conditions to assess their impact on cohort size and diversity [20]. This simulation process enables the design of recruitment strategies that are both scientifically rigorous and operationally feasible.

For example, a Phase III clinical trial investigating a novel therapeutic for hormone receptor-positive breast cancer used this method to address recruitment delays. By simulating eligibility criteria including age between 30 and 75 years, prior chemotherapy, and absence of major cardiovascular conditions on a real-world breast cancer dataset, investigators identified constraints that limited enrollment. Adjusting these parameters, such as slightly expanding the age range, helped increase the candidate pool while preserving trial integrity [26].

The Individual Timeline-Based CTS captures the temporal dynamics of clinical events at the patient level, supporting analyses of time-dependent phenomena such as treatment onset and disease progression. While effective for intra-individual variability and temporal causality, it is less suited for between-group comparisons. In contrast, the Cohort-Based CTS organizes participants into predefined groups based on treatment or baseline characteristics, simulating longitudinal outcomes to assess efficacy, safety, event incidence, and dropout rates. This structure, aligned with parallel-arm trial designs, aids trial feasibility, sample size estimation, and recruitment planning. Cohorts are defined by Base Criteria (shared attributes), Case Criteria (presence of key exposures), and Control Criteria (absence of exposures), enabling robust comparative analyses and accounting for real-world complexities such as time-to-event variability, adherence, and attrition.

This section formalizes a timeline-based CTS using the TEL framework. The model is anchored by a start event (S) and an index event (I), such as a diagnosis or lab finding, which serves as the temporal reference for aligning all other trial components. Between these events lies the observation window (W), used to assess baseline covariates and eligibility status. Eligibility criteria (E) may span both pre- and post-index periods. The baseline visit (B) captures pre-intervention assessments. The intervention phase (T) begins after the index event, followed by post-treatment follow-up visits (F) to monitor outcomes and safety. Outcome assessment (O) occurs within a bounded period at the end of the trial. TEL constraints are defined with modal operators to precisely capture temporal relationships.

• $\mathrm{■}$

  Start Event: The TEL expression for the start event occurring at time $x$ is: $\exists x\left(S_x\right)$.

• $\mathrm{■}$

  Index Event: The TEL expression for the index event occurring at time $x+i$ is given by: $\exists x\exists i\left(S_x\wedge I_{x+i}\right)$. The $x+i$ subscript ensures that Index event can occur only after the Start Event. This represents the key modeling strategy of using distinct terms to represent time dependencies, rather than using explicit comparison such as in other approaches.

• $\mathrm{■}$

  Observation Window: The observation window defines the time interval between the start event and the index event, within which prior clinical events must occur.The corresponding TEL expression is given by: $\exists x\exists i\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{◇}}_{i}W\right)}_x\right]$.

• $\mathrm{■}$

  Baseline Visit: The TEL expression for the baseline visit $B$ occurs within $b$ units after the index event is given by: $\exists x\exists i\exists b\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{◇}}_{i}W\right)}_x\wedge {\left({\mathrm{◇}}_{b}B\right)}_{x+i}\right]$.

• $\mathrm{■}$

  Intervention Phase: The TEL expression for the intervention phase $T$ occurring within $t$ units post-baseline is given by:

  $$\exists x\exists i\exists b\exists t\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{◇}}_{i}W\right)}_x\wedge {\left({\mathrm{◇}}_{b}B\right)}_{x+i}\wedge {\left({\mathrm{◇}}_{t}T\right)}_{x+i+b}\right].$$

• $\mathrm{■}$

  Follow-up visits: The TEL expression for the follow-up visit $F$ occurring within $f$ units after the intervention phase is given by:

  $$\exists x\exists i\exists b\exists t\exists f\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{◇}}_{i}W\right)}_x\wedge {\left({\mathrm{◇}}_{b}B\right)}_{x+i}\wedge {\left({\mathrm{◇}}_{t}T\right)}_{x+i+b}\wedge {\left({\mathrm{◇}}_{f}F\right)}_{x+i+b+t}\right].$$

• $\mathrm{■}$

  Outcome Assessment: The TEL expression for the outcome assessment $O$ occurring within $o$ units after the follow-up visit is given by:

  $$\exists x\exists i\exists b\exists t\exists f\exists o\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{◇}}_{i}W\right)}_x\wedge {\left({\mathrm{◇}}_{b}B\right)}_{x+i}\wedge {\left({\mathrm{◇}}_{t}T\right)}_{x+i+b}\wedge {\left({\mathrm{◇}}_{f}F\right)}_{x+i+b+t}\wedge {\left({\mathrm{◇}}_{o}O\right)}_{x+i+b+t+f}\right].$$

• $\mathrm{■}$

  Eligibility Criteria: Eligibility Criteria define the conditions under which a participant is deemed suitable for enrollment in the clinical trial.

  • –

    Inclusion Criteria (IC): which specify characteristics that must be present for a participant to qualify. The TEL expression is given by:

    $$\exists x\exists i\exists c_1\exists c_2\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{◇}}_{c_1}IC\right)}_x\vee {\left({\mathrm{◇}}_{c_2}IC\right)}_{x+i}\right].$$

  • –

    Exclusion Criteria (EX), which specify conditions that, if present, disqualify a participant from participation. The TEL expression is given by:

    $$\exists x\exists i\exists e_1\exists e_2\left[S_x\wedge I_{x+i}\wedge {\left({\mathrm{\square }}_{e_1}\neg EX\right)}_x\wedge {\left({\mathrm{\square }}_{e_2}\neg EX\right)}_{x+i}\right].$$

The full TEL expression representing the clinical trial structure temporally anchored on the start event and index event, and encoding the logical and temporal constraints across eligibility, baseline, treatment, follow-up, and outcome phases, is defined as follows:

The Cohort-Based CTS models trial participants as belonging to logically distinct subpopulations, defined through a combination of base eligibility and group-specific cohort criteria. Each individual in the simulation is first evaluated against the Base Criteria to determine inclusion in the eligible study population. Then, individuals are assigned to mutually exclusive groups according to whether they satisfy the Case Criteria or Control Criteria.

• $\mathrm{■}$

  Base Criteria: All individuals must meet the base criteria within a defined observation window starting at the reference time $t_0$. These criteria typically include basic demographic filters, the length of the observation period, and the exclusion of confounders. The TEL expression is: $\exists t_0\left(Bas{e}_{t_0}\right)$.

• $\mathrm{■}$

  Case Criteria: Individuals who meet the case criteria are assigned to the case cohort. These criteria usually capture exposure to an intervention, diagnosis of a condition, or other qualifying events. The case criteria must be met after satisfying the base criteria. The TEL expression is: $\exists t_0\exists t_1\left[Bas{e}_{t_0}\wedge {\left({\mathrm{◇}}_{t_1}\text{Case}\right)}_{t_0}\right]$.

• $\mathrm{■}$

  Control Criteria: Individuals who meet the control criteria are assigned to the control cohort. These criteria typically indicate the absence of the exposure or condition that defines the case group. The assignment of control also follows the base criterion. The TEL expression is: $\exists t_0\exists t_2\left[Bas{e}_{t_0}\wedge {\left({\mathrm{◇}}_{t_2}\text{Control}\right)}_{t_0}\right]$.

Formally, the model-checking [6, 45] process seeks to determine whether a patient record $\alpha$ satisfies a given clinical trial specification $\phi$, as defined in TEL. That is, we aim to verify whether there exists a time point $i\ge 1$ such that $(\alpha ,i)\vDash \phi$, under the TEL semantics. This generalizes beyond traditional initial-time evaluation by enabling satisfaction to be checked at any point along a patient’s longitudinal record, allowing for alignment of protocol logic with varying index events. The language defined by a TEL formula, denoted $ℒ(\phi )$, consists of all $\omega$-words (i.e., patient records) that satisfy the formula at some valid time index. This capability supports temporal abstraction and flexible anchoring of eligibility and trial components in real-world datasets. TEL-based model-checking provides a scalable and precise method for aligning structured clinical data with complex temporal protocol logic, improving the interpretability, consistency, and reproducibility of virtual clinical trials.

We developed the AD Clinical Trial Ontology (ADCTO) to represent key elements frequently encountered in the eligibility criteria of Alzheimer’s disease (AD) clinical trials, using data from ClinicalTrials.gov. The ontology encompasses a comprehensive range of categories, including Disease, Medication, Diagnostic Test, Procedure, Rating Criteria, Social Determinants of Health, and Fertility. Each concept was mapped to the Unified Medical Language System (UMLS) with assigned Concept Unique Identifiers (CUIs) and annotated with Observational Health Data Sciences and Informatics (OHDSI) Athena identifiers. We enriched ADCTO with annotations from resources such as the National Library of Medicine (NLM) Value Set Authority Center, the National Drug Code (NDC) directory, UMLS Terminology Services, Codify by the American Academy of Professional Coders (AAPC), and the Phenotype KnowledgeBase (PheKB). To construct a coherent hierarchy, we integrated established biomedical ontologies and classification systems, including the Disease Ontology for disease concepts and DrugBank and the Anatomical Therapeutic Chemical (ATC) classification system for medications, with refinements informed by domain experts to ensure semantic precision and relevance.

Compared to existing ontologies, ADCTO maintains a lightweight structure, with 274 classes, 278 logical axioms, and 284 declaration axioms. To evaluate its adequacy, we achieved a recall of 0.63 (the proportion of ontology-mapped elements relative to all extracted eligibility elements) and an average term frequency–inverse document frequency (TF-IDF) score of 3.91, indicating ADCTO’s effectiveness in capturing the essential elements of AD eligibility criteria in a compact and computationally efficient structure.

We developed the AD Clinical Trial Simulation System, a logic-based platform for designing and evaluating virtual clinical trials using real-world data. Built on the ADCTO, the system provides a formally defined and semantically consistent vocabulary to represent key trial components, including event types, eligibility criteria, interventions, outcomes, and their temporal dependencies. Users interact with a web-based interface that offers ontology-aligned dropdown menus, enabling the configuration of trial components without the need for manual coding. These selections are automatically compiled into formal representations, allowing for precise and interpretable modeling of trial logic. The simulation engine leverages TEL to capture and enforce time-dependent relationships among clinical events. All components are temporally anchored to a defined index event, enabling precise sequencing of trial activities. The system supports fixed and flexible timelines and allows retrospective simulations using observational data. It is designed to bridge the gap between descriptions of natural language protocols and formal computational models. The user interface reflects the core vision of the system, which is to democratize formal trial design by making logical and ontological structures accessible to clinical researchers without requiring expertise in logic or programming.

Figure 1 illustrates the user interface of our system. Figure 1.(a).A shows the components of a clinical trial and allows users to click on each element to begin configuring it. Figure 1.(a).B showcases the trial builder, with subpanels B.1 and B.2 displaying interfaces for entering trial information and configuring timeline parameters. Figure 1(b) illustrates the configuration interface for specifying Inclusion Criteria, which serves as a representative example; similar interfaces are employed across other trial components to ensure consistency and usability. Figure 1.(b).C presents the ontology navigation interface, enabling users to explore standardized ADCTO terms. Figure 1.(b).D and E highlight the specification of temporal constraints and eligibility criteria, with E.1 featuring a dropdown menu populated by ontology-aligned terms. Finally, Figure 1.(b).F depicts the trial management interface, where users can review and save configured trials. Configured trials are automatically translated into formal TEL expressions and executed against real-world EHR datasets to simulate trial behavior and validate protocol feasibility. This enables researchers to assess cohort sizes, timing constraints, and outcome trajectories in silico. The system was implemented using Ruby on Rails [15] with a Model-View-Controller (MVC) architecture and used MongoDB [3] as the backend database to support scalable, document-based storage of evolving trial representations and large-scale simulations.

The interface serves as an authoring tool and compilation engine, generating formal TEL models from high-level trial designs. Each session outputs a reusable TEL expression anchored by start and index events, enriched with modal and quantified constraints. These specifications support downstream tasks such as simulation, model-checking, and validation against EHR or registry data. The platform enforces an ontology-driven workflow that enhances semantic clarity, reduces variability, and promotes reuse across studies. Aligned with standardized vocabularies, it enables integration with external data models and supports automated reasoning. Designed for longitudinal datasets, the system facilitates rapid prototyping, cohort selection, and eligibility screening. Each simulation is saved as a machine-readable specification that adheres to FAIR (Findable, Accessible, Interoperable, Reusable) data principles, supporting reproducibility, version control, and collaboration across institutions.