Return to search

Bisimulation quantifiers for modal logics

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.

Identiferoai:union.ndltd.org:ADTP/221304
Date January 2006
CreatorsFrench, Timothy Noel
PublisherUniversity of Western Australia. School of Computer Science and Software Engineering
Source SetsAustraliasian Digital Theses Program
LanguageEnglish
Detected LanguageEnglish
RightsCopyright Timothy Noel French, http://www.itpo.uwa.edu.au/UWA-Computer-And-Software-Use-Regulations.html

Page generated in 0.0017 seconds