Abstraction-Based Algorithm for 2QBF

被引：0
|
作者：
Janota, Mikolas [2 ]
Marques-Silva, Joao [1 ,2 ]
机构：
[1] Univ Coll Dublin, Dublin, Ireland
[2] INESC ID, Lisbon, Portugal
来源：
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2011 | 2011年 / 6695卷
关键词：
MODEL CHECKING; REFINEMENT;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Quantified Boolean Formulas (QBFs) enable standard representation of PSPACE problems. In particular, formulas with two quantifier levels (2QBFs) enable representing problems in the second level of the polynomial hierarchy (Pi(P)(2), Sigma(P)(2)). This paper proposes an algorithm for solving 2QBF satisfiability by counterexample guided abstraction refinement (CEGAR). This represents an alternative approach to 2QBF satisfiability and, by extension, to solving decision problems in the second level of polynomial hierarchy. In addition, the paper presents a comparison of a prototype implementing the presented algorithm to state of the art QBF solvers, showing that a larger set of instances is solved.
引用
收藏
页码：230 / 244
页数：15
相关论文
共 50 条
  • [21] An Abstraction-Based Data Model for Information Retrieval
    McAllister, Richard A.
    Angryk, Rafal A.
    AI 2009: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2009, 5866 : 567 - 576
  • [22] Trace Abstraction-Based Verification for Uninterpreted Programs
    Hong, Weijiang
    Chen, Zhenbang
    Du, Yide
    Wang, Ji
    FORMAL METHODS, FM 2021, 2021, 13047 : 545 - 562
  • [23] Poster: Resilient Abstraction-Based Controller Design
    Samuel, Stanly
    Mallik, Kaushik
    Schmuck, Anne-Kathrin
    Neider, Daniel
    PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC2020) (PART OF CPS-IOT WEEK), 2020,
  • [24] Towards Abstraction-based Probabilistic Program Analysis
    Szekeres, Daniel
    Majzik, Istvan
    ACTA CYBERNETICA, 2024, 26 (03): : 671 - 711
  • [25] Neural Abstraction-Based Controller Synthesis and Deployment
    Majumdar, Rupak
    Salamati, Mahmoud
    Soudjani, Sadegh
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2023, 22 (05)
  • [26] State Abstraction-based Synchronization for Thread Libraries
    Ohki, Atsuo
    Kuno, Yasushi
    INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2007, 7 (06): : 36 - 44
  • [27] Towards Abstraction-Based Verification of Shape Calculus
    Buti, F.
    De Donato, M. Callisto
    Corradini, F.
    Di Berardini, M. R.
    Merelli, E.
    Tesei, L.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 284 : 23 - 34
  • [28] Abstraction-based satisfiability solving of Presburger arithmetic
    Kroening, D
    Ouaknine, J
    Seshia, SA
    Strichman, O
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 308 - 320
  • [29] On Abstraction-Based Controller Design With Output Feedback
    Majumdar, Rupak
    Ozay, Necmiye
    Schmuck, Anne-Kathrin
    PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC2020) (PART OF CPS-IOT WEEK), 2020,
  • [30] Abstraction-based Relation Mining for Functional Test Generation
    Gent, Kelson
    Hsiao, Michael S.
    2015 IEEE 33RD VLSI TEST SYMPOSIUM (VTS), 2015,
12345