中文摘要：

基于无界FIFO消息队列的通信框架作为一种通用的并发系统模型，常用于事件驱动的并发程序或分布式程序建模．然而当模型包含递归过程调用时，即使仅考虑执行有限次上下文切换，其可达性问题仍是不可判定的．假定进程的消息队列约束为良序，即仅当进程的局部栈为空时才能从队列中读取消息，则其在上下文切换定界上的可达性为可判定．文中以基于队列通信的递归并发程序为对象，研究其可达性问题．首先构造能模拟递归队列并发程序执行的多栈下推系统，并提出转换方法；然后给出一种基于多栈下推系统的上下文切换定界可达算法，算法使用标准Post’操作描述下推系统的迭代，基于良序排队控制进程对队列的出队操作，穷尽地计算k次上下文切换之内的正向可达格局，并证明了构造多栈下推系统方法和上下文切换定界可达算法的正确性；最后对目标状态集合与可达格局状态集合的交集进行判空，确定目标状态是否可达，从而较好地解决此类并发程序的可达性问题．

英文摘要：

Communication frameworks based on unbounded FIFO message queues form a commonly used model for systems such as event-driven concurrent programs and distributed programs. However, even if we only consider executions with few numbers of context switches, the reach- ability problem for these concurrent systems with recursive procedure calls is still undecidable. When imposing the well-queuing constraint on all processes that each process can only read messages from its queue in case that its local stack is empty, the context-switching bounded reachability problem becomes decidable. Firstly, a method is proposed for converting concurrent programs to multi-stack pushdown systems that are capable of simulating the execution of concurrent programs with recursive queue. Secondly, a context-switching bounded reachability algorithm is proposed for multi-stack systems, which iteratively applies standard Post＂ algorithm on each pushdown system, controlling dequeue operations of current processes by the well-aueuingconstrain, and then exhaustively computes the forward reachable configurations via executions with at most k context switches. The correctness of both the convertion method and context- switching bounded algorithm is shown in the paper. Finally the reachability problem for recursive queue concurrent programs is solved by checking emptiness of intersection of the target states set and the reachable configurations set.