Formal Modelling of Concurrent and Distributed Systems, Intelligent Agents, Grid Systems.


Main results:

  • Development of the specification language for the Logic of Rational Agency and corresponding resolution based proof technique (KARO framework);
  • Extension of the specification language to capture Normative Agents; Introduction of the formal framework for specification and verification of Grid Component Model in the setting of Branching-time Logic;
  • Specification of Components and Resources for the General Component Model;
  • Application of the Automata-based Approach to represent General Component Model and its environment.

Main results:

·         Development of the Deductive Proof technique, the Clausal Resolution Method, for the Branching-time Logic setting, (computation tree logic CTL and its extensions) commonly used in computer science;

·         Extension of the applicability of the Clausal Resolution technique capturing Temporal Fixpoint Logics;

·         Formulation of a Loop Searching Algorithm enabling the automation of the method;

·         Study of expressiveness of obtained formalisms and complexity analysis.

                     This is the only clausal resolution based deductive proof method for branching-time logics

Journal Articles


[1]  Resolution in a Logic of Rational Agency (with C. Dixon and M. Fisher). Artificial Intelligence, volume 139, issue 1, July 2002, pages 47-89, Elsevier Science, Available online from Sciencedirect.

Conference/workshop  Proceedings


[2]  Handling Periodic Properties: Deductive Verification for Quantified Temporal Logic Specifications. Proceedings of the 5th IEEE International Conference on Secure Software Integration & Reliability Improvement Companion (SSIRI-C), pages: 179 – 186, Jeju Island, 27-29 June 2011, Print ISBN: 978-14577-0781-0.


[3] Safety and Liveness of Component-oriented Protocols: A Feasibility Study (with Shamima Paurobally and Vladimir Getov) The 17th Workshop on Automated Reasoning, (ARW 2010), University of Westminster, March 2010.


[4] Deontic Extension of Deductive Verification of Component Model: Combining Computation Tree Logic and Deontic Logic in Natural Deduction Style Calculus. (with A. Basso and O.Grigoriev) in Proceedings of the 4th Indian International Conference on Artificial Intelligence (IICAI-09), December 16-18, 2009, Tumkur, India.



[5]  Multi-Agent Systems in engineering of e-commerce and e-business systems (with S. Maltseva), RIW 2009: Russian Internet Week, Joint exhibition presentations (


[6] Temporal Specification and Deductive Verification of a Distributed Component Model and Its Environment. (with A. Basso, and V. Getov). Proceedings of the workshop Model-Based Verification and Validation in conjunction with the 3rd IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI)', Shanghai, China, July 2009.


[7] State-Based Behavior Specification for GCM Systems (with A. Basso, and V. Getov). The 16th Workshop on Automated Reasoning, (ARW 2008), University of Liverpool, April 2009.

 [8] Behavioural model of component-Based Grid Environments (with A. Basso and V.Getov)  In T. Priol and M. Vanneschi (Ed.), From Grids to Service and Pervasive Computing. Proceedings of the CoreGrid Symposium 2008, Las Palmas, Canary Island, August 2008 in conjunction with EUROPAR, Springer, 2008, pages 19-30, ISBN 978-0-387-78447-2.

[9] Automata-based Formal Specification of Stateful Systems (with Alessandro Basso and Vladimir Getov)  The 15th Workshop on Automated Reasoning, (ARW 2008), University of Birmingham, July 2008.

[10] Towards GCM re-configuration - extending specification by norms (with A. Basso) In Marco Danelutto, Paraskevi Fragopoulou and Vladimir Getov (Editors) Making Grids Work. Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments, 12-13 June 2007, Heraklion, Crete, Greece, Springer, 2007, pages 17-29, ISBN 978-0-387-09454-0.

[11] Verification tool Grid component system (with A.Basso). The 14th Workshop on Automated Reasoning, (ARW 2007), Imperial College, April 2007.


 [12] Specifcation and Verifcation of Reconfguration Protocols in Grid Component Systems (with Alessandro Basso, Artie Basukoski, Vladimir Getov, Ludovic Henrio, and Mariusz Urbanski) In the Proceedings of the 3d IEEE Conference on Intelligent Systems (IS-2006), September 2006.


 [13] Specifcation and Verifcation of Reconfguration Protocols in Grid Component Systems (with A. Basso, A. Basukoski, V. Getov, L. Henrio, and M. Urbanski). The 13th Workshop on Automated Reasoning, (ARW 2006), Bristol, July 2006.


[14] Resolution in a Logic of Rational Agency (with C. Dixon - main contributor, and M. Fisher).  Proceedings of the 14th European Conference on Artificial Intelligence (Berlin, August 2000), IOS Press.