Deciding branching time properties for asynchronous programs

Asynchronous programming is a paradigm that supports asynchronous function Calls ill addition to synchronous function Calls. Programs ill such a setting call 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 all 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 call be simulated by a given finite state system; and whether the system call simulate a given finite state system. We present decision algorithms for all these problems. (C) 2009 Elsevier B.V. All rights reserved.