Deciding branching time properties for asynchronous programs |
| |
Authors: | Rohit Chadha Mahesh Viswanathan |
| |
Affiliation: | Department of Computer Science, University of Illinois at Urbana–Champaign, United States |
| |
Abstract: | 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. |
| |
Keywords: | Asynchronous programs Well-structured transition systems Model checking |
本文献已被 ScienceDirect 等数据库收录! |