动态逻辑AUL中的秘密宣告

Privacy in Arrow Update Logic

AUL(Arrow Update Logic)是一个刻画多主体的信念变化的动态逻辑。AUL通过更新模型中的可及关系来刻画行为对主体信念造成的影响。但是,在AUL中信息对所有主体都是公开的,因此AUL无法刻画在秘密宣告的情况下主体信念状态的变化。本论文在AUL的基础上进行扩充,得到一个新的动态逻辑系统PAUL(Private Arrow Update Logic)。所有基于事实的宣告都可以被PAUL刻画,无论该宣告是公开的还是秘密的。同时,本论文还给出了PAUL的语义图,并证明了PAUL是可判定的。

Arrow Update Logic is a theory of epistemic access elimination that can be used to reason about multi-agent belief change.In Arrow Update Logic,it is common knowledge among agents how each will process incoming information.This paper develops the basic theory of Arrow Update Logic to deal with private announcements.In this framework,the information is private for an agent group.Moreover,this paper proposes a labelled tableau calculus for this logic and also shows that this logic is decidable.