Implementation of Epistemic Operators for Model Checking Multi-agent Systems
作者： Marina Bagić Babac , Marijan Kunštić
DOI: 10.1007/978-3-642-04441-0_19
关键词:
摘要: The problem of multi-agent system (MAS) specification and verification has been introduced in this paper, Epistemic transition (ETS) represents an agent as the smallest unit a system, while synchronous product (ESP) formal model for system. Therefore, framework epistemic properties systems provided. A special extension Action computation tree logic with unless operator reasoning (ACTLW-ER) is used MAS checking. operators ACTLW-ER are implemented by symbolic checking algorithms using binary decision diagrams.
springer.com
sci-hub.st 参考文章(10)
A. Lomuscio, S. Edelkamp, Model Checking and Artificial Intelligence ,(2008)
Tatjana Kapus, Zmago Brezo, Robert Meolic, VERIFICATION OF CONCURRENT SYSTEMS USING ACTL ,(2000)
Robin Milner, Communication and Concurrency ,(1989)
Michael Huth, Mark Ryan, Logic in Computer Science Cambridge University Press. ,(2004) , 10.1017/CBO9780511810275
Charles Pecheur, Franco Raimondi, Symbolic Model Checking of Logics with Actions Model Checking and Artificial Intelligence. pp. 113- 128 ,(2007) , 10.1007/978-3-540-74128-2_8
Marina Bagic, Marijan Kun!stic, Verification of Intelligent Agents with ACTL for Epistemic Reasoning computational intelligence for modelling, control and automation. pp. 62- 62 ,(2006) , 10.1109/CIMCA.2006.229
A. Fantechi, S. Gnesi, A. Maggiore, Enhancing Test Coverage by Back-tracing Model-checker Counterexamples Electronic Notes in Theoretical Computer Science. ,vol. 116, pp. 199- 211 ,(2005) , 10.1016/J.ENTCS.2004.02.077
Bernd-Holger Schlingloff, Edmund M. Clarke, Model Checking ,(1999)
Edmund M. Clarke, Bernd-Holger Schlingloff, Chapter 24 – Model Checking Handbook of Automated Reasoning. pp. 1635- 1790 ,(2001) , 10.1016/B978-044450813-3/50026-6
Joseph Y. Halpern, Moshe Y. Vardi, Yoram Moses, Ronald Fagin, Reasoning About Knowledge MIT Press Books. ,vol. 1, ,(2003)