Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers

被引：4

作者：

Zbrzezny, Agnieszka M. ^{[1
]}

Zbrzezny, Andrzej ^{[1
]}

Raimondi, Franco ^{[2
]}

机构：

[1] Jan Dlugosz Univ, IMCS, Al Armii Krajowej 13-15, P-42200 Czestochowa, Poland

[2] Middlesex Univ, Sch Sci & Technol, London, England

来源：

AGENT AND MULTI-AGENT SYSTEMS: TECHNOLOGY AND APPLICATIONS, KES-AMSTA 2016 | 2016年 / 58卷

关键词：

D O I：

10.1007/978-3-319-39883-9_4

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In this paper we define Satisfiability Modulo Theory based (SMT-based) and SAT-based bounded model checking (BMC) methods for the existential fragment of Weighted Epistemic Linear Time Logic (WLTLK) interpreted on Timed Weighted Interpreted Systems (TWISs). We provide an implementation based on Z3 and PicoSAT solvers and we present a comparison of the two methods on common instances that can be scaled up to for performance evaluation. A detailed analysis of results shows that in many instances the SMT-based approach can be significantly faster than the SAT-based approach.

引用

页码：45 / 55

页数：11

共 50 条

[41] SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata
Malinowski, Janusz
Niebert, Peter
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 405 - 419
[42] Model Checking Using SMT and Theory of Lists
Milicevic, Aleksandar
Kugler, Hillel
[J]. NASA FORMAL METHODS, 2011, 6617 : 282 - +
[43] Unbounded Data Model Verication Using SMT Solvers
Nijjar, Jaideep
Bultan, Tevfik
[J]. 2012 PROCEEDINGS OF THE 27TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2012, : 210 - 219
[44] 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
[45] 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
[46] Logic and Model Checking by Imprecise Probabilistic Interpreted Systems
Termine, Alberto
Antonucci, Alessandro
Primiero, Giuseppe
Facchini, Alessandro
[J]. MULTI-AGENT SYSTEMS, EUMAS 2021, 2021, 12802 : 211 - 227
[47] 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
[48] Model checking epistemic-probabilistic logic using probabilistic interpreted systems
Wan, Wei
Bentahar, Jamal
Ben Hamza, Abdessamad
[J]. KNOWLEDGE-BASED SYSTEMS, 2013, 50 : 279 - 295
[49] Efficient encoding for bounded model checking of timed automata
Chen, Zuxi
Xu, Zhongwei
Du, Junwei
Mei, Meng
Guo, Jing
[J]. IEEJ TRANSACTIONS ON ELECTRICAL AND ELECTRONIC ENGINEERING, 2017, 12 (05) : 710 - 720
[50] Guaranteeing Timed Opacity using Parametric Timed Model Checking
Andre, Etienne
Lime, Didier
Marinho, Dylan
Sun, Jun
[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2022, 31 (04)

← 1 2 3 4 5 →