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
关键词
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 条
  • [21] SAT-based unbounded symbolic model checking
    Kang, HJ
    Park, IC
    40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 840 - 843
  • [22] SAT-based unbounded symbolic model checking
    Kang, HJ
    Park, IC
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2005, 24 (02) : 129 - 140
  • [23] Certifying proofs for SAT-based model checking
    Griggio, Alberto
    Roveri, Marco
    Tonetta, Stefano
    FORMAL METHODS IN SYSTEM DESIGN, 2021, 57 (02) : 178 - 210
  • [24] Improving SAT-based Bounded Model Checking by means of BDD-based approximate traversals
    Cabodi, G
    Nocco, S
    Quer, S
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2004, 10 (12) : 1693 - 1730
  • [25] Improving SAT-based bounded model checking by means of BDD-based approximate traversals
    Cabodi, G
    Nocco, S
    Quer, S
    DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, PROCEEDINGS, 2003, : 898 - 903
  • [26] SAT-based Unbounded Model Checking of Timed Automata
    Penczek, Wojciech
    Szreter, Maciej
    FUNDAMENTA INFORMATICAE, 2008, 85 (1-4) : 425 - 440
  • [27] Simultaneous SAT-based model checking of safety properties
    Khasidashvili, Z
    Nadel, A
    Palti, A
    Hanna, Z
    HARDWARE AND SOFTWARE VERIFICATION AND TESTING, 2006, 3875 : 56 - 75
  • [28] Interpolant Learning and Reuse in SAT-Based Model Checking
    Marques-Silva, Joao
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 174 (03) : 31 - 43
  • [29] Solving Linear Arithmetic with SAT-based Model Checking
    Vizel, Yakir
    Nadel, Alexander
    Malik, Sharad
    PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 47 - 54
  • [30] Improvement of SAT-based Model Checking of Security Protocols
    Yang, Yuanyuan
    Ma, Wenping
    2009 INTERNATIONAL CONFERENCE ON E-BUSINESS AND INFORMATION SYSTEM SECURITY, VOLS 1 AND 2, 2009, : 223 - 227