Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
CTL with finitely bounded semantics
Stockholm University, Faculty of Humanities, Department of Philosophy.ORCID iD: 0000-0002-0157-1644
University of Bremen, Germany.
University of Tampere, Finland.
2017 (English)In: Proceedings of the 24th International Symposium on Temporal Representation and Reasoning (TIME'2017) / [ed] Sven Schewe, Thomas Schneider, Jef Wijsen, Schloss Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2017, p. 14:1-14:19Conference paper, Published paper (Refereed)
Abstract [en]

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 oftruth of an eventuality must commit to a time limit (number of transition steps) within which theformula should become true on all (resp. some) paths starting from the state where the formulais evaluated. The resulting version CTL_FB of CTL differs essentially from the standard one asit 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 allowingexplicit indication of time limits in formulae. We prove soundness and completeness of bothsystems and also show that the latter tableaux system provides an EXPTIME decision procedurefor it and thus prove EXPTIME-completeness of the satisfiability problem.

Place, publisher, year, edition, pages
Schloss Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2017. p. 14:1-14:19
Series
Leibniz International Proceedings in Informatics (LIPIcs), ISSN ISSN 1868-8969 ; 90
Keywords [en]
CTL, finitely bounded semantics, tableaux, decidability
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:su:diva-152853DOI: 10.4230/LIPIcs.TIME.2017.14ISBN: 978-3-95977-052-1 (print)OAI: oai:DiVA.org:su-152853DiVA, id: diva2:1181537
Conference
24th International Symposium on Temporal Representation and Reasoning (TIME'2017)
Funder
Swedish Research Council, 2015-04388Available from: 2018-02-08 Created: 2018-02-08 Last updated: 2018-03-14Bibliographically approved

Open Access in DiVA

CTL with finitely bounded semantics(1530 kB)3 downloads
File information
File name FULLTEXT01.pdfFile size 1530 kBChecksum SHA-512
81ed5186152d4875609f498225e349b19bf4f972028912872da78d62404d3bbf4146394a25e0db9dcfe6876141e55d23131f986e905ceea108d049ee809b07f6
Type fulltextMimetype application/pdf

Other links

Publisher's full texthttp://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7932

Search in DiVA

By author/editor
Goranko, Valentin
By organisation
Department of Philosophy
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 3 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 12 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf