Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2019.11
URN: urn:nbn:de:0030-drops-113699
URL: https://drops.dagstuhl.de/opus/volltexte/2019/11369/
Hossain, Akash ; Laroussinie, François
From Quantified CTL to QBF
| pdf-format: |
|
Abstract
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 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 the SMT-solver Z3) on several examples.
BibTeX - Entry
@InProceedings{hossain_et_al:LIPIcs:2019:11369,
author = {Akash Hossain and Fran{\c{c}}ois Laroussinie},
title = {{From Quantified CTL to QBF}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11369},
URN = {urn:nbn:de:0030-drops-113699},
doi = {10.4230/LIPIcs.TIME.2019.11},
annote = {Keywords: Model-checking, Quantified CTL, QBF solvers, SAT based model-checking}
}
| Keywords: | Model-checking, Quantified CTL, QBF solvers, SAT based model-checking | |
| Seminar: | 26th International Symposium on Temporal Representation and Reasoning (TIME 2019) | |
| Issue date: | 2019 | |
| Date of publication: | 07.10.2019 |
