For a number of years, temporal and modal logics have been used as the basis of formal methods for reactive systems. With the advent of more complex applications, *combinations* of temporal and modal logics are increasingly required. Examples of areas where such logics have been used (or proposed) include agent-based systems, accident analysis, temporal databases, legal reasoning, knowledge representation, and distributed systems security. In spite of this increasing level of use, proof methods for these logics are rare, particularly in cases where temporal and modal dimensions interact.
In this seminar, I will provide background on these combined temporal and modal logics, and sketch how such logics might be applied. I will then describe the resolution-based approach that we use for proving properties within these logics, particularly concentrating on the combination of temporal and epistemic logics. Finally, I will highlight current problems and consider how these will be addressed in our future work.
For more information about this talk contact: M.Fisher@doc.mmu.ac.uk