Proof Methods for Branching-Time Logic.

 

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.

 

Related publications

Some of the publications below are available electronically. Otherwise, please contact me if you require a copy.


 

Journal Articles

 

 

[1] A Clausal Resolution Method for Branching Time Logic ECTL+ (with A. Basukoski). Annals of Mathematics and Artificial Intelligence, Springer, 46(3): 235-263

    (2006), ISSN: 1012-2443 (Print) 1573-7470 (Online), http://dx.doi.org/10.1007/s10472-006-9018-1. Available on-line from Springer.

[2] Clausal Resolution for Extended Computation Tree Logic ECTL (with A. Basukoski). Journal of Applied Logic, Elsevier, 4(2): 141-167 (2006), http://dx.doi.org/10.1016/j.apal.2005.03.002.

[3] Alternating Automata and Temporal Logic Normal Forms (with C. Dixon and M. Fisher). Annals of Pure and Applied Logic, Volume 135, Issues 1-3, September 2005, Pages 263-285, Elsevier. http://dx.doi.org/10.1016/j.apal.2005.03.002. Available online from Sciencedirect.

[4] On the Relationship between Normal Form and “w”-automata (with M. Fisher and C. Dixon). Journal of Logic and Computation, Volume 12, Issue 4, August 2002, pages 561-581, Oxford University Press, ISSN: 0955-792X. http://www3.oup.co.uk/logcom/hdb/Volume_12/Issue_04/120561.sgm.abs.html.

 

[5] 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, http://dx.doi.org/10.1016/S0004-3702(02)00196-0. Available online from Sciencedirect.

 

[6] A Clausal Resolution Method for CTL Branching Time Temporal Logic (with M. Fisher). Journal of Experimental and Theoretical Artificial Intelligence, volume 11, 1999, pages 77-93, Taylor & Francis. ISSN: 1362-3079 (electronic) 0952-813X (paper). Draft version.

 

Conference/workshop  Proceedings

 

[7]  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.

 

[8] Invariant-Free Deduction for CTL*: The Tableau Method (with Jose Gaintzarain and Paqui Lucio) The 17th Workshop on Automated Reasoning, (ARW 2010), University of Westminster, March 2010.

 

 [9] 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.

 

[10] 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.

 

[12] 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.

 

[13] 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.

[14] 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.

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

[16] Clausal Resolution for ECTL+: Complexity Analysis (with A. Basukoski). Proceedings of IEEE 2006 John Vincent Atanasoff International Symposium o Modern Computing, 3-6 October 2006, Sofia, Bulgaria, pages 1-6 (Young Researchers Session).

[17] 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.

 

[18] 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.

[19] Search Strategies for Resolution in CTL-Type Logics: Extension and Complexity, (with A. Basukoski). Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, 2005. TIME 2005. 23-25 June 2005,  IEEE Computer Society 2005, pages 195 - 197.

[20] Clausal Resolution in the Framework of Social Agency (with I. Swigkos) The 12th Workshop on Automated Reasoning, (ARW 2005), Edinburgh, 2005.

[20] Clausal Resolution for Extended Computation Tree Logic ECTL+ (with A. Basukoski). Proceedings of the Time 2004 International Conference on Temporal Representation and Reasoning, France, Tatihou, July 2004, pages 140-147.

[21] Clausal Resolution for Extended Computation Tree Logic ECTL. Proceedings of the Time-2003/ICTL-2003 International Conference on Temporal Representation and Reasoning/International Conference on Temporal Logic (Australia, July 2003), IEEE Computer Society, 2003, pages 107-117.

 

[22] Resolution for Branching Time Temporal Logics.  Smirnov's Readings. 4th International Conference, Moscow, 2003.

 

[23] Clausal Resolution for Extended Computation Tree Logic ECTL. 10th Workshop on Automated        

      Reasoning,  AR2003, Liverpool, 2003.

 

[24] Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule (with C. Dixon). Proceedings of the Time-2000 International Conference on Temporal Representation and Reasoning (Nova Scotia, Canada, July 2000), IEEE Computer Society, 2000, pages 163-172.

 

[25] 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.

 

[26] On the Relationship between Normal Form and `w’-automata (with M. Fisher and C. Dixon).  Proceedings of the Advances in Modal Logic - International Conference on Temporal Logic 2000 (University of Leipzig, October 2000), pages 13-22.

 

[27] Automata on Infinite Words and Temporal Logic Normal Forms. 7th Workshop on Automated Reasoning (AR2000), King’s College, London, 2000.

 

[28] General Normal Form for Temporal Logic. British Colloquium of Theoretical Computer Science (BCTCS16), Liverpool, 2000.

 

[29] Clausal Resolution for Branching-time Logics. PhD, Manchester Metropolitan University.

 

[30] Clausal Resolution for Branching-Time Logic (with M. Fisher). Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science (Crakow, Poland, August 1999), pages 137-148.

 

[31] Clausal Resolution for CTL* (with C. Dixon, and M. Fisher) Mathematical Foundations of Computer Science, Proceedings of the 24th International Symposium (MFCS'99), (Poland, August 1999), volume 1672 of Lecture Notes in Computer Science, Springer, 1999, pages 137-148.

 

[32] Clausal Resolution for Branching-Time Temporal Logics and Temporal Mu-Calculus. 6th Workshop on Automated Reasoning, Edinburgh, 1999.

 

[33] A Resolution Method for CTL Branching-Time Temporal Logic (with M. Fisher). Proceedings of the 4th International Workshop on Temporal Representation and Reasoning (TIME'97) (Florida, 1997), IEEE Computer Society, pages 20-27.

 

[34] Clausal Resolution for CTL. British Colloquium of Theoretical Computer Science (BCTCS13), Sheffield, 1997.