微信服务号

微信订阅号

2025-4-3- 20
Home > Archive>Volume 29, Issue 10, 2018 >3009-3020. DOI:10.13328/j.cnki.jos.005321
PDF HTML XML Export Cite reminder
Lower Bound for Coverability Problem of Well-Structured Pushdown Systems
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61472238, 61672340, 61472240, 61872232)

  • Article
    • | |
  • Metrics
    • |
  • Reference [23]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Well-Structured pushdown systems (WSPDSs) combine pushdown systems and well-structured transition systems to allow locations and stack alphabets to be vectors, and thus they are unbounded. States change with the push and pop operations on the stack. The model has been said to be "very close to the border of undecidability". This paper proposes a general framework to get the lower bounds for coverability complexity of a model by adopting the reset-zero method. The paper proves that the complexity is Tower-hard when a WSPDS is restricted with three dimensional state vectors, and Hyper-Ackermann hard for the general WSPDSs.

    Reference
    [1] Derick WD. Theory of Computation:A Primer. Boston:Addison-Wesley Longman Publishing Co., 1987.
    [2] Autebert JM, Berstel J, Boasson L. Context-Free languages and pushdown automata. Handbook of Formal Languages, 1997,6(3):111-174.[doi:10.1007/978-3-642-59136-5_3]
    [3] Abdulla PA, Čerāns K, Jonsson B, Tsay YK. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 2000,160(1-2):109-127.[doi:10.1006/inco.1999.2843]
    [4] Cai X, Ogawa M. Well-Structured pushdown systems. In:D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin:Springer-Verlag, 2013. 121-136.[doi:10.1007/978-3-642-40184-8_10]
    [5] Jin Y, Cai XJ, Li GQ. Expressiveness of well-structured pushdown systems. Journal of Shanghai Jiaotong University, 2015,49(8):1084-1089(in Chinese with English abstract).[doi:10.16183/j.cnki.jsjtu.2015.08.002]
    [6] Leroux J, Praveen M, Sutre G. Hyper-Ackermannian bounds for pushdown vector addition systems. In:Henzinger T, Miller D, eds. Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). New York:ACM, 2014. Article 63.[doi:10.1145/2603088.2603146]
    [7] Sen K, Viswanathan M. Model checking multithreaded programs with asynchronous atomic methods. In:Ball T, Jones RB, eds. Proc. of the Int'l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2006. 300-314.[doi:10.1007/11817963_29]
    [8] Kochems J, Luke Ong CH. Safety verification of asynchronous pushdown systems with shaped stacks. In:D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin:Springer-Verlag, 2013. 288-302.[doi:10.1007/978-3-642-40184-8_21]
    [9] Bouajjani A, Emmi M. Analysis of recursively parallel programs. In:Field J, ed. Proc. of the 39th Annual ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. New York:ACM, 2012. 203-214.[doi:10.1145/2103621.2103681]
    [10] Lipton RJ. The reachability problem requires exponential space[Ph.D. Thesis]. Department of Computer Science, Yale University, 1976.
    [11] Lazic R. The reachability problem for vector addition systems with a stack is not elementary. Computer Science, 2013.
    [12] Schnoebelen P. Revisiting Ackermann-Hardness for lossy counter machines and reset Petri nets. Lecture Notes in Computer Science, 2010,6281:616-628.[doi:10.1007/978-3-642-15155-2_54]
    [13] Haddad S, Schmitz S, Schnoebelen P. The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In:Logic in Computer Science. IEEE, 2012. 355-364.[doi:10.1109/LICS.2012.46]
    [14] Demri S, Jurdziński M, Lachish O, Lazić R. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 2013,79(1):23-38.[doi:10.1016/j.jcss.2012.04.002]
    [15] Lazić R. The reachability problem for branching vector addition systems requires doubly-exponential space. Information Processing Letters, 2010,110(17):740-745.[doi:10.1016/j.ipl.2010.06.008]
    [16] Bonnet R. The reachability problem for vector addition system with one zero-test. In:Murlak F, Sankowski P, eds. Mathematical Foundations of Computer Science. Berlin:Springer-Verlag, 2011. 145-157.[doi:10.1007/978-3-642-22993-0_16]
    [17] Lincoln P, Mitchell J, Scedrov A, Shankar N. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 1992,56(1-3):239-311.[doi:10.1016/0168-0072(92)90075-B]
    [18] Kanovich MI. Petri nets, Horn programs, linear logic, and vector games. Annals of Pure and Applied Logic, 1995,75(1-2):107-135.[doi:10.1016/0168-0072(94)00060-G]
    [19] Raskin JF, Samuelides M, Begin LV. Games for counting abstractions. Electronic Notes in Theoretical Computer Science, 2005,128(6):69-85.[doi:10.1016/j.entcs.2005.04.005]
    [20] Urquhart A. The complexity of decision procedures in relevance logic Ⅱ. The Journal of Symbolic Logic, 1999,64(4):1774-1802.[doi:10.2307/2586811]
    [21] Cantor G. Ueber unendliche, lineare Punktmannichfaltigkeiten. Mathematische Annalen, 1883,21(4):545-591.[doi:10.1007/BF01446819]
    [22] Minsky ML. Computation:Finite and Infinite Machines. Prentice-Hall, Inc., 1967.
    [23] Schmitz S, Schnoebelen P. The power of well-structured systems. In:D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin:Springer-Verlag, 2013. 5-24.[doi:10.1007/978-3-642-40184-8_2]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李春淼,蔡小娟,李国强.良结构下推系统的可覆盖性问题的下界.软件学报,2018,29(10):3009-3020

Copy
Share
Article Metrics
  • Abstract:3374
  • PDF: 3904
  • HTML: 1940
  • Cited by: 0
History
  • Received:February 18,2017
  • Revised:May 09,2017
  • Online: March 14,2018
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2032443Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063