Complexity Analysis of the Backward Coverability Algorithm for VASS

1. Abdulla, P., Čerāns, K., Jonsson, B., Tsay, Y.: General Decidability Theorems for Infinite-State Systems. In: LICS 1996, pp. 313–321. IEEE Computer Society Press, Los Alamitos (1996)

   Google Scholar 

2. Arnold, A., Latteux, M.: Recursivite et cones rationnels fermes par intersection. Calcolo 15, 381–394 (1978)

   Article  MathSciNet  MATH  Google Scholar 

3. Delzanno, G., Raskin, J.-F.: Symbolic representation of upward-closed sets. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 426–440. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

4. Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 298–310. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

5. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics 35, 413–422 (1913)

   Article  MathSciNet  MATH  Google Scholar 

6. Esparza, J.: Decidability and Complexity of Petri Net Problems - An Introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998)

   Chapter  Google Scholar 

7. Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics 30(3), 143–160 (1994)

   MATH  Google Scholar 

8. Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s lemma. In: LICS 2011: Proc. 26th Annual IEEE Symp. on Logic in Computer Science, pp. 269–278. IEEE Computer Society Press, Los Alamitos (2011)

   Chapter  Google Scholar 

9. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)

   Article  MathSciNet  MATH  Google Scholar 

10. Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. CoRR, abs/1011.0551 (2010)

    Google Scholar 

11. Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society (3) 2(7), 326–336 (1952)

    Article  MathSciNet  MATH  Google Scholar 

12. Karp, R.M., Miller, R.E.: Parallel program schemata. Journal of Comput. Syst. Sci. 3(2), 147–195 (1969)

    Article  MathSciNet  MATH  Google Scholar 

13. Lipton, R.: The Reachability Problem Requires Exponential Space. Technical Report 62, Yale University (1976)

    Google Scholar 

14. Rackoff, C.: The Covering and Boundedness Problems for Vector Addition Systems. Theoretical Computer Science 6, 223–231 (1978)

    Article  MathSciNet  MATH  Google Scholar 

15. Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 300–314. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

16. Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability problems in Petri nets. Acta Informatica 21, 643–674 (1985)

    Article  MathSciNet  MATH  Google Scholar 

17. Yen, H.-C., Chen, C.-L.: On minimal elements of upward-closed sets. Theoretical Computer Science 410(24-25), 2442–2452 (2009)

    Article  MathSciNet  MATH  Google Scholar 

Download references