The language theory of bounded context-switching

Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato

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


Concurrent compositions of recursive programs with finite data are a natural abstraction model for concurrent programs. Since reachability is undecidable for this class, a restricted form of reachability has become popular in the formal verification literature, where the set of states reached within k context-switches, for a fixed small constant k, is explored. In this paper, we consider the language theory of these models: concurrent recursive programs with finite data domains that communicate using shared memory and work within k round-robin rounds of context-switches, and where further the stack operations are made visible (as in visibly pushdown automata). We show that the corresponding class of languages, for any fixed k, forms a robust subclass of context-sensitive languages, closed under all the Boolean operations. Our main technical contribution is to show that these automata are determinizable as well. This is the first class we are aware of that includes non-context-free languages, and yet has the above properties.

Original languageEnglish (US)
Title of host publicationLATIN 2010
Subtitle of host publicationTheoretical Informatics - 9th Latin American Symposium, Proceedings
Number of pages12
StatePublished - 2010
Event9th Latin American Theoretical Informatics Symposium, LATIN 2010 - Oaxaca, Mexico
Duration: Apr 19 2010Apr 23 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6034 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th Latin American Theoretical Informatics Symposium, LATIN 2010

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'The language theory of bounded context-switching'. Together they form a unique fingerprint.

Cite this