Deciding branching time properties for asynchronous programs

Rohit Chadha, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review


Asynchronous programming is a paradigm that supports asynchronous function calls in addition to synchronous function calls. Programs in such a setting can be modeled by automata with counters that keep track of the number of pending asynchronous calls for each function, as well as a call stack for synchronous recursive computation. These programs have the restriction that an asynchronous call is processed only when the call stack is empty. The decidability of the control state reachability problem for such systems was recently established. In this paper, we consider the problems of checking other branching time properties for such systems. Specifically we consider the following problems - termination, which asks if there is an infinite (non-terminating) computation exhibited by the system; control state maintainability, which asks if there is a maximal execution of the system, where all the state visited lie in some "good" set; whether the system can be simulated by a given finite state system; and whether the system can simulate a given finite state system. We present decision algorithms for all these problems.

Original languageEnglish (US)
Pages (from-to)4169-4179
Number of pages11
JournalTheoretical Computer Science
Issue number42
StatePublished - Sep 28 2009


  • Asynchronous programs
  • Model checking
  • Well-structured transition systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Deciding branching time properties for asynchronous programs'. Together they form a unique fingerprint.

Cite this