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 条

[31] Bounded model checking for timed systems
Audemard, G
Cimatti, A
Kornilowicz, A
Sebastiani, R
[J]. FORMAL TECHNIQUE FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2002, PROCEEDINGS, 2002, 2529 : 243 - 259
[32] Model Checking Weighted Integer Reset Timed Automata
Manasa, Lakshmi
Krishna, Shankara Narayanan
Jain, Chinmay
[J]. THEORY OF COMPUTING SYSTEMS, 2011, 48 (03) : 648 - 679
[33] Model Checking Prioritized Timed Systems
Lin, Shang-Wei
Hsiung, Pao-Ann
[J]. IEEE TRANSACTIONS ON COMPUTERS, 2012, 61 (06) : 843 - 856
[34] Model Checking Weighted Integer Reset Timed Automata
Lakshmi Manasa
Shankara Narayanan Krishna
Chinmay Jain
[J]. Theory of Computing Systems, 2011, 48 : 648 - 679
[35] Model checking for probabilistic timed systems
Sproston, J
[J]. VALIDATION OF STOCHASTIC SYSTEMS: A GUIDE TO CURRENT RESEARCH, 2004, 2925 : 189 - 229
[36] Model checking timed systems with priorities
Hsiung, PA
Lin, SW
[J]. 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Proceedings, 2005, : 539 - 544
[37] Bounded Model Checking for Deontic Interpreted Systems
Wozna, Bozena
Lomuscio, Alessio
Penczek, Wojciech
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 126 : 93 - 114
[38] Efficient reachability checking using sequential SAT
Parthasarathy, G
Iyer, MK
Cheng, KT
Wang, LC
[J]. ASP-DAC 2004: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2004, : 418 - 423
[39] STLMC: Robust STL Model Checking of Hybrid Systems Using SMT
Yu, Geunyeol
Lee, Jia
Bae, Kyungmin
[J]. COMPUTER AIDED VERIFICATION (CAV 2022), PT I, 2022, 13371 : 524 - 537
[40] Finding Efficient Circuits Using SAT-Solvers
Kojevnikov, Arist
Kulikov, Alexander S.
Yaroslavtsev, Grigory
[J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2009, PROCEEDINGS, 2009, 5584 : 32 - 44

← 1 2 3 4 5 →