Verification of Branch-Time Property Based on Dynamic Description Logic

摘要：

　　The dynamic description logic DDL provides formalism for describing dynamic system in the semantic Web environment Model checking is a formal verification method based on state transition system.In this paper, we bring dynamic description logic into model checking.Firstly, state transition systems considered in model checking are modeled as complex actions in dynamic description logic.Secondly, a kind of temporal description logic DL-CTL is introduced to specify temporal properties on state transition systems, where DL-CTL is a DL-based extension of propositional branch-time temporal logic CTL.Finally, verification algorithm is presented with the help of reasoning mechanisms provided by description logic.

关键词： dynamic description logic verification temporal description logic action theory

作者: Yaoguang Wang Liang Chang Fengying Li Tianlong Gu

作者单位: Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China

会议类型: 国际会议

会议名称: 8th International Conference on Intelligent Information Processing(2014年IFIP智能信息处理国际会议)

会议地点: 杭州

会议语种:英文

页码: 161-170

在线出版日期: 2014-10-01（万方平台首次上网日期，不代表论文的发表时间）