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 条
  • [41] Efficient SMT-Based Model Checking for Signal Temporal Logic
    Lee, Jia
    Yu, Geunyeol
    Bae, Kyungmin
    [J]. 2021 36TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING ASE 2021, 2021, : 343 - 354
  • [42] Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking
    Cordeiro, Lucas
    Fischer, Bernd
    [J]. 2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2011, : 331 - 340
  • [43] An SMT-based approach to satisfiability checking of MITL
    Bersani, Marcello M.
    Rossi, Matteo
    San Pietro, Pierluigi
    [J]. INFORMATION AND COMPUTATION, 2015, 245 : 72 - 97
  • [44] SMT-based Safety Checking of Parameterized Multi-Agent Systems
    Felli, Paolo
    Gianola, Alessandro
    Montali, Marco
    [J]. THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 6321 - 6330
  • [45] SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms
    Beyer, Dirk
    Dangl, Matthias
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, VSTTE 2016, 2016, 9971 : 181 - 198
  • [46] SMT-Based Symbolic Model-Checking for Operator Precedence Languages
    Chiari, Michele
    Geatti, Luca
    Gigante, Nicola
    Pradella, Matteo
    [J]. COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 387 - 408
  • [47] SAT-based Bounded Model Checking forWeighted Deontic Interpreted Systems
    Wozna-Szczesniak, Bozena
    [J]. FUNDAMENTA INFORMATICAE, 2016, 143 (1-2) : 173 - 205
  • [48] On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets
    Amat, Nicolas
    Berthomieu, Bernard
    Dal Zilio, Silvano
    [J]. APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY (PETRI NETS 2021), 2021, 12734 : 164 - 185
  • [49] Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking
    Bożena Woźna-Szcześniak
    Andrzej Zbrzezny
    [J]. Studia Logica, 2016, 104 : 641 - 678
  • [50] Simple Bounded MTLK Model Checking for Timed Interpreted Systems
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. AGENT AND MULTI-AGENT SYSTEMS: TECHNOLOGY AND APPLICATIONS, 2018, 74 : 88 - 98
12345