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.CSL.2013.348
URN: urn:nbn:de:0030-drops-42072
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4207/
Go to the corresponding LIPIcs Volume Portal

Hampson, Christopher ; Kurucz, Agi

One-variable first-order linear temporal logics with counting

pdf-format:
27.pdf (0.5 MB)

Abstract

First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various timelines. However, following the introduction of the monodic formulas (where temporal operators can be applied only to subformulas with at most one free variable), there has been a renewed interest in understanding extensions of the one-variable fragment and identifying those that are decidable. Here we analyse the one-variable fragment of temporal logic extended with counting (to two), interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator 'eventually'. A more general result says that the bimodal logic of commuting linear and pseudo-equivalence relations is undecidable. The proofs are by reductions of various counter machine problems.

BibTeX - Entry

@InProceedings{hampson_et_al:LIPIcs:2013:4207,
  author =	{Christopher Hampson and Agi Kurucz},
  title =	{{One-variable first-order linear temporal logics with counting}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{348--362},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4207},
  URN =		{urn:nbn:de:0030-drops-42072},
  doi =		{10.4230/LIPIcs.CSL.2013.348},
  annote =	{Keywords: modal and temporal logic, counting, decision procedures}
}

Keywords: modal and temporal logic, counting, decision procedures
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

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