|
|
School of Computer Science & Software Engineering |
Tim French's Home Page
Tim is a lecturer in The School of Computer Science and Software Engineering at the University of Western Australia.
Teaching
Semester 1, 2008: CITS2200 - Data Structures and AlgorithmsSemester 2, 2008: CITS3210 - Algorithms
Semester 2, 2008: CITS7212 - Computational Intelligence
Semester 2, 2008: CITS1220 - Software Engineering
Semester 2, 2008: MCTX2420 - Mechatronic Systems (Finite State Machines)
I am available for consultation in room 2.14 of the computer science and software engineering building on Wednesday, 10.00-11.30, during semester. To arrange a meeting outside these times, please email.
Research
My research is on extensions of modal logics, and their applications to formal methods for software engineering. I wrote my PhD thesis on bisimulation quantifiers for modal logics. This work has applications in the automated reasoning about properties of various systems and programs, and particularly for reasoning about different levels of abstraction.
The following are unpublished works I have written:
- Counting points on elliptic curves and applications to cryptography.This was my honours thesis, and isn't strongly related to my current research.
- A proof of the completeness of PLTL. This paper just fills in the details for the proof given by Gabbay, Pnueli, Shelah and Stavi, in "On the temporal analysis of fairness" (1980).
- Bisimulation quantifiers for modal logics. This is my PhD. thesis, and was passed in 2006. It describes the application of bisimulation quantifiers to a range of modal logics and presents several decidability and expressivity results.
Publications
Below is a list of some of my publications, in chronological order.
- Decidability of branching time logics with quantified propositions. This was presented at the 14th Australian Joint Conference on Artificial Intelligence.
- A sound and complete proof system for QPTL. This paper was co-written with Mark Reynolds and was presented at AiML'02.
- Quantified propositional temporal logic with repeating states. This was presented at the TIME-ICTL 2003.
- Decidability of propositionally quantified logics of knowledge. This paper is an updated version of a paper that was presented at the 16th Australian Joint Conference on Artificial Intelligence.
- Complete axiomatizations for logics of knowledge and past time. This paper was co-written with Ron van der Meyden and Mark Reynolds, and is a long version of a paper that has been submitted to Advances in Modal Logic, 2004
- Bisimulation quantified logics: undecidability. This is a version of a paper that appeared at FSTTCS, 2005
- Bisimulation quantified logics: decidability. This is a version of a paper that appeared at AiML, 2006
- mu-programs, uniform interpolation and bisimulation quantifiers for modal logics (with Giovanna D'Agostino and Giacomo Lenzi). This paper appeared in the Journal of Applied Non-classical Logics, vol 16, 3-4, 2006.
- Idempotent transduction logics. This is a version of a paper that appeared at FroCoS, 2007
- A temporal logic of robustness. This paper was written with John McCabe-Dansted and Mark Reynolds. It appeared at FroCoS, 2007
Projects
I will periodically describe Professional Computing, Honours, Masters, and PhD projects I have available here. Please contact me if you are interested in any of these projects.
- Specifying and refining security policies The project would consider the implementation of tools to support the formal reasoning about security policies. Particularly, we would be interested in representing the knowledge of a group of agents, and how these agents can evolve there knowledge over time. The project will involve implementing known algorithms to automatically determine the correctness of such policies.
- Auctions for autonomus agents
This project would investigate the design of online auctions and the agents who would bid in these auctions. The aim is to provide an auction system that provides optimal results for both buyers and sellers, where the buyers are simple autonomous agents.- Automated collection of meta-data from software repositories
(with A/Prof Mark Reynolds). Software development companies often maintain repositories of software modules they have previously used. To efficiently reuse these modules they must have sufficient meta-data about the modules purpose, and this meta-data is often lacking. This project would look at methods to automatically generate such meta-data.- Algorithms for model-checking (with A/Prof Mark Reynolds).
Model-checking is the process of verifying that an implementation satisfies some formally specified property. This project would investigate the development of efficient algorithms for model-checking complex properties. This is a very difficult problem and it is not expected that a complete solution will be produced.- Reasoning about Trust
Trust is an integral concept in many areas such as security (do we trust someone is who they say they are), data management (do we trust a database to keep our personal details private) and sensor networks (do we trust that the data from a sensor is accurate). In many of these applications trust i s dealt with in an ad hoc manner. This project would look at designing theories for reasoning about trust in a general sense. We would be interested in designing algorithms to answer questions such as "how many sensors do I need to trust in order to infer property p?", or "Can I trust agent Alice, and not trust agent Bob at the same time?". The project would establish a common semantic for trust based problems and design some simple algorithms for reasoning about trust.
Pictures
I am on the left. Isaac is in the middle. Diane is on the right.
|
Last updated 18/3/2008.