On Lowerbounds Of VAS-like Models

The safety problem of software is becoming more and more crucial.Formal verification other than peer review and software testing can assist to find software bugs at the early stage of project development as soon as possible.By applying mathematical means to model and analyze software systems,formal verification aims to build correct systems by using strict mathematical deductions.For some software systems with highly safety requirements,formal methods even is the best verification technique.Formal verifications of these systems usually are implemented by providing the formal proofs based on abstract mathematical models of systems and the correspondence between mathematical models and verified systems.Currently,mathematical models used to model systems include finite state sets,labelled transition systems,Petri nets,vector addition systems,time automata,process algebra and so on.Concurrency theory is always one of hot research areas in theoretical computer science.Some formal models were proposed successively to model and verify concurrent systems,such as Petri nets,vector addition systems and process algebra.Although Petri nets mainly provides computation methods in physical world and vector addition systems are mostly used as formal models in concurrent programming,they were proved equivalent in mathematics.A vector addition system(VAS hereafter)consists of finite integer vectors.The configuration of VAS is a set of vectors ranging over natural numbers.Each configuration transition is an application of a vector ranging over integer numbers to current configuration and then reach another configuration.Some studies of VAS are related to reachability problem,coverability problem,etc.To empower the expression of VAS,some other models deriving from VAS were proposed,such as vector addition systems with states,recursive vector addition systems(recursive VASs hereafter),alternating vector addition systems,etc.Cai and Ogawa proposed well structured pushdown systems(WSPDSs hereafter),which combine pushdown systems with VAS so that they can model recursive multi-thread programs.WSPDSs are so expressive that VAS and extended VAS-based models can be reduced to WSPDSs,such as branching VAS and recursive VAS.Therefore,the research conclusions of WSPDSs can be directly applied to these models.The coverability problems for some VAS-extended models still keep unsolved,but one can measure the complexity of them,i.e.,given a coverability problem of a model,one can pursue an upper bound and lower bound of it and determine the complexity by reducing the gap between them.This paper proposes a general framework to get the lower bound of coverability problem for any model.This framework heavily relies on reset-0 operations,i.e.,just assign 0 to a variable no matter what the current value of it is,and uses the idea of reduction.Also,based on this framework,we verify that the lower bound of coverability problem for pushdown vector addition systems is TOWER hard,which is consistent with the result which was claimed by Lazic.Moreover,we show that for WSPDSs with three dimensional vectors as states or WSPDSs with three dimensional vectors as stack alphabet,the coverability problem becomes Ackermann hard.Meanwhile,we prove that for WSPDSs with finite states but n + 3 dimensional well quasi ordered set as stack alphabet,the coverability problem becomes Hyper-Ackermann hard.This paper presents well structured scope bounded multistack pushdown systems(WSMPDS hereafter),which limit the times of the pop operations on stacks,i.e.,a stack symbol only can be popped if it was pushed to the stack during the last k cycles(k is a fixed constant),and stack alphabet is well quasi ordered.Also,the definition of coverability problem for WSMPDS is given.By the reduction from VAS to W SM P DS,we show that the lower bound of coverability for W SM P DS is EXP SP ACE hard.