BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance

著录项

• 来源
  《Autonomous agents and multi-agent systems》 |2014年第4期|558-604|共47页
• 作者

  Artur Meski; Wojciech Penczek; Maciej Szreter; Bozena Wozna-Szczesniak; Andrzej Zbrzezny;

  展开▼
• 作者单位

  Institute of Computer Science, PAS, Jana Kazimierza 5.01-237 Warszawa, Poland,University of Lodz, FMCS, Banacha 22, 90-238 Lodz, Poland;

  Institute of Computer Science, PAS, Jana Kazimierza 5.01-237 Warszawa, Poland,University of Natural Sciences and Humanities, Ⅱ, Sienkiewicza 51, 08-110 Siedlce, Poland;

  Institute of Computer Science, PAS, Jana Kazimierza 5.01-237 Warszawa, Poland;

  Jan Dlugosz University, IMCS, Armii Krajowej 13/15, 42-200 Czestochowa, Poland;

  Jan Dlugosz University, IMCS, Armii Krajowej 13/15, 42-200 Czestochowa, Poland;

  展开▼
• 收录信息
• 原文格式 PDF
• 正文语种 eng
• 中图分类
• 关键词

  Bounded model checking; Binary decision diagrams; Propositional satisfiability problem (SAT); Interpreted systems; Interleaved interpreted systems; Epistemic linear temporal logic;

  机译：有界模型检查;二进制决策图;命题可满足性问题（SAT）;解释系统;交错解释系统;认知线性时间逻辑;