­Dimitar P. Guelev - publications


Journal papers

 Dimitar P. Guelev and Ben Moszkowski . A separation theorem for discrete-time interval temporal logic. Journal of Applied Non-Classical Logics, volume 32, issue 1, pp 28-54, 2022.

Ben Moszkowski  and Dimitar P. Guelev. An Application of Temporal Projection to Interleaving Concurrency. Formal Aspects of Computing, volume 29, issue 4, pp 705-750, 2017.

Dimitar P. Guelev. Refining Strategic Ability in ATL. Information and Computation. Special issue on selected papers from the 2nd Intl. Workshop on Strategic Reasoning (SR 2014), volume 254, pp. 316-328, 2017.

Ben Moszkowski, Dimitar P. Guelev and Martin Leucker. Guest Editor's Preface to Special Issue on Interval Temporal Logics. Annals of Mathematics and Artificial Intelligence, volume 71, issue 1-3, pp. 1-9, 2014.

Dimitar P. Guelev, Catalin Dima and Constantin Enea. An Alternating-time Temporal Logic with Knowledge, Perfect Recall and Past: Axiomatisation and Model Checking. Journal of Applied Non-classical Logic, volume 21, issue 1, pp. 93-131, 2011.

Dimitar P. Guelev. A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic. Journal of Logic and Computation, volume 18, issue 4, pp. 615-623, 2008.

Nan Zhang, Mark D. Ryan and Dimitar P. Guelev. Synthesising Verified Access Control Systems through Model Checking.  Journal of Computer Security, volume 16, issue 1, pp. 1-61, 2008.

Dimitar P. Guelev. Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems.  Logical Methods in Computer Science, volume 3, issue 3, 44 p., 2007.

Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Model-checking the Preservation of Temporal Properties upon Feature Integration. Software Tools for Technology Transfer, volume 9, issue 1, pp 53-62, 2007. A revised version of the paper presented at the CONCUR workshop Automated Verification of Critical Systems (AVoCS'04), London, September 2004.

Dimitar P. Guelev and Dang Van Hung. On the Completeness and Decidability of Duration Calculus with Iteration.
Theoretical Computer Science, volume 337, pp. 278-304, 2005.

Dimitar P. Guelev and Dang Van Hung. A Relatively Complete Axiomatisation of Projection onto State in the Duration Calculus. Journal of Applied Non-classical Logic, volume 14, issue 1-2, pp. 149-180, 2004.

Dimitar P. Guelev. Logical Interpolation and Projection onto State in the Duration Calculus. Journal of Applied Non-classical Logic, volume 14, issue 1-2, 2004, pp. 181-208. An extended abstract was presented at the Workshop on Interval Temporal Logics and Duration Calculi of ESSLLI 2003.

Dimitar P. Guelev. A Complete Proof System for First Order Interval Temporal Logic with Projection. Journal of Logic and Computation, volume 14, issue 2, pp. 215-249, 2004.

Dimitar P. Guelev. Interval-related Interpolation in Interval Temporal Logics. Logic Journal of the IGPL, volume 9 issue 5, 2001, pp. 677-685. Presented at ICTL 2000.

Dimitar P. Guelev. A Propositional Dynamic Logic with Qualitative Probabilities. Journal of Philosophical Logic, volume 28, number 6, 1999, pp. 575-605.

Conference and workshop papers

Dimitar P. Guelev. Of Temporary Coalitions in Terms of Concurrent Game Models, Announcements, and Temporal Projection  Proceedings of LORI 2023, LNCS 14329, Springer, pp. 126-134, 2023.

Dimitar P. Guelev. Gabbay Separation for the Duration Calculus Proceedings of TIME 2022, LIPICS Volume 247, Dagstuhl Publishing, pp. 10:1-10:14, 2022.

Dimitar P. Guelev. Reasoning about Temporary Coalitions and LTL-definable Ordered Objectives in Infinite Concurrent Multiplayer Games To be presented online at the 8th Intl. Workshop on Strategic Reasoning (SR 2020), September, 2020. Also available from arXiv 2011.03724 .

Dimitar P. Guelev,.Shuling Wang and Naijun Zhan. Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. Proceedings of SETTA 2017, LNCS 10606, Springer-Verlag, 2015, pp. 110-127.

Ben Moszkowski and Dimitar P. Guelev. An Application of Temporal Projection to Interleaving Concurrency. Proceedings of SETTA 2015, LNCS 9409, Springer-Verlag, 2015, pp. 153-167.

Dimitar P. Guelev, Shuling Wang, Naijun Zhan and Chaochen Zhou. Super-Dense Computation in Verification of Hybrid CSP Processes. Proceedings of FACS 2013, LNCS 8348, Springer-Verlag, 2014, pp. 13-22.

Dimitar P. Guelev. Refining and Delegating Strategic Ability in ATL. Presented and published in the Proceedings of the 2nd Intl. Workshop on Strategic Reasoning (SR 2014), EPTCS, volume 146, pp 57-64, 2014.

Dimitar P. Guelev. Reducing Validity in Epistemic ATL to Validity in Epistemic CTL. Presented and published in the Proceedings of the 1st Intl. Workshop on Strategic Reasoning (SR 2013), EPTCS, volume 112, pp 81-90, 2013.

Dimitar P. Guelev and Catalin DimaEpistemic ATL with Perfect Recall, Past and Strategy Contexts. Proceedings of CLIMA XIII, LNCS 7486, Springer-Verlag, 2012, pp. 77-93.

Wang Shuling, Zhan Naijun and Dimitar P. Guelev. An Assume/Guarantee Based Compositional Calculus for Hybrid CSP. Proceedings of TAMC 2012, LNCS 7287, Springer-Verlag, 2012, pp. 72-83.

Dimitar P. Guelev and Mads Dam. An Epistemic Predicate CTL* for Finite Control π-Processes. Presented and published in the Proceedings of the 7th Workshop on Methods for Modalities (M4M 2011) and the 4th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2011), Osuna, Spain, November 2011, Electronic Notes in Theoretical Computer Science, volume 278, pp. 229-243, 2011.

Catalin Dima, Constantin Enea, Dimitar Guelev and Ferucio Tiplea. Positive and negative results on the model-checking problem for ATL with imperfect information. Presented at the 2nd Workshop on Games for Design, Verification and Synthesis, Paris (France), September 4, 2010.

Catalin Dima, Constantin Enea and Dimitar Guelev. Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions. Presented and published in the Proceedings of the First Symposium on Games, Automata, Logic, and Formal Verification (GandALF 2010), Electronic Proceedings in Theoretical Computer Science (EPTCS) volume 25, pp 103-117, 2010.

Dimitar P. Guelev and Catalin Dima. Model-checking strategic ability and knowledge of the past of communicating coalitions. Presented at the AAMAS workshop Declarative Agent Languages and Technologies (DALT), 2008, LNAI 5397, Springer, 2008, pp. 75-90.

Dimitar P. Guelev and Dang Van Hung. Reasoning about QoS contracts in the Probabilistic Duration Calculus. Presented at the ETAPS workshop Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA), 2008. Electronic Notes in Theoretical Computer Science, volume 238, issue 6, pp. 41-62, 2010.

Nan Zhang, Mark Ryan and Dimitar P. Guelev, Evaluating Access Control Policies through Model-checking. Presented and published in the Proceedings of the 8th Information Security Conference (ISC'05), Singapore, September 2005, LNCS 3650, Springer, 2005, pp. 446-460.

Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Synthesising Features by Games. Presented at the fifth workshop Automated Verification of Critical Systems (AVoCS'05), Warwick University, UK, September 2005. Electronic Notes in Theoretical Computer Science, volume 145, pp. 79-93, 2006.

Nan Zhang, Mark Ryan and Dimitar P. Guelev, Synthesising Verified Access Control Systems in XACML. Proceedings of the 2nd ACM Workshop on Formal Methods in Security Engineering (FMSE 2004), Washingtion, DC, USA, October 29, 2004, ACM, pp. 56-65.

Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Model-checking the Preservation of Temporal Properties upon Feature Integration. Presented at the CONCUR workshop Automated Verification of Critical Systems (AVoCS'04), London, September 2004. Electronic Notes in Theoretical Computer Science, volume 128, issue 6, pp. 311-324, 2005. A revised version in Software Tools for Technology Transfer, volume 9, issue 1, pp 53-62, 2007.

Dimitar P. Guelev. Sharpening the Incompleteness of the Duration Calculus. Proceedings of the AMAST Workshop on Real-time Systems (ARTS), Stirling, UK, June 2004. Electronic Notes in Theoretical Computer Science, volume 139, issue 1, pp. 91-104, 2005.

Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Model-checking Access Control Policies. Presented at the LICS workshop Foundations of Computer Security (FCS'04), Turku, Finland, July 2004. Presented and published in the Proceedings of the 7th Information Security Conference (ISC'04), Palo Alto, California, September 2004, LNCS 3225, Springer, 2004, pp. 219-230.

Dimitar P. Guelev. Logical Interpolation and Projection onto State in the Duration Calculus (Extended Abstract). Workshop on Interval Temporal Logics and Duration Calculi, ESSLLI, Vienna, 2003. The full paper appeared in the Journal of Applied Non-classical Logic.

Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Feature Integration as Substitution. Logrippo, L. and D. Amyot (eds.), Feature Interactions in Telecommunications and Software Systems VII, IOS Press, Amsterdam, 2003, pp. 275-294.

Dimitar P. Guelev and Dang Van Hung. Projection onto State in Duration Calculus: Relative Completeness (Extended Abstract). Third Workshop on Automatic Verification of Critical Systems (AVoCS'03), Southampton, UK, April 2-3, 2003.

Dimitar P. Guelev and Dang Van Hung. Prefix and Projection onto State in Duration Calculus. Proceedings of the ETAPS workshop Theory and Practice of Timed Systems (TPTS'02), 2002. Electronic Notes in Theoretical Computer Science volume 65, Issue 6, Elsevier Science.

Dimitar P. Guelev and Mark D. Ryan. Logical Analysis of Feature Integration. Second Workshop on Automatic Verification of Critical Systems (AVoCS'02), April 15-16, 2002, Birmingham, United Kingdom.

Dang Van Hung and Dimitar P. Guelev. Real-Time Refinement with State Projections. Presented at the UNU/IIST 10th Anniversary Colloquium, March 18-22, 2002, Lisbon, Portugal.

Dimitar P. Guelev. A Complete Fragment of the Higher-order Duration µ-Calculus. Proceedings of FST TCS 2000, LNCS 1974, Springer, 2000, pp. 264-276.

Dimitar P. Guelev. Interval-related Interpolation in Interval Temporal Logics. Proceedings of ICTL 2000. A revised version appeared in the Logic Journal of the IGPL.

Dimitar P. Guelev. Probabilistic Neighbourhood Logic. Proceedings of FTRTFT 2000, LNCS 1926, Springer, 2000, pp. 264-275.

Zhou Chaochen, Dimitar P. Guelev, and Zhan Naijun. A Higher-Order Duration Calculus. Jim Davies, Bill Roscoe and Jim Woodcock (eds.) Millenial Perspectives in Computer Science. Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Professor Sir Anthony Hoare, Palgrave, 2000, pp. 407-416.

Dang Van Hung and Dimitar P. Guelev. Completeness and Decidability of a Fragment of Duration Calculus with Iteration. Proceedings of ASIAN'99, LNCS 1742, Springer-Verlag, 1999, pp. 139-150.

Technical Reports

UNU/IIST reports listed below are no longer available from http://www.iist.unu.edu .

Dimitar P. Guelev and Dang Van Hung. Reasoning about QoS contracts in the Probabilistic Duration Calculus. UNU/IIST Technical Report 384, September 2008. Presented at the ETAPS workshop Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA), 2008.

Dimitar P. Guelev and Dang Van Hung. Projection onto State in Duration Calculus: Relative Completeness. UNU/IIST Technical Report 269, November 2002. An extended abstract was presented at the Third Workshop on Automatic Verification of Critical Systems (AVoCS'03).

Dimitar P. Guelev and Dang Van Hung. Prefix and Projection onto State in Duration Calculus. UNU/IIST Technical Report 236, April 2001. Appeared in the Proceedings of the ETAPS workshop Theory and Practice of Timed Systems (TPTS'02).

Dimitar P. Guelev. Interpolation and Related Results on the P-fragment of Duration Calculus with Iteration. UNU/IIST Technical Report 203, June 2000.

Dimitar P. Guelev. Probabilistic Neighbourhood Logic. UNU/IIST Technical Report 196, April 2000. A short version appeared in the Proceedings of FTRTFT 2000.

Dimitar P. Guelev. A Complete Proof System for First Order Interval Temporal Logic with Projection. UNU/IIST Technical Report 202, June 2000. A revised version appeared in the Journal of Logic and Computation.

Dimitar P. Guelev. A Complete Fragment of the Higher-order Duration µ-Calculus. UNU/IIST Technical Report 195, April 2000. A short version appeared in the Proceedings of FST TCS 2000, LNCS 1974, Springer, 2000.

Dimitar P. Guelev. Probabilistic Interval Temporal Logic, UNU/IIST Technical Report 144, August 1998, Draft. Superceded by Report 196 of UNU/IIST.

Zhou Chaochen, Dimitar P. Guelev, and Zhan Naijun. A Higher-Order Duration Calculus. UNU/IIST Technical Report 167, July 1999. Published in the Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Professor Sir Anthony Hoare, Palgrave, 2000.

Dang Van Hung and Dimitar P. Guelev. Completeness and Decidability of a Fragment of Duration Calculus with Iteration. UNU/IIST Technical Report 163, April 1999. Appeared in the Proceedings of ASIAN'99.

Dimitar P. Guelev. Quantification over State in Duration Calculus is Essentially First Order. Technical Note 52, DeTfoRS, UNU/IIST, P.O.Box 3058, Macau, July 1998.

Dimitar P. Guelev. An Undecidable Fragment of Propositional Interval Temporal Logic, Technical Note 50, DeTfoRS, UNU/IIST, P.O.Box 3058, Macau, May 1998.

Dimitar P. Guelev. Iteration of Simple Formulas in Duration Calculus. UNU/IIST Technical Report 141, June 1998. Appeared in the Proceedings of ASIAN'99, 1999, as part of joint paper with Dang Van Hung.

Dimitar P. Guelev. A Calculus of Durations on Abstract Domains: Completeness and Extensions. UNU/IIST Technical Report 139, May 1998.

Theses

Probabilistic and Temporal Modal Logics, In Bulgarian. Ph.D. thesis, Faculty of Mathematics and Informatics, Sofia University, February, 2000.

A Strong Completeness Theorem for the Probabilistic Logic of Segerberg. M. Sc. thesis, Sofia University, 1994. In Bulgarian. An extended version appeared in the Journal of Philosophical Logic.

Last updated: November, 2023

 

Home | Institute of Mathematics and Informatics | BAS