SMT-based Bounded Model Checking for Weighted Interpreted Systems and for Weighted Epistemic ECTL

被引：0
|
作者：
Zbrzezny, Agnieszka M. [1 ]
Wozna-Szczesniak, Bozena [1 ]
Zbrzezny, Andrzej [1 ]
机构：
[1] Jan Dlugosz Univ Czestochowa, IMCS, Al Armii Krajowej 13-15, PL-42200 Czestochowa, Poland
来源：
PROCEEDINGS OF THE 2015 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS (AAMAS'15) | 2015年
关键词：
Bounded model checking; SMT; SAT; Weighted Interpreted Systems; Weighted Epistemic Computation Tree Logic;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We define the SMT-based bounded model checking (BMC) method for Weighted Interpreted Systems and for the existential fragment of the Weighted Epistemic Computation Tree Logic. We implemented the new BMC algorithm and compared it with the SAT-based BMC method for the same systems and the same property language on several benchmarks for multi-agent systems.
引用
收藏
页码：1671 / 1672
页数：2
相关论文
共 50 条
  • [1] SMT-Based Bounded Model Checking for Weighted Epistemic ECTL
    Zbrzezny, Agnieszka M.
    Wozna-Szczesniak, Bozena
    Zbrzezny, Andrzej
    [J]. PROGRESS IN ARTIFICIAL INTELLIGENCE-BK, 2015, 9273 : 651 - 657
  • [2] Checking WELTLK Properties of Weighted Interpreted Systems via SMT-Based Bounded Model Checking
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. PRIMA 2015: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2015, 9387 : 660 - 669
  • [3] Checking WECTLK Properties of Timed Real-Weighted Interpreted Systems via SMT-Based Bounded Model Checking
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. PROGRESS IN ARTIFICIAL INTELLIGENCE-BK, 2015, 9273 : 638 - 650
  • [4] Simple SMT-Based Bounded Model Checking for Timed Interpreted Systems
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. ROUGH SETS, IJCRS 2017, PT II, 2017, 10314 : 487 - 504
  • [5] Bounded Model Checking for Weighted Interpreted Systems and for Flat Weighted Epistemic Computation Tree Logic
    Wozna-Szczesniak, Bozena
    Szczesniak, Ireneusz
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. PRIMA 2014: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2014, 8861 : 107 - 115
  • [6] SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems
    Wozna-Szczesniak, Bozena
    [J]. PROGRESS IN ARTIFICIAL INTELLIGENCE, EPIA 2013, 2013, 8154 : 444 - 455
  • [7] SMT-based Bounded Model Checking for Real-time Systems
    Xu, Liang
    [J]. QSIC 2008: PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2008, : 120 - 125
  • [8] Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    Raimondi, Franco
    [J]. AGENT AND MULTI-AGENT SYSTEMS: TECHNOLOGY AND APPLICATIONS, KES-AMSTA 2016, 2016, 58 : 45 - 55
  • [9] Checking RTECTL Properties of STSs via SMT-Based Bounded Model Checking
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. DISTRIBUTED COMPUTING AND ARTIFICIAL INTELLIGENCE, 12TH INTERNATIONAL CONFERENCE, 2015, 373 : 55 - 62
  • [10] SMT-based Bounded Model Checking for OSEK/VDX Applications
    Zhang, Haitao
    Aoki, Toshiaki
    Lin, Hsin-Hung
    Zhang, Min
    Chiba, Yuki
    Yatake, Kenro
    [J]. 2013 20TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2013), VOL 1, 2013, : 307 - 314
12345