DocumentCode :
3650636
Title :
On the Context-Freeness Problem for Vector Addition Systems
Author :
Jérôme ;Vincent Penelle;Grégoire
Author_Institution :
LaBRI, Univ. of Bordeaux, Talence, France
fYear :
2013
Firstpage :
43
Lastpage :
52
Abstract :
Petri nets, or equivalently vector addition systems (VAS), are widely recognized as a central model for concurrent systems. Many interesting properties are decidable for this class, such as boundedness, reachability, regularity, as well as context-freeness, which is the focus of this paper. The context-freeness problem asks whether the trace language of a given VAS is context-free. This problem was shown to be decidable by Schwer in 1992, but the proof is very complex and intricate. The resulting decision procedure relies on five technical conditions over a customized coverability graph. These five conditions are shown to be necessary, but the proof that they are sufficient is only sketched. In this paper, we revisit the context-freeness problem for VAS, and give a simpler proof of decidability. Our approach is based on witnesses of non-context-freeness, that are bounded regular languages satisfying a nesting condition. As a corollary, we obtain that the trace language of a VAS is context-free if, and only if, it has a context-free intersection with every bounded regular language.
Keywords :
"Vectors","Automata","Computational modeling","Educational institutions","Labeling","Indexes","Semantics"
Publisher :
ieee
Conference_Titel :
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
ISSN :
1043-6871
Print_ISBN :
978-1-4799-0413-6
Type :
conf
DOI :
10.1109/LICS.2013.9
Filename :
6571535
Link To Document :
بازگشت