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.2020.14
URN: urn:nbn:de:0030-drops-129824
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12982/
Go to the corresponding LIPIcs Volume Portal

Abuin, Alex ; Bolotov, Alexander ; Hermo, Montserrat ; Lucio, Paqui

One-Pass Context-Based Tableaux Systems for CTL and ECTL

pdf-format:
LIPIcs-TIME-2020-14.pdf (0.7 MB)

Abstract

When building tableau for temporal logic formulae, applying a two-pass construction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second "pass", we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtaining a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics.

BibTeX - Entry

@InProceedings{abuin_et_al:LIPIcs:2020:12982,
  author =	{Alex Abuin and Alexander Bolotov and Montserrat Hermo and Paqui Lucio},
  title =	{{One-Pass Context-Based Tableaux Systems for CTL and ECTL}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Emilio Mu{\~n}oz-Velasco and Ana Ozaki and Martin Theobald},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12982},
  URN =		{urn:nbn:de:0030-drops-129824},
  doi =		{10.4230/LIPIcs.TIME.2020.14},
  annote =	{Keywords: Temporal logic, fairness, expressiveness, branching-time}
}

Keywords: Temporal logic, fairness, expressiveness, branching-time
Collection: 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)
Issue Date: 2020
Date of publication: 15.09.2020

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