License: 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.12
URN: urn:nbn:de:0030-drops-113702
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11370/
Go to the corresponding LIPIcs Volume Portal

Abuin, Alex ; Bolotov, Alexander ; Díaz de Cerio, Unai ; Hermo, Montserrat ; Lucio, Paqui

Towards Certified Model Checking for PLTL Using One-Pass Tableaux

pdf-format:
LIPIcs-TIME-2019-12.pdf (1 MB)

Abstract

The standard model checking setup analyses whether the given system specification satisfies a dedicated temporal property of the system, providing a positive answer here or a counter-example. At the same time, it is often useful to have an explicit proof that certifies the satisfiability. This is exactly what the certified model checking (CMC) has been introduced for. The paper argues that one-pass (context-based) tableau for PLTL can be efficiently used in the CMC setting, emphasising the following two advantages of this technique. First, the use of the context in which the eventualities occur, forces them to fulfil as soon as possible. Second, a dual to the tableau sequent calculus can be used to formalise the certificates. The combination of the one-pass tableau and the dual sequent calculus enables us to provide not only counter-examples for unsatisfied properties, but also proofs for satisfied properties that can be checked in a proof assistant. In addition, the construction of the tableau is enriched by an embedded solver, to which we dedicate those (propositional) computational tasks that are costly for the tableaux rules applied solely. The combination of the above techniques is particularly helpful to reason about large (system) specifications.

BibTeX - Entry

@InProceedings{abuin_et_al:LIPIcs:2019:11370,
  author =	{Alex Abuin and Alexander Bolotov and Unai D{\'\i}az de Cerio and Montserrat Hermo and Paqui Lucio},
  title =	{{Towards Certified Model Checking for PLTL Using One-Pass Tableaux}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{12:1--12:18},
  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/11370},
  URN =		{urn:nbn:de:0030-drops-113702},
  doi =		{10.4230/LIPIcs.TIME.2019.12},
  annote =	{Keywords: Temporal logic, fairness, expressiveness, linear-time, Certified model checking}
}

Keywords: Temporal logic, fairness, expressiveness, linear-time, Certified model checking
Collection: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Issue Date: 2019
Date of publication: 07.10.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI