اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدReachability in fixed dimension vector addition systems with states
72
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.
قيم البحث
اقرأ أيضاً
By adapting the iterative yardstick construction of Stockmeyer, we show that the reachability problem for vector addition systems with a stack does not have elementary complexity. As a corollary, the same lower bound holds for the satisfiability prob
lem for a two-variable first-order logic on trees in which unbounded data may label only leaf nodes. Whether the two problems are decidable remains an open question.
This paper studies tree-automatic ordinals (or equivalently, well-founded linearly ordered sets) together with the ordinal addition operation +. Informally, these are ordinals such that their elements are coded by finite trees for which the linear or
der relation of the ordinal and the ordinal addition operation can be determined by tree automata. We describe an algorithm that, given two tree-automatic ordinals with the ordinal addition operation, decides if the ordinals are isomorphic.
This paper introduces two mechanisms for computing over-approximations of sets of reachable states, with the aim of ensuring termination of state-space exploration. The first mechanism consists in over-approximating the automata representing reachabl
e sets by merging some of their states with respect to simple syntactic criteria, or a combination of such criteria. The second approximation mechanism consists in manipulating an auxiliary automaton when applying a transducer representing the transition relation to an automaton encoding the initial states. In addition, for the second mechanism we propose a new approach to refine the approximations depending on a property of interest. The proposals are evaluated on examples of mutual exclusion protocols.
It was conjectured by v{C}erny in 1964 that a synchronizing DFA on $n$ states always has a shortest synchronizing word of length at most $(n-1)^2$, and he gave a sequence of DFAs for which this bound is reached. In this paper, we investigate the ro
le of the alphabet size. For each possible alphabet size, we count DFAs on $n le 6$ states which synchronize in $(n-1)^2 - e$ steps, for all $e < 2lceil n/2 rceil$. Furthermore, we give constructions of automata with any number of states, and $3$, $4$, or $5$ symbols, which synchronize slowly, namely in $n^2 - 3n + O(1)$ steps. In addition, our results prove v{C}ernys conjecture for $n le 6$. Our computation has led to $27$ DFAs on $3$, $4$, $5$ or $6$ states, which synchronize in $(n-1)^2$ steps, but do not belong to v{C}ernys sequence. Of these $27$ DFAs, $19$ are new, and the remaining $8$ which were already known are exactly the emph{minimal} ones: they will not synchronize any more after removing a symbol. So the $19$ new DFAs are extensions of automata which were already known, including the v{C}erny automaton on $3$ states. But for $n > 3$, we prove that the v{C}erny automaton on $n$ states does not admit non-trivial extensions with the same smallest synchronizing word length $(n-1)^2$.
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. T
he central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS 2019. We establish a non-elementary lower bound, i.e. that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi and other areas, that are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the currently best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
