异构多智能体系统模型检查
|
摘要
模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑(ATL),也被给予了高度关注.根据智能体是否可以看到全局信息,分为不完全信息和完全信息;根据智能体是否可以记录历史信息,分为无记忆能力和无限记忆能力,提出了4种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而在一个多智能体系统中,考虑完全信息和无限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或无记忆能力时,仅在联合模态操作《A》φ和[[A]]φ的A里出现的智能体具备这种策略类型,而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即,智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题,提出了一种在语法层对智能体策略类型进行刻画的系统模型——带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入策略类型这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具Sh TMC.
Model-checking, an automatic verification methodology, has been applied to verify multi-agent systems. Alternating-time temporal logic(ATL), a property specification language for multi-agent systems was also investigated. According to whether agents are able to observe the whole information of the system and whether agents are able to record the history information, agents' strategies are divided into four types. These strategy abilities are defined in semantic level of ATL, as well as other logics. However, under perfect information and perfect recall setting, all agents have the same strategy ability. Under imperfect information and/or imperfect recall setting, only agents appeared in coalition modalities 《A》φ and [[A]]φ have imperfect information and/or imperfect recall strategies, while other agents not in A still have perfect information and perfect recall strategies. When coalition modalities are nested, same agents may have different strategy abilities to fulfill different sub formulas, which results in inconsistency. On the other hand, in practice, agents' strategy abilities are usually decided by the multi-agent systems rather than the specifications, and different agents may own different strategy abilities. This kind of multi-agent systems is called heterogeneous mutli-agent systems. To overcome these problems, this paper proposes a new formal model, called typed interpreted systems which are able to define agent's strategy abilities at syntax level. Typed interpreted systems extend interpreted systems by associating each agent with a strategy type denoting the agent's strategy ability, therefore are able to model heterogeneous mutli-agent systems. The paper investigates the semantics of ATL on this new model and proposes an EXPTIME model-checking algorithm. The model-checking algorithm is implemented in a prototype tool Sh TMC.
Model-checking, an automatic verification methodology, has been applied to verify multi-agent systems. Alternating-time temporal logic(ATL), a property specification language for multi-agent systems was also investigated. According to whether agents are able to observe the whole information of the system and whether agents are able to record the history information, agents' strategies are divided into four types. These strategy abilities are defined in semantic level of ATL, as well as other logics. However, under perfect information and perfect recall setting, all agents have the same strategy ability. Under imperfect information and/or imperfect recall setting, only agents appeared in coalition modalities 《A》φ and [[A]]φ have imperfect information and/or imperfect recall strategies, while other agents not in A still have perfect information and perfect recall strategies. When coalition modalities are nested, same agents may have different strategy abilities to fulfill different sub formulas, which results in inconsistency. On the other hand, in practice, agents' strategy abilities are usually decided by the multi-agent systems rather than the specifications, and different agents may own different strategy abilities. This kind of multi-agent systems is called heterogeneous mutli-agent systems. To overcome these problems, this paper proposes a new formal model, called typed interpreted systems which are able to define agent's strategy abilities at syntax level. Typed interpreted systems extend interpreted systems by associating each agent with a strategy type denoting the agent's strategy ability, therefore are able to model heterogeneous mutli-agent systems. The paper investigates the semantics of ATL on this new model and proposes an EXPTIME model-checking algorithm. The model-checking algorithm is implemented in a prototype tool Sh TMC.
引文
[1]Clarke EM,Grumberg O,Peled DA.Model Checking.Cambridge:MIT Press,1999.
[2]Clarke EM,Emerson EA.Design and synthesis of synchronization skeletons using branching-time temporal logic.In:Proc.of the Workshop on Logics of Programs.Berlin:Springer-Verlag,1981.52-71.[doi:10.1007/978-3-540-69850-0_12]
[3]Kupferman O,Vardi MY.Module checking.In:Proc.of the 8th Int’l Conf.on Computer Aided Verification.Berlin:SpringerVerlag,1996.75-86.[doi:10.1007/3-540-61474-5_59]
[4]Muscettola N,Nayak PP,Pell B,Williams BC.Remote agent:To boldly go where no AI system has gone before.Artificial Intelligence,1998,103(1-2):5-47.[doi:10.1016/S0004-3702(98)00068-X]
[5]Alur R,Henzinger TA,Kupferman O.Alternating-Time temporal logic.Journal of the ACM,2002,49(5):672-713.[doi:10.1145/585265.585270]
[6]Schobbens P.Alternating-Time logic with imperfect recall.Electronic Notes in Theoretical Computer Science,2004,85(2):82-93.[doi:10.1016/S1571-0661(05)82604-0]
[7]Dima C,Tiplea FL.Model-Checking ATL under imperfect information and perfect recall semantics is undecidable.Co RR,abs/1102.4225,2011.
[8]Jamroga W,Dix J.Model checking abilities under incomplete information is indeed Delta2-complete.In:Proc.of the 4th European Workshop on Multi-Agent System.CEUR-WS,2006.
[9]Pilecki J,Bednarczyk MA,Jamroga W.Model checking properties of multi-agent systems with imperfect information and imperfect recall.In:Proc.of the 7th Int’l Conf.on Intelligent Systems.Berlin:Springer-Verlag,2014.415-426.[doi:10.1007/978-3-319-11313-5_37]
[10]Jamroga W.Logical Methods for Specification and Verification of Multi-Agent Systems.Warszawa:ICS PAS Publishing House,2015.
[11]Chatterjee K,Henzinger TA,Piterman N.Strategy logic.In:Proc.of the 18th Int’l Conf.on Concurrency Theory.Berlin:SpringerVerlag,2007.59-73.[doi:10.1007/978-3-540-74407-8_5]
[12]Mogavero F,Murano A,Vardi MY.Reasoning about strategies.In:Proc.of the Annual Conf.on Foundations of Software Technology and Theoretical Computer Science.Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik,2010.133-144.[doi:10.4230/LIPIcs.FSTTCS.2010.133]
[13]Mogavero F,Murano A,Vardi MY.Reasoning about strategies:On the model-checking problem.ACM Trans.on Computational Logic,2014,15(4):34:1-34:47.[doi:10.1145/2631917]
[14]Jamroga W.Some remarks on alternating temporal epistemic logic.In:Proc.of the Formal Approaches to Multi-Agent Systems.2003.133-140.
[15]Hoek W,Wooldridge M.Cooperation,knowledge,and time:Alternating-time temporal epistemic logic and its applications.Studia Logica,2003,75(1):125-157.[doi:10.1023/A:1026185103185]
[16]Lomuscio A,Raimondi F.Model checking knowledge,strategies,and games in multi-agent systems.In:Proc.of the 5th Int’l Joint Conf.on Autonomous Agents and Multiagent Systems.New York:ACM Press,2006.161-168.[doi:10.1145/1160633.1160660]
[17]Hoek W,Wooldridge M.Tractable multiagent planning for epistemic goals.In:Proc.of the 1st Int’l Joint Conf.on Autonomous Agents and Multiagent Systems.New York:ACM Press,2002.1167-1174.[doi:10.1145/545056.545095]
[18]Bulling N,Jamroga W.Alternating epistemic mu-calculus.In:Proc.of the 22nd Int’l Joint Conf.Artificial Intelligence.Austin:AAAI,2011.109-114.[doi:10.5591/978-1-57735-516-8/IJCAI11-030]
[19]Agotnes T,Goranko V,Jamroga W.Alternating-Time temporal logics with irrevocable strategies.In:Proc.of the 11th Conf.on Theoretical Aspects of Rationality and Knowledge.New York:ACM Press,2007.15-24.[doi:10.1145/1324249.1324256]
[20]Pinchinat S.A generic constructive solution for concurrent games with expressive constraints on strategies.In:Proc.of the 5th Int’l Symp.on Automated Technology for Verification and Analysis.Berlin:Springer-Verlag,2007.253-267.[doi:10.1007/978-3-540-75596-8_19]
[21]Lopes ADC,Laroussinie F,Markey N.ATL with strategy contexts:Expressiveness and model checking.In:Proc.of the IARCS Annual Conf.on Foundations of Software Technology and Theoretical Computer Science.Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik,2010.120-132.[doi:10.4230/LIPIcs.FSTTCS.2010.120]
[22]Laroussinie F,Markey N.Augmenting ATL with strategy contexts.Information and Computation,2015,245:98-123.[doi:10.1016/j.ic.2014.12.020]
[23]Goranko V,Kuusisto A,R?nnholm R.Game-Theoretic semantics for ATL+with applications to model checking.In:Proc.of the16th Conf.on Autonomous Agents and Multi Agent Systems.New York:ACM Press,2017.1277-1285.
[24]Wang F,Schewe S,Huang CH.An extension of ATL with strategy interaction.ACM Trans.on Programming Languages and Systems,2015,37(3):9:1-9:41.[doi:10.1145/2734117]
[25]Huang CH,Schewe S,Wang F.Model-Checking iterated games.Acta Informatica,2017,54(7):625-654.[doi:10.1007/s00236-016-0277-y]
[26]Lomuscio A,Qu H,Raimondi F.MCMAS:A model checker for the verification of multi-agent systems.In:Proc.of the 21st Int’l Conf.on Computer Aided Verification.Berlin:Springer-Verlag,2009.682-688.[doi:10.1007/978-3-642-02658-4_55]
[27]Lomuscio A,Qu H,Raimondi F.MCMAS:An open-source model checker for the verification of multi-agent systems.Int’l Journal on Software Tools for Technology Transfer,2017,19(1):9-30.[doi:10.1007/s10009-015-0378-x]
[28]Chaum D.The dining cryptographers problem:Unconditional sender and recipient untraceability.Journal of Cryptology,1988,1(1):65-75.[doi:10.1007/BF00206326]
[2]Clarke EM,Emerson EA.Design and synthesis of synchronization skeletons using branching-time temporal logic.In:Proc.of the Workshop on Logics of Programs.Berlin:Springer-Verlag,1981.52-71.[doi:10.1007/978-3-540-69850-0_12]
[3]Kupferman O,Vardi MY.Module checking.In:Proc.of the 8th Int’l Conf.on Computer Aided Verification.Berlin:SpringerVerlag,1996.75-86.[doi:10.1007/3-540-61474-5_59]
[4]Muscettola N,Nayak PP,Pell B,Williams BC.Remote agent:To boldly go where no AI system has gone before.Artificial Intelligence,1998,103(1-2):5-47.[doi:10.1016/S0004-3702(98)00068-X]
[5]Alur R,Henzinger TA,Kupferman O.Alternating-Time temporal logic.Journal of the ACM,2002,49(5):672-713.[doi:10.1145/585265.585270]
[6]Schobbens P.Alternating-Time logic with imperfect recall.Electronic Notes in Theoretical Computer Science,2004,85(2):82-93.[doi:10.1016/S1571-0661(05)82604-0]
[7]Dima C,Tiplea FL.Model-Checking ATL under imperfect information and perfect recall semantics is undecidable.Co RR,abs/1102.4225,2011.
[8]Jamroga W,Dix J.Model checking abilities under incomplete information is indeed Delta2-complete.In:Proc.of the 4th European Workshop on Multi-Agent System.CEUR-WS,2006.
[9]Pilecki J,Bednarczyk MA,Jamroga W.Model checking properties of multi-agent systems with imperfect information and imperfect recall.In:Proc.of the 7th Int’l Conf.on Intelligent Systems.Berlin:Springer-Verlag,2014.415-426.[doi:10.1007/978-3-319-11313-5_37]
[10]Jamroga W.Logical Methods for Specification and Verification of Multi-Agent Systems.Warszawa:ICS PAS Publishing House,2015.
[11]Chatterjee K,Henzinger TA,Piterman N.Strategy logic.In:Proc.of the 18th Int’l Conf.on Concurrency Theory.Berlin:SpringerVerlag,2007.59-73.[doi:10.1007/978-3-540-74407-8_5]
[12]Mogavero F,Murano A,Vardi MY.Reasoning about strategies.In:Proc.of the Annual Conf.on Foundations of Software Technology and Theoretical Computer Science.Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik,2010.133-144.[doi:10.4230/LIPIcs.FSTTCS.2010.133]
[13]Mogavero F,Murano A,Vardi MY.Reasoning about strategies:On the model-checking problem.ACM Trans.on Computational Logic,2014,15(4):34:1-34:47.[doi:10.1145/2631917]
[14]Jamroga W.Some remarks on alternating temporal epistemic logic.In:Proc.of the Formal Approaches to Multi-Agent Systems.2003.133-140.
[15]Hoek W,Wooldridge M.Cooperation,knowledge,and time:Alternating-time temporal epistemic logic and its applications.Studia Logica,2003,75(1):125-157.[doi:10.1023/A:1026185103185]
[16]Lomuscio A,Raimondi F.Model checking knowledge,strategies,and games in multi-agent systems.In:Proc.of the 5th Int’l Joint Conf.on Autonomous Agents and Multiagent Systems.New York:ACM Press,2006.161-168.[doi:10.1145/1160633.1160660]
[17]Hoek W,Wooldridge M.Tractable multiagent planning for epistemic goals.In:Proc.of the 1st Int’l Joint Conf.on Autonomous Agents and Multiagent Systems.New York:ACM Press,2002.1167-1174.[doi:10.1145/545056.545095]
[18]Bulling N,Jamroga W.Alternating epistemic mu-calculus.In:Proc.of the 22nd Int’l Joint Conf.Artificial Intelligence.Austin:AAAI,2011.109-114.[doi:10.5591/978-1-57735-516-8/IJCAI11-030]
[19]Agotnes T,Goranko V,Jamroga W.Alternating-Time temporal logics with irrevocable strategies.In:Proc.of the 11th Conf.on Theoretical Aspects of Rationality and Knowledge.New York:ACM Press,2007.15-24.[doi:10.1145/1324249.1324256]
[20]Pinchinat S.A generic constructive solution for concurrent games with expressive constraints on strategies.In:Proc.of the 5th Int’l Symp.on Automated Technology for Verification and Analysis.Berlin:Springer-Verlag,2007.253-267.[doi:10.1007/978-3-540-75596-8_19]
[21]Lopes ADC,Laroussinie F,Markey N.ATL with strategy contexts:Expressiveness and model checking.In:Proc.of the IARCS Annual Conf.on Foundations of Software Technology and Theoretical Computer Science.Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik,2010.120-132.[doi:10.4230/LIPIcs.FSTTCS.2010.120]
[22]Laroussinie F,Markey N.Augmenting ATL with strategy contexts.Information and Computation,2015,245:98-123.[doi:10.1016/j.ic.2014.12.020]
[23]Goranko V,Kuusisto A,R?nnholm R.Game-Theoretic semantics for ATL+with applications to model checking.In:Proc.of the16th Conf.on Autonomous Agents and Multi Agent Systems.New York:ACM Press,2017.1277-1285.
[24]Wang F,Schewe S,Huang CH.An extension of ATL with strategy interaction.ACM Trans.on Programming Languages and Systems,2015,37(3):9:1-9:41.[doi:10.1145/2734117]
[25]Huang CH,Schewe S,Wang F.Model-Checking iterated games.Acta Informatica,2017,54(7):625-654.[doi:10.1007/s00236-016-0277-y]
[26]Lomuscio A,Qu H,Raimondi F.MCMAS:A model checker for the verification of multi-agent systems.In:Proc.of the 21st Int’l Conf.on Computer Aided Verification.Berlin:Springer-Verlag,2009.682-688.[doi:10.1007/978-3-642-02658-4_55]
[27]Lomuscio A,Qu H,Raimondi F.MCMAS:An open-source model checker for the verification of multi-agent systems.Int’l Journal on Software Tools for Technology Transfer,2017,19(1):9-30.[doi:10.1007/s10009-015-0378-x]
[28]Chaum D.The dining cryptographers problem:Unconditional sender and recipient untraceability.Journal of Cryptology,1988,1(1):65-75.[doi:10.1007/BF00206326]