Dimitar P. Guelev  publications 

Ben Moszkowski and Dimitar P. Guelev. An Application of Temporal Projection to Interleaving Concurrency. Formal Aspects of Computing, volume 29, issue 4, pp 705750, 2017. Dimitar P. Guelev. Refining Strategic Ability in ATL. Information and Computation. Special issue
on selected papers from the 2^{nd
}Intl. Workshop on Strategic Reasoning (SR 2014), volume 254,
pp. 316328, 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 13, pp. 19, 2014. Dimitar P. Guelev, Catalin Dima and Constantin Enea. An Alternatingtime Temporal Logic with Knowledge, Perfect Recall and Past: Axiomatisation and Model Checking. Journal of Applied Nonclassical Logic, volume 21, issue 1, pp. 93131, 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. 615623, 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. 161, 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 PierreYves Schobbens. Modelchecking the Preservation of Temporal Properties upon Feature Integration. Software Tools for Technology Transfer, volume 9, issue 1, pp 5362, 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. Dimitar P. Guelev and Dang Van Hung. A Relatively Complete Axiomatisation of Projection onto State in the Duration Calculus. Journal of Applied Nonclassical Logic, volume 14, issue 12, pp. 149180, 2004. Dimitar P. Guelev. Logical Interpolation and Projection onto State in the Duration Calculus. Journal of Applied Nonclassical Logic, volume 14, issue 12, 2004, pp. 181208. 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. 215249, 2004. Dimitar P. Guelev. Intervalrelated Interpolation in Interval Temporal Logics. Logic Journal of the IGPL, volume 9 issue 5, 2001, pp. 677685. Presented at ICTL 2000. Dimitar P. Guelev. A Propositional Dynamic Logic with Qualitative Probabilities. Journal of Philosophical Logic, volume 28, number 6, 1999, pp. 575605. Conference and workshop papers Dimitar P. Guelev,.Shuling Wang and Naijun Zhan. Compositional
HoareStyle Reasoning About Hybrid CSP in the Duration Calculus. Proceedings of SETTA 2017, LNCS 10606,
SpringerVerlag, 2015, pp. 110127. Ben Moszkowski and Dimitar P. Guelev. An Application of Temporal Projection to Interleaving Concurrency. Proceedings of SETTA 2015, LNCS 9409, SpringerVerlag, 2015, pp. 153167. Dimitar P. Guelev, Shuling Wang, Naijun Zhan and Chaochen Zhou. SuperDense Computation in Verification of Hybrid CSP Processes. Proceedings of FACS 2013, LNCS 8348, SpringerVerlag, 2014, pp. 1322. Dimitar P. Guelev. Refining and Delegating Strategic Ability in ATL. Presented and published in the Proceedings of the 2^{nd }Intl. Workshop on Strategic Reasoning (SR 2014), EPTCS, volume 146, pp 5764, 2014. Dimitar P. Guelev. Reducing Validity in Epistemic ATL to Validity in Epistemic CTL. Presented and published in the Proceedings of the 1^{st }Intl. Workshop on Strategic Reasoning (SR 2013), EPTCS, volume 112, pp 8190, 2013. Dimitar P. Guelev and Catalin Dima. Epistemic ATL with Perfect Recall, Past and Strategy
Contexts. Proceedings
of CLIMA XIII, LNCS 7486, SpringerVerlag, 2012, pp. 7793. Wang Shuling, Zhan Naijun and Dimitar
P. Guelev. An Assume/Guarantee Based Compositional Calculus for Hybrid
CSP. Proceedings of
TAMC 2012, LNCS 7287, SpringerVerlag, 2012, pp. 7283. 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 MultiAgent Systems (LAMAS 2011), Osuna, Spain, November
2011, Electronic Notes in
Theoretical Computer Science, volume 278, pp. 229243, 2011. Catalin Dima, Constantin Enea, Dimitar Guelev and Ferucio Tiplea. Positive and negative results on the modelchecking 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. ModelChecking an Alternatingtime 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 103117, 2010. Dimitar P. Guelev and Catalin Dima. Modelchecking 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. 7590. 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 ComponentBased Software Architectures (FESCA), 2008. Electronic Notes in Theoretical Computer Science, volume 238, issue 6, pp. 4162, 2010. Nan Zhang, Mark Ryan and Dimitar P. Guelev, Evaluating Access Control Policies through Modelchecking. Presented and published in the Proceedings of the 8th Information Security Conference (ISC'05), Singapore, September 2005, LNCS 3650, Springer, 2005, pp. 446460. Dimitar P. Guelev, Mark D. Ryan and PierreYves 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. 7993, 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. 5665. Dimitar P. Guelev, Mark D. Ryan and PierreYves Schobbens. Modelchecking 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. 311324, 2005. A revised version in Software Tools for Technology Transfer, volume 9, issue 1, pp 5362, 2007. Dimitar P. Guelev. Sharpening the Incompleteness of the Duration Calculus. Proceedings of the AMAST Workshop on Realtime Systems (ARTS), Stirling, UK, June 2004. Electronic Notes in Theoretical Computer Science, volume 139, issue 1, pp. 91104, 2005. Dimitar P. Guelev, Mark D. Ryan and PierreYves Schobbens. Modelchecking 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. 219230. 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 Nonclassical Logic. Dimitar P. Guelev, Mark D. Ryan and PierreYves Schobbens. Feature Integration as Substitution. Logrippo, L. and D. Amyot (eds.), Feature Interactions in Telecommunications and Software Systems VII, IOS Press, Amsterdam, 2003, pp. 275294. 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 23, 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 1516, 2002, Birmingham, United Kingdom. Dang Van Hung and Dimitar P. Guelev. RealTime Refinement with State Projections. Presented at the UNU/IIST 10th Anniversary Colloquium, March 1822, 2002, Lisbon, Portugal. Dimitar P. Guelev. A Complete Fragment of the Higherorder Duration µCalculus. Proceedings of FST TCS 2000, LNCS 1974, Springer, 2000, pp. 264276. Dimitar P. Guelev. Intervalrelated 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. 264275. Zhou Chaochen, Dimitar P. Guelev, and Zhan Naijun. A HigherOrder Duration Calculus. Jim Davies, Bill Roscoe and Jim Woodcock (eds.) Millenial Perspectives in Computer Science. Proceedings of the 1999 OxfordMicrosoft Symposium in Honour of Professor Sir Anthony Hoare, Palgrave, 2000, pp. 407416. Dang Van Hung and Dimitar P. Guelev. Completeness and Decidability of a Fragment of Duration Calculus with Iteration. Proceedings of ASIAN'99, LNCS 1742, SpringerVerlag, 1999, pp. 139150. 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 ComponentBased 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 Pfragment 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 Higherorder 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 HigherOrder Duration Calculus. UNU/IIST Technical Report 167, July 1999. Published in the Proceedings of the 1999 OxfordMicrosoft 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. 

