On Some Issues Of N-refinement Modal Logic

Propositional modal logics are extensions of the propositional logic by adding modal operators,which are adopted to describe properties of dynamic systems based on states and capture epistemic laws of multi-agent system.The occurrence of informative events will lead to the change of an agent's epistemic attitudes.In order to capture the internal logical laws of such changes,the notion of refinement is introduced.Recently,a so called refinement modal logic has been presented by Laura Bazzelli,which provides an external and global perspective on refinement relations on the level of object language.This logic system is obtained from propositional modal logic by adding refinement-quantifier ?(?).A pointed model satisfies ?(or ?)means all(some,resp.)refinement models of satisfy .Such refinement-quantifier can be used to describe related issues in formal modeling and epistemic changing of multi-agent systems.The notion of refinement requests that the simulations between models are always preserved while states transfer.However,in some situation,e.g.,formal designing of control systems and real systems e.t.c(they are described as LTS with quantitative information),we often consider finite approximation of refinement,which is captured by the notion of n-refinement.Based on the notion of n-refinement,this thesis aims to present and explore n-refinement modal logic by introducing n-refinement quantifier.Main contributions include:(1)Present n-refinement modal logic,give its axiomatic system and establish its soundness andcompleteness by showing that each n-refinement modal logic formula is proviablyequivalent to a formula in K-system.(2)Based on the notion of relativizatioin,we consider the translation from the n-refinementmodal logic language to the n-bisimulation quantization language.(3)Present the n-refinement modal ? calculus and its axiomatic system,and prove its soundnessand completeness based on(2).