ADJACENT ORDERED MULTI-PUSHDOWN SYSTEMS

被引:7
作者
Atig, Mohamed Faouzi [1 ]
Kumar, K. Narayan [2 ]
Shivasan, Prakash [2 ]
机构
[1] Uppsala Univ, Uppsala, Sweden
[2] Chennai Math Inst, Madras, Tamil Nadu, India
关键词
Concurrent pushdown systems; reachability problem; LTL model-checking; recursive Boolean programs; REACHABILITY ANALYSIS; MODEL CHECKING; EMPTINESS; PROGRAMS;
D O I
10.1142/S0129054114400255
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:1083 / 1096
页数:14
相关论文
共 26 条
[1]  
[Anonymous], 1986, P 1 S LOG COMP SCI L
[2]  
[Anonymous], 1996, INT J FOUND COMPUT S, DOI DOI 10.1142/S0129054196000191
[3]  
Atig Mohamed Faouzi, 2013, Developments in Language Theory. 17th International Conference, DLT 2013. Proceedings: LNCS 7907, P58, DOI 10.1007/978-3-642-38771-5_7
[4]  
Atig Mohamed Faouzi, 2012, Automated Technology for Verification and Analysis. Proceedings of the 10th International Symposium, ATVA 2012, P152, DOI 10.1007/978-3-642-33386-6_13
[5]  
Atig Mohamed Faouzi, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P210, DOI 10.1007/978-3-642-31424-7_19
[6]  
Atig MF, 2008, LECT NOTES COMPUT SC, V5257, P121, DOI 10.1007/978-3-540-85780-8_9
[7]   Global Model Checking of Ordered Multi-Pushdown Systems [J].
Atig, Mohamed Faouzi .
IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2010), 2010, 8 :216-227
[8]  
Bollig B, 2011, LECT NOTES COMPUT SC, V6907, P132, DOI 10.1007/978-3-642-22993-0_15
[9]  
Bouajjani A, 2005, LECT NOTES COMPUT SC, V3821, P348, DOI 10.1007/11590156_28
[10]  
Bouajjani A, 2007, LECT NOTES COMPUT SC, V4590, P207