DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2019.11

From Quantified CTL to QBF

Authors: Akash Hossain and François Laroussinie

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.

Cite as

Akash Hossain and François Laroussinie. From Quantified CTL to QBF. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{hossain_et_al:LIPIcs.TIME.2019.11,
  author =	{Hossain, Akash and Laroussinie, Fran\c{c}ois},
  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 =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.11},
  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}
}

Search Results

Documents authored by Hossain, Akash

From Quantified CTL to QBF

Abstract

Cite as

Thanks for your feedback!

Could not send message