In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge...In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.展开更多
Coalition logic （CL） is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by ...Coalition logic （CL） is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by [C]φ to state that a group of agents C can have a strategy to bring about φ by collective actions, no matter what the other agents do. However, CL lacks the temporal dimension and thus can not capture the dynamic aspects of a system. Therefore, CL can not formalize the evolvement of rational mental attitudes of the agents such as knowledge, which has been shown to be very useful in specifications and verifications of distributed systems, and has received substantial amount of studies. In this paper, we introduce coalition logic of temporal knowledge （CLTK）, by incorporating a temporal logic of knowledge （Halpern and Vardi＇s logic of CKLn） into CL to equip CL with the power to formalize how agents＇ knowledge （individual or group knowledge） evolves over the time by coalitional forces and the temporal properties of strategic abilities as well. Furthermore, we provide an axiomatic system for CLTK and prove that it is sound and complete, along with the complexity of the satisfiability problem which is shown to be EXPTIME-complete.展开更多
基金The National Natural Science Foundation of China (No.10974093)the Scientific Research Foundation for Senior Personnel of Jiangsu University (No.07JDG014)the Natural Science Foundation of Higher Education Institutions of Jiangsu Province (No.08KJD520015)
文摘In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.
基金This work was supported by National Basic Research Program of China （973 Program） （2010CB328103） the National Natural Science Foundation of China （Grant Nos. 61272415, 61003056, 71271061 and 61370177） ARC Future Fellowship （FT0991785） and Business Intelligence Key Team of Guangdong University of Foreign Studies （TD 1202）.
文摘Coalition logic （CL） is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by [C]φ to state that a group of agents C can have a strategy to bring about φ by collective actions, no matter what the other agents do. However, CL lacks the temporal dimension and thus can not capture the dynamic aspects of a system. Therefore, CL can not formalize the evolvement of rational mental attitudes of the agents such as knowledge, which has been shown to be very useful in specifications and verifications of distributed systems, and has received substantial amount of studies. In this paper, we introduce coalition logic of temporal knowledge （CLTK）, by incorporating a temporal logic of knowledge （Halpern and Vardi＇s logic of CKLn） into CL to equip CL with the power to formalize how agents＇ knowledge （individual or group knowledge） evolves over the time by coalitional forces and the temporal properties of strategic abilities as well. Furthermore, we provide an axiomatic system for CLTK and prove that it is sound and complete, along with the complexity of the satisfiability problem which is shown to be EXPTIME-complete.
