New Complexity Results for Some Linear Counting Problems Using Minimal Solutions to Linear Diophantine Equations

Extended Abstract
  • Gaoyan Xie
  • Cheng Li
  • Zhe Dang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2759)


The linear reachability problem is to decide whether there is an execution path in a given finite state transition system such that the counts of labels on the path satisfy a given linear constraint. Using results on minimal solutions (in nonnegative integers) for linear Diophantine systems, we obtain new complexity results for the problem, as well as for other linear counting problems of finite state transition systems and timed automata. In contrast to previously known results, the complexity bounds obtained in this paper are polynomial in the size of the transition system in consideration, when the linear constraint is fixed.


Nonnegative Integer Linear Constraint Minimal Solution Linear Temporal Logic Execution Path 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, April 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. [2]
    R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–204, January 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  3. [3]
    A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS’99, volume 1579 of LNCS, pages 193–207. Springer-Verlag, 1999.Google Scholar
  4. [4]
    I. Borosh, M. Flahive, and B. Treybig. Small solutions of linear diophantine equations. Discrete Mathematics, 58:215–220, 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [5]
    I. Borosh and B. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55:299–304, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In LICS’95, pages 123–133. IEEE CS Press, 1995.Google Scholar
  7. [7]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS, 8(2):244–263, 1986.zbMATHCrossRefGoogle Scholar
  8. [8]
    H. Comon and Y. Jurski. Timed automata and the theory of real numbers. In CONCUR’99, volume 1664 of LNCS, pages 242–257. Springer, 1999.Google Scholar
  9. [9]
    Zhe Dang. Binary reachability analysis of pushdown timed automata with dense clocks. In CAV’01, volume 2102 of LNCS, pages 506–517. Springer, 2001.Google Scholar
  10. [10]
    Zhe Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. In CAV’00, volume 1855 of LNCS, pages 69–84. Springer, 2000.Google Scholar
  11. [11]
    Zhe Dang, O. H. Ibarra, and P. San Pietro. Liveness Verification of Reversal-bounded Multicounter Machines with a Free Counter. In FSTTCS’01, volume 2245 of LNCS, pages 132–143. Springer, 2001.Google Scholar
  12. [12]
    Zhe Dang, P. San Pietro, and R. A. Kemmerer. On Presburger Liveness of Discrete Timed Automata. In STACS’01, volume 2010 of LNCS, pages 132–143. Springer, 2001.Google Scholar
  13. [13]
    E. Domenjoud. Solving systems of linear diophantine equations: an algebraic approach. In MFCS’91, volume 520 of LNCS, pages 141–150. Springer-Verlag, 1991.Google Scholar
  14. [14]
    Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In ICSE’99, pages 411–421. ACM Press, 1999.Google Scholar
  15. [15]
    G. J. Holzmann. The model checker SPIN. TSE, 23(5):279–295, May 1997.MathSciNetGoogle Scholar
  16. [16]
    J. Hopcroft and J. Ullman. Introduction to Automata theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979.Google Scholar
  17. [17]
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.zbMATHGoogle Scholar
  18. [18]
    Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, 1989.CrossRefGoogle Scholar
  19. [19]
    R. Parikh. On context-free languages. JACM, 13:570–581, 1966.zbMATHCrossRefMathSciNetGoogle Scholar
  20. [20]
    A. Pnueli. The temporal logic of programs. In FOCS’77, pages 46–57. IEEE CS Press, 1977.Google Scholar
  21. [21]
    L. Pottier. Minimal solutions of linear diophantine equations: Bounds and algorithms. In Rewriting Techniques and Applications, volume 488 of LNCS, pages 162–173. Springer-Verlag, 1991.Google Scholar
  22. [22]
    M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In LICS’86, pages 332–344. IEEE CS Press, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Gaoyan Xie
    • 1
  • Cheng Li
    • 1
  • Zhe Dang
    • 1
  1. 1.School of Electrical Engineering and Computer ScienceWashington State UniversityPullmanUSA

Personalised recommendations