DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2017.14

CTL with Finitely Bounded Semantics

Authors: Valentin Goranko, Antti Kuusisto, and Raine Rönnholm

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

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.

Cite as

Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. CTL with Finitely Bounded Semantics. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{goranko_et_al:LIPIcs.TIME.2017.14,
  author =	{Goranko, Valentin and Kuusisto, Antti and R\"{o}nnholm, Raine},
  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 =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.14},
  URN =		{urn:nbn:de:0030-drops-79325},
  doi =		{10.4230/LIPIcs.TIME.2017.14},
  annote =	{Keywords: CTL, finitely bounded semantics, tableaux, decidability}
}

Search Results

Documents authored by Rönnholm, Raine

CTL with Finitely Bounded Semantics

Abstract

Cite as

Thanks for your feedback!

Could not send message