Completeness and Decidability of a Fragment of Duration Calculus with Iteration. - Dang Van Hung; Dimitar P. Guelev (ASIAN, 1999)

A Propositional Dynamic Logic with Qualitative Probabilities. - Dimitar P. Guelev (J. Philos. Log., 1999)

A Complete Fragment of Higher-Order Duration µ-Calculus. - Dimitar P. Guelev (FSTTCS, 2000)

Probabilistic Neighbourhood Logic. - Dimitar P. Guelev (FTRTFT, 2000)

Interval-Related Interpolation in Interval Temporal Logics. - Dimitar P. Guelev (Log. J. IGPL, 2001)

Prefix and Projection onto State in Duration Calculus. - Dimitar P. Guelev; Dang Van Hung (Theory and Practice of Timed Systems @ ETAPS, 2002)

Feature Integration as Substitution. - Dimitar P. Guelev; Mark Dermot Ryan; Pierre-Yves Schobbens (FIW, 2003)

Synthesising verified access control systems in XACML. - Nan Zhang 003; Mark Ryan 001; Dimitar P. Guelev (FMSE, 2004)

Model-Checking Access Control Policies. - Dimitar P. Guelev; Mark Ryan 001; Pierre-Yves Schobbens (ISC, 2004)

Sharpening the Incompleteness of the Duration Calculus. - Dimitar P. Guelev (ARTS, 2004)

Logical Interpolation and Projection onto State in the Duration Calculus. - Dimitar P. Guelev (J. Appl. Non Class. Logics, 2004)

A Relatively Complete Axiomatisation of Projection onto State in the Duration Calculus. - Dimitar P. Guelev; Dang Van Hung (J. Appl. Non Class. Logics, 2004)

A Complete Proof System for First-order Interval Temporal Logic with Projection. - Dimitar P. Guelev (J. Log. Comput., 2004)

Evaluating Access Control Policies Through Model Checking. - Nan Zhang 003; Mark Ryan 001; Dimitar P. Guelev (ISC, 2005)

Synthesising Features by Games. - Dimitar P. Guelev; Mark Dermot Ryan; Pierre-Yves Schobbens (AVoCS, 2005)

On the completeness and decidability of duration calculus with iteration. - Dimitar P. Guelev; Dang Van Hung (Theor. Comput. Sci., 2005)

Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems. - Dimitar P. Guelev (Log. Methods Comput. Sci., 2007)

Model-checking the preservation of temporal properties upon feature integration. - Dimitar P. Guelev; Mark Dermot Ryan; Pierre-Yves Schobbens (Int. J. Softw. Tools Technol. Transf., 2007)

Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions. - Dimitar P. Guelev; Catalin Dima (DALT, 2008)

Reasoning about QoS Contracts in the Probabilistic Duration Calculus. - Dimitar P. Guelev; Dang Van Hung (FESCA@ETAPS, 2008)

Synthesising verified access control systems through model checking. - Nan Zhang 003; Mark Ryan 001; Dimitar P. Guelev (J. Comput. Secur., 2008)

A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic. - Dimitar P. Guelev (J. Log. Comput., 2008)

Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions - Catalin Dima; Constantin Enea; Dimitar P. Guelev (GANDALF, 2010)

An Epistemic Predicate CTL* for Finite Control π-Processes. - Dimitar P. Guelev; Mads Dam (M4M/LAMAS, 2011)

An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. - Dimitar P. Guelev; Catalin Dima; Constantin Enea (J. Appl. Non Class. Logics, 2011)

Epistemic ATL with Perfect Recall, Past and Strategy Contexts. - Dimitar P. Guelev; Catalin Dima (CLIMA, 2012)

An Assume/Guarantee Based Compositional Calculus for Hybrid CSP. - Shuling Wang 003; Naijun Zhan; Dimitar P. Guelev (TAMC, 2012)

Super-Dense Computation in Verification of Hybrid CSP Processes. - Dimitar P. Guelev; Shuling Wang 003; Naijun Zhan; Chaochen Zhou (FACS, 2013)

Reducing Validity in Epistemic ATL to Validity in Epistemic CTL - Dimitar P. Guelev (SR, 2013)

Guest editors' preface to special issue on interval temporal logics. - Ben C. Moszkowski; Dimitar P. Guelev; Martin Leucker (Ann. Math. Artif. Intell., 2014)

Refining and Delegating Strategic Ability in ATL. - Dimitar P. Guelev (SR, 2014)

Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. - Dimitar P. Guelev; Shuling Wang 003; Naijun Zhan (SETTA, 2017)

An application of temporal projection to interleaving concurrency. - Ben C. Moszkowski; Dimitar P. Guelev (Formal Aspects Comput., 2017)

Refining strategic ability in alternating-time temporal logic. - Dimitar P. Guelev (Inf. Comput., 2017)

Reasoning about Temporary Coalitions and LTL-definable Ordered Objectives in Infinite Concurrent Multiplayer Games. - Dimitar P. Guelev (CoRR, 2020)

Gabbay Separation for the Duration Calculus. - Dimitar P. Guelev (TIME, 2022)

A separation theorem for discrete-time interval temporal logic. - Dimitar P. Guelev; Ben C. Moszkowski (J. Appl. Non Class. Logics, 2022)

Of Temporary Coalitions in Terms of Concurrent Game Models, Announcements, and Temporal Projection. - Dimitar P. Guelev (LORI, 2023)

A Generalized Hybrid Hoare Logic. - Naijun Zhan; Bohua Zhan; Shuling Wang 003; Dimitar P. Guelev; Xiangyu Jin (CoRR, 2023)

Expressive completeness by separation for discrete time interval temporal logic with expanding modalities. - Dimitar P. Guelev; Ben C. Moszkowski (Inf. Process. Lett., 2024)

On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts. - Dimitar P. Guelev (CoRR, 2025)