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 条

[1] Bounded model checking of software using SMT solvers instead of SAT solvers
Armando A.
Mantovani J.
Platania L.
[J]. International Journal on Software Tools for Technology Transfer, 2009, 11 (01) : 69 - 83
[2] Bounded model checking of software using SMT solvers instead of SAT solvers
Armando, A
Mantovani, J
Platania, L
[J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2006, 3925 : 146 - 162
[3] Selected Methods of Model Checking using SAT and SMT-solvers
Zbrzezny, Agnieszka M.
[J]. PROCEEDINGS OF THE 2015 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS (AAMAS'15), 2015, : 2021 - 2022
[4] Selected Methods of Model Checking Using SAT and SMT-Solvers
Zbrzezny, Agnieszka M.
[J]. TRENDS IN PRACTICAL APPLICATIONS OF AGENTS, MULTI-AGENT SYSTEMS AND SUSTAINABILITY: THE PAAMS COLLECTION, 2015, 372 : 231 - 232
[5] 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
[6] 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
[7] SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems
Wozna-Szczesniak, Bozena
[J]. PROGRESS IN ARTIFICIAL INTELLIGENCE, EPIA 2013, 2013, 8154 : 444 - 455
[8] SMT-based Bounded Model Checking for Weighted Interpreted Systems and for Weighted Epistemic ECTL
Zbrzezny, Agnieszka M.
Wozna-Szczesniak, Bozena
Zbrzezny, Andrzej
[J]. PROCEEDINGS OF THE 2015 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS (AAMAS'15), 2015, : 1671 - 1672
[9] 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
[10] 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

← 1 2 3 4 5 →