An Algorithm Constructing the Semilinear Post for 2-Dim Reset/Transfer VASS
The main result of this paper is a proof that the reachability set (post *) of any 2-dim Reset/Transfer Vector Addition System with States is an effectively computable semilinear set. Our result implies that numerous boundedness and reachability properties are decidable for this class. Since the traditional Karp and Miller’s algorithm does not terminate when applied to 2-dim Reset/Transfer VASS, we introduce, as a tool for the proof, a new technique to construct a finite coverability tree for this class.
KeywordsModel Check Coverability Tree Label Transition System Reachability Problem Path Scheme
Unable to display preview. Download preview PDF.
- [BM99]A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. In Proc. 16th Ann. Symp. Theoretical Aspects of Computer Science (STACS’99), Trier, Germany, Mar. 1999, volume 1563 of Lecture Notes in Computer Science, pages 323–333. Springer, 1999.Google Scholar
- [DFS98]C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset nets between decidability and undecidability. In Proc. 25th Int. Coll. Automata, Languages, and Programming (ICALP’98), Aalborg, Denmark, July 1998, volume 1443 of Lecture Notes in Computer Science, pages 103–115. Springer, 1998.Google Scholar
- [DJS99]C. Dufourd, P. Jančar, and Ph. Schnoebelen. Boundedness of Reset P/T nets. In Proc. 26th Int. Coll. Automata, Languages, and Programming (ICALP’99), Prague, Czech Republic, July 1999, volume 1644 of Lecture Notes in Computer Science, pages 301–310. Springer, 1999.Google Scholar
- [FS00a]A. Finkel and G. Sutre. Decidability of reachability problems for classes of two counters automata. In Proc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS’2000), Lille, France, Feb. 2000, volume 1770 of Lecture Notes in Computer Science, pages 346–357. Springer, 2000.Google Scholar
- [FS00b]A. Finkel and G. Sutre. Verification of two counters automata. Research Report LSV-2000-7, Lab. Specification and Verification, ENS de Cachan, Cachan, France, June 2000.Google Scholar
- [Kos82]S. R. Kosaraju. Decidability of reachability in vector addition systems. In Proc. 14th ACM Symp. Theory of Computing (STOC’82), San Francisco, CA, May 1982, pages 267–281, 1982.Google Scholar