Advertisement

An Algorithm Constructing the Semilinear Post for 2-Dim Reset/Transfer VASS

Extended Abstract
  • A. Finkel
  • G. Sutre
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)

Abstract

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.

Keywords

Model Check Coverability Tree Label Transition System Reachability Problem Path Scheme 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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
  2. [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
  3. [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
  4. [Fin90]
    A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144–179, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [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
  6. [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
  7. HP79]
    J. Hopcroft and J. J. Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135–159, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [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
  9. [May84]
    E. W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441–460, 1984.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • A. Finkel
    • 1
  • G. Sutre
    • 1
  1. 1.LSV, ENS Cachan & CNRS UMRFrance

Personalised recommendations