QCTL model-checking with QBF solvers

被引：2
|
作者：
Hossain, Akash [1 ]
Laroussinie, Francois [1 ]
机构：
[1] Univ Paris Diderot, IRIF, Case 7024, F-75205 Paris 13, France
来源：
INFORMATION AND COMPUTATION | 2021年 / 280卷
关键词：
Model-checking; Temporal Logics; Quantified CTL; QBF solvers; LOGICS;
D O I：
10.1016/j.ic.2020.104642
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Quantified CTL (QCTL) extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a new model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies and we compare them with a prototype (based on several QBF solvers) on different examples. (C) 2020 Elsevier Inc. All rights reserved.
引用
收藏
页数：19
相关论文
共 50 条
  • [31] Foundations of incremental aspect model-checking
    Krishnamurthi, Shriram
    Fisler, Kathi
    [J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (02)
  • [32] Model-checking TRIO specifications in SPIN
    Morzenti, A
    Pradella, M
    San Pietro, P
    Spoletini, P
    [J]. FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
  • [33] A Model-Checking Tool for Families of Services
    Asirelli, Patrizia
    ter Beek, Maurice H.
    Fantechi, Alessandro
    Gnesi, Stefania
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, 2011, 6722 : 44 - 58
  • [34] Model-checking access control policies
    Guelev, DP
    Ryan, M
    Schobbens, PY
    [J]. INFORMATION SECURITY, PROCEEDINGS, 2004, 3225 : 219 - 230
  • [35] On complexity of model-checking for the TQL logic
    Boneva, I
    Talbot, JM
    [J]. EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, 2004, 155 : 381 - 394
  • [36] Understanding SIP through Model-Checking
    Zave, Pamela
    [J]. PRINCIPLES, SYSTEMS AND APPLICATIONS OF IP TELECOMMUNICATIONS, 2008, 5310 : 256 - 279
  • [37] On Model-Checking Optimistic Replication Algorithms
    Boucheneb, Hanifa
    Imine, Abdessamad
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 73 - +
  • [38] Symbolic model-checking for biochemical systems
    Fages, F
    [J]. LOGIC PROGRAMMING, PROCEEDINGS, 2003, 2916 : 102 - 102
  • [39] LTL Model-Checking for Malware Detection
    Song, Fu
    Touili, Tayssir
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 416 - 431
  • [40] Towards Model-Checking Programs with Lists
    Finkel, Alain
    Lozes, Etienne
    Sangnier, Arnaud
    [J]. INFINITY IN LOGIC AND COMPUTATION, 2009, 5489 : 56 - 86
12345