SAT-based Bounded Model Checking forWeighted Deontic Interpreted Systems

被引：6
|
作者：
Wozna-Szczesniak, Bozena [1 ]
机构：
[1] Jan Dlugosz Univ Czestochowa, IM & CS, Al Armii Krajowej 13-15, PL-42200 Czestochowa, Poland
来源：
FUNDAMENTA INFORMATICAE | 2016年 / 143卷 / 1-2期
关键词：
FRAGMENT;
D O I：
10.3233/FI-2016-1310
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present WECTL*KD, a weighted branching time temporal logic to specify knowledge, and correct functioning behaviour in multi-agent systems (MAS). We interpret the formulae of the logic over models generated by weighted deontic interpreted systems (WDIS). Furthermore, we investigate a SAT-based bounded model checking (BMC) technique for WDIS and for WECTL*KD.
引用
收藏
页码：173 / 205
页数：33
相关论文
共 50 条
  • [1] SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems
    Wozna-Szczesniak, Bozena
    [J]. PROGRESS IN ARTIFICIAL INTELLIGENCE, EPIA 2013, 2013, 8154 : 444 - 455
  • [2] Bounded Model Checking for Deontic Interpreted Systems
    Wozna, Bozena
    Lomuscio, Alessio
    Penczek, Wojciech
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 126 : 93 - 114
  • [3] Efficient distributed SAT and SAT-based distributed Bounded Model Checking
    Malay K. Ganai
    Aarti Gupta
    Zijiang Yang
    Pranav Ashar
    [J]. International Journal on Software Tools for Technology Transfer, 2006, 8 (4-5) : 387 - 396
  • [4] Efficient distributed SAT and SAT-based distributed bounded model checking
    Ganai, MK
    Gupta, A
    Yang, ZJ
    Ashar, P
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 334 - 347
  • [5] SAT-based bounded model checking for SE-LTL
    Zhou Conghua
    Ju Shiguang
    [J]. SNPD 2007: EIGHTH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING, AND PARALLEL/DISTRIBUTED COMPUTING, VOL 3, PROCEEDINGS, 2007, : 582 - +
  • [6] Efficient SAT-based bounded model checking for software verification
    Ivancic, Franio
    Yang, Zijiang
    Ganai, Malay K.
    Gupta, Aarti
    Ashar, Pranav
    [J]. THEORETICAL COMPUTER SCIENCE, 2008, 404 (03) : 256 - 274
  • [7] Learning from BDDs in SAT-based bounded model checking
    Gupta, A
    Ganai, M
    Chao, W
    Yang, ZJ
    Ashar, P
    [J]. 40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 824 - 829
  • [8] Evaluation of SAT-based bounded model checking of ACTL properties
    Xu, Yanyan
    Chen, Wei
    Xu, Liang
    Zhang, Wenhui
    [J]. TASE 2007: FIRST JOINT IEEE/IFIP SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, : 339 - +
  • [9] Incremental deductive & inductive reasoning for SAT-based Bounded Model Checking
    Zhang, L
    Prasad, MR
    Hsiao, MS
    [J]. ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS, 2004, : 502 - 509
  • [10] On SAT-based bounded invariant checking of blackbox designs
    Herbstritt, Marc
    Becker, Bernd
    [J]. MTV 2005: SIXTH INTERNATIONAL WORKSHOP ON MICROPRESSOR TEST AND VERIFICATION: COMMON CHALLENGES AND SOLUTIONS, PROCEEDINGS, 2006, : 23 - +
12345