A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness
Jérôme Leroux, M. Praveen, Grégoire Sutre · Lecture notes in computer science · 2013
We introduce a logic for specifying trace properties of vector addition systems (VAS). This logic can express linear relations among pumping segments occurring in a trace. Given a VAS and a formula in the logic, we investigate the question whether the VAS contains a trace satisfying the formula. Our main contribution is an exponential space upper bound for this problem. The proof is based on a small model property for the logic. Compared to similar logics that are solvable in exponential space, a distinguishing feature of our logic is its ability to express non-context-freeness of the trace language of a VAS. This allows us to show that the context-freeness problem for VAS, whose complexity was not established so far, is ExpSpace -complete. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.