Search Results

Documents authored by Zhang, Guo-Qiang

Document
DOI: 10.4230/OASIcs.TIME.2026.4
Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization

Authors: Manfred Droste and Guo-Qiang Zhang

Published in: OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)

Abstract
We study the discrete point-based fragment of Ensemble Logic EL(ℕ) over the natural numbers, a logic combining displacement φ_u, term-dependent metric modalities ☐_t and ♢_t with respect to an additive term t, Boolean connectives, and first-order quantification over ℕ. Motivated by the need for a unified symbolic representation of biomedical knowledge with temporal, spatial, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of EL(ℕ) (over a finite proposition set 𝒫) into first-order monadic Presburger arithmetic FO(ℕ,<,+;𝒫). This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter Turing machines with recurring control states proves that satisfiability is Σ¹₁-complete and validity is dually Π¹₁-complete. Expressively, EL(ℕ) strictly extends the star-free ω-languages and is incomparable with the ω-regular languages: it defines the non-ω-regular counting language {a^m b^m c^m d^m∣ m ≥ 1}⋅Σ^ω, whereas a delimited parity language remains outside the logic by a quantifier-bounding argument combined with classical circuit lower bounds for parity. On the proof-theoretic side, we present a sound Hilbert system ℋ_EL and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible. We also prove that the existential fragment ∃EL(ℕ) has NP-complete satisfiability and coNP-complete unsatisfiability. Finally, we show that finite active-domain model-checking has PTIME data complexity and PSPACE-complete combined complexity. Together, these results give a precise decidability, expressiveness, proof-theoretic, and model-checking baseline for subsequent algorithmic applications of Ensemble Logic in biomedicine. This work is a part of the Symbolic Biomedicine program championed by the corresponding author.
Cite as

Manfred Droste and Guo-Qiang Zhang. Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{droste_et_al:OASIcs.TIME.2026.4,
  author =	{Droste, Manfred and Zhang, Guo-Qiang},
  title =	{{Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization}},
  booktitle =	{33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
  pages =	{4:1--4:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-448-2},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{146},
  editor =	{Orlandini, AndreA and Pinchinat, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.4},
  URN =		{urn:nbn:de:0030-drops-277009},
  doi =		{10.4230/OASIcs.TIME.2026.4},
  annote =	{Keywords: Temporal logic, monadic Presburger arithmetic, descriptive complexity, electronic health records}
}
Document
DOI: 10.4230/LIPIcs.TIME.2025.13
Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials

Authors: Xiaojin Li, Yan Huang, Rashmie Abeysinghe, Zenan Sun, Hongyu Chen, Pengze Li, Xing He, Shiqiang Tao, Cui Tao, Jiang Bian, Licong Cui, and Guo-Qiang Zhang

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract
Clinical trials are typically specified with protocols that define eligibility criteria, treatment regimens, follow-up schedules, and outcome assessments. Temporality is a hallmark of all clinical trials, reflected within and across trial components, with complex dependencies unfolding across multiple time points. Despite their importance, clinical trial protocols are described in free-text format, limiting their semantic precision and the ability to support automated reasoning, leverage data across studies and sites, or simulate trial execution under varying assumptions using Real-World Data. This paper introduces a formalized representation of clinical trials using Temporal Ensemble Logic (TEL). TEL incorporates metricized modal operators, such as "always until t" (□_t) and "possibly until t" (◇_t), where t is a time-length parameter, to offer a logical framework for capturing phenotypes in biomedicine. TEL is more expressive in syntax than classical linear temporal logic (LTL) while maintaining the simplicity of semantic structures. The attributes of TEL are exploited in this paper to formally represent not only individual clinical trial components, but also the timing and sequential dependencies of these components as a whole. Modeling strategies and demonstration case studies are provided to show that TEL can represent the entirety of clinical trials, whereby providing a formal logical framework that can be used to represent the intricate temporal dependencies in trial structure specification. Since clinical trials are a cornerstone of evidence-based medicine, serving as the scientific basis for evaluating the safety, efficacy, and comparative effectiveness of therapeutic interventions, results reported here can serve as a stepping stone that leads to scalable, consistent, and reproducible representation and simulation of clinical trials across all disease domains.
Cite as

Xiaojin Li, Yan Huang, Rashmie Abeysinghe, Zenan Sun, Hongyu Chen, Pengze Li, Xing He, Shiqiang Tao, Cui Tao, Jiang Bian, Licong Cui, and Guo-Qiang Zhang. Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.TIME.2025.13,
  author =	{Li, Xiaojin and Huang, Yan and Abeysinghe, Rashmie and Sun, Zenan and Chen, Hongyu and Li, Pengze and He, Xing and Tao, Shiqiang and Tao, Cui and Bian, Jiang and Cui, Licong and Zhang, Guo-Qiang},
  title =	{{Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.13},
  URN =		{urn:nbn:de:0030-drops-244595},
  doi =		{10.4230/LIPIcs.TIME.2025.13},
  annote =	{Keywords: Temporal ensemble logic, Clinical trials, Logic-based modeling}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact