Modal logics have found applications in many diferent 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 secondorder properties that are expressible, for example, in the μ-calculus. Here 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.
| Identifer | oai:union.ndltd.org:ADTP/221304 |
| Date | January 2006 |
| Creators | French, Timothy Noel |
| Publisher | University of Western Australia. School of Computer Science and Software Engineering |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
| Rights | Copyright Timothy Noel French, http://www.itpo.uwa.edu.au/UWA-Computer-And-Software-Use-Regulations.html |
Page generated in 0.0017 seconds