School of Computer Science and Software Engineering

Postgraduate profiles

Contact

Tim French


Start date

Submission date

Dec 2006

Tim French

Thesis

Bisimulation quantifiers for modal logics

Summary

Modal logics have found applications in many different contexts. For example, epistemic modal logics can be used to reason about security protocols, temporal modal logics can be used to reason about the correctness of distributed systems and propositional dynamic logic can reason about the correctness of programs. However, pure modal logic is expressively weak and cannot represent many interesting second order properties that are expressible, for example, in the μ-calculus we investigate the extension of modal logics with propositional quantification modulo bisimulation (bisimulation quantification). We extend existing work on bisimulation quantified modal logic by considering the variety of logics that result by restricting the structures over which they are interpreted. We show this can be a natural extension of modal logic preserving the intuitions of both modal logic and propositional quantification. However, we also find cases where such intuitions are not preserved. We examine cases where the axioms of pure modal logic and propositional quantification are preserved and where bisimulation quantifiers preserve the decidability of modal logic. We translate a number of recent decidability results for monadic second order logics into the context of bisimulation quantified modal logics, and show how these results can be used to generate a number of interesting bisimulation quantified modal logics.

Why my research is important

As pure modal logic is expressively weak and cannot represent many interesting second order properties that are expressible, we investigate the extension of modal logics with propositional quantification modulo bisimulation (bisimulation quantification).

The research also extends existing work on bisimulation quantified modal logic.


 

School of Computer Science and Software Engineering

This Page

Last updated:
Wednesday, 13 February, 2013 8:19 AM

http://web.csse.uwa.edu.au/430207