The tree width of auxiliary storage

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose a generalization of results on the decidability of emptiness for several restricted classes of sequential and distributed automata with auxiliary storage (stacks, queues) that have recently been proved. Our generalization relies on reducing emptiness of these automata to finite-state graph automata (without storage) restricted to monadic second-order (MSO) definable graphs of bounded tree-width, where the graph structure encodes the mechanism provided by the auxiliary storage. Our results outline a uniform mechanism to derive emptiness algorithms for automata, explaining and simplifying several existing results, as well as proving new decidability results.

Original languageEnglish (US)
Title of host publicationPOPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages283-294
Number of pages12
DOIs
StatePublished - 2010
Event38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11 - Austin, TX, United States
Duration: Jan 26 2011Jan 28 2011

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Conference

Conference38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
Country/TerritoryUnited States
CityAustin, TX
Period1/26/111/28/11

Keywords

  • Automata
  • Bounded tree-width
  • Decision procedures
  • Model checking

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'The tree width of auxiliary storage'. Together they form a unique fingerprint.

Cite this