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.FSTTCS.2016.20
URN: urn:nbn:de:0030-drops-68554
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6855/
Go to the corresponding LIPIcs Volume Portal

Bollig, Benedikt

One-Counter Automata with Counter Observability

pdf-format:
LIPIcs-FSTTCS-2016-20.pdf (0.5 MB)

Abstract

In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.

BibTeX - Entry

@InProceedings{bollig:LIPIcs:2016:6855,
  author =	{Benedikt Bollig},
  title =	{{One-Counter Automata with Counter Observability}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{20:1--20:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6855},
  URN =		{urn:nbn:de:0030-drops-68554},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.20},
  annote =	{Keywords: One-counter automata, inclusion checking, observability, visibly one- counter automata, strong automata}
}

Keywords: One-counter automata, inclusion checking, observability, visibly one- counter automata, strong automata
Collection: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Issue Date: 2016
Date of publication: 10.12.2016

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