ADJACENT ORDERED MULTI-PUSHDOWN SYSTEMS

作者：Atig Mohamed Faouzi^*; Kumar K Narayan; Shivasan Prakash

来源：International Journal of Foundations of Computer Science, 2014, 25(8): 1083-1096.

DOI：10.1142/S0129054114400255

• Concurrent pushdown systems
• reachability problem
• LTL model-checking
• recursive Boolean programs

Multi-pushdown systems are formal models of multi-threaded programs. As they are Turing powerful in their full generality, several decidable subclasses, constituting under-approximations of the original system, have been studied in the recent years. Ordered Multi-Pushdown Systems (OMPDSs) impose an order on the stacks and limit pop actions to the lowest non-empty stack. The control state reachability for OMPDSs is 2-ETIME-COMPLETE. We propose a restriction on OMPDSs, called Adjacent OMPDSs (AOMPDS), where values may be pushed only on the lowest non-empty stack or one of its two neighbours. We describe EXPTIME decision procedures for reachability and LTL model-checking and establish matching lower bounds. We demonstrate the utility of this model as an algorithmic tool via optimal reductions from other models.

• 出版日期2014-12