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.2017.14
URN: urn:nbn:de:0030-drops-79325
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7932/
Go to the corresponding LIPIcs Volume Portal

Goranko, Valentin ; Kuusisto, Antti ; Rönnholm, Raine

CTL with Finitely Bounded Semantics

pdf-format:
LIPIcs-TIME-2017-14.pdf (0.6 MB)

Abstract

We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property.

We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.

BibTeX - Entry

@InProceedings{goranko_et_al:LIPIcs:2017:7932,
  author =	{Valentin Goranko and Antti Kuusisto and Raine R{\"o}nnholm},
  title =	{{CTL with Finitely Bounded Semantics}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Sven Schewe and Thomas Schneider and Jef Wijsen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7932},
  URN =		{urn:nbn:de:0030-drops-79325},
  doi =		{10.4230/LIPIcs.TIME.2017.14},
  annote =	{Keywords: CTL, finitely bounded semantics, tableaux, decidability}
}

Keywords: CTL, finitely bounded semantics, tableaux, decidability
Collection: 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)
Issue Date: 2017
Date of publication: 25.09.2017

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