Temporal Verification of Parameterized Systems

When?

Wednesday 12 December 2007, 14:00 to 15:00

Where?

39BB02

Open to:

Staff, Students

Abstract:

In this talk, I will consider the analysis of infinite-state systems using temporal logic. In particular, I will address the problem of specifying and verifying parameterized systems. These are infinite-state systems, typically comprising arbitrary numbers of identical processes. Such systems are increasingly important, with practical problems of an open, distributed nature often fitting into this model, for example in areas such as: multi-agent systems; communications protocols; swarm robotics.

However, while verification techniques for such parameterized systems are important, and automated methods are desirable, the verification problem is inherently difficult. We will show how first-order temporal logics can be used to specify certain classes of parameterized system and how deductive methods for these logics can be used in property verification. Such an approach provides a complete and decidable route to the verification of parameterized systems.

In the second part of the talk, I will address current research issues concerning this approach. Firstly, what can we
say about parameterized systems when some number of components fail? Specifically, how can we cope with the problem of not knowing exactly how many components will fail, but knowing that only a finite number of failures can occur? Secondly, can we improve the complexity of the basic deductive process to enable temporal deduction to become a viable verification method? Can we modify the underlying temporal logic to give temporal deduction a complexity closer to that of model checking?

* This work is joint with Boris Konev, Alexei Lisitsa and (concerning the last part of the talk) Clare Dixon.

* Relevant papers (all available from my WWW page) are:

- Fisher, M., Lisitsa, A., and Konev, B. "Practical Infinite-state Verification with Temporal Reasoning." In Verification of Infinite-State Systems with Applications to Security". IOS Press, 2006.

- Degtyarev, A., Fisher, M., and Konev, B. "Monodic Temporal Resolution." ACM Transactions on Computational Logic 7(1):108-150. ACM Press, 2006.

- Dixon, C., Fisher, M., and Konev, B. "Tractable Temporal Reasoning." In Proc. International Joint Conference on Artificial Intelligence (IJCAI), pp 318-323. AAAI Press, 2007.

- Fisher, M., Konev, B., and Lisitsa, A. "Temporal Verification of Fault-Tolerant Protocols." In IFM'07 Workshop on Methods, Models and Tools for Fault Tolerance (MeMoT), Oxford, UK, 2007.

Notes

Professor Michael Fisher is Professor of Computer Science within the Department of Computer Science at the University of Liverpool, Director of the Liverpool Verification Laboratory, and head of the Logic and Computation research group.

My research interests concern the use of Logic in Computer Science and Artificial Intelligence, particularly temporal reasoning, theorem-proving, programming languages, formal verification, and autonomous and agent-based systems. I have been active in research for over 20 years, have produced many books and papers, and am involved in a number of current research projects.

In addition to my research activities, I Chair the Department's Industrial Liaison Committee and am a member of both its Management and Research Committees. I am a Fellow of the British Computer Society, a Fellow of the IET, and a Member of the UK Computing Research Committee.

For more information about Prof Fisher please refer to his home page: http://www.csc.liv.ac.uk/~michael/