Analyzing Chain Programs over Difference Constraints

  • K. Subramani
  • John Argentieri
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3959)


Chain Programming is a restricted form of Linear Programming; in a Chain Program, there exists a total ordering on the program variables. In other words, the constraints x 1x 2 ... x n are either implicitly or explicitly part of the constraint system. At the present juncture, it is not clear whether an arbitrary linear program augmented with a chain is easier to solve than linear programs in general, either asymptotically or computationally. However, if the linear program is constituted entirely of difference constraints, then the total ordering results in a number of interesting properties, which are not true of constraint systems in general. Inasmuch as difference constraint logic is an integral part of a number of verification problems in both model-checking and real-time scheduling, our results are of particular importance to these communities.


Constraint System Constraint Network Symbolic Model Check Bound Model Check Time Automaton 
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. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994) Fundamental StudyGoogle Scholar
  2. Armando, A., Castellini, C., Giunchiglia, E.: Sat-based procedures for temporal reasoning. In: ECP, pp. 97–108 (1999)Google Scholar
  3. Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: SFM, pp. 200–236 (2004)Google Scholar
  4. Brucker, P.: Scheduling Algorithms, 2nd edn. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  5. Clarke, E.M.: Automatic verification of sequential circuit designs. In: Agnew, D., Claesen, L., Camposano, R. (eds.) Proceedings of the 11th International Conference on Computer Hardware Description Languages and their Applications (CHDL 1993). IFIP Transactions A: Computer Science and Technology, vol. 32, pp. 163–166. North-Holland, Amsterdam (1993)Google Scholar
  6. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)zbMATHCrossRefGoogle Scholar
  7. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms, 2nd edn. MIT Press and McGraw-Hill Book Company, Boston (1992)Google Scholar
  8. Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artificial Intelligence 49, 61–95 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  9. Demtrescu, C.: A new approach to dynamic all pairs shortest paths. Journal of the ACM 51(6), 968–992 (2004)CrossRefMathSciNetGoogle Scholar
  10. Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Computers 44(3), 471–479 (1995)zbMATHCrossRefGoogle Scholar
  11. Goldberg, A.V.: Scaling algorithms for the shortest paths problem. SIAM Journal on Computing 24(3), 494–504 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  12. Han, C.C., Lin, K.J.: Scheduling real-time computations with separation constraints. Information Processing Letters 12, 61–66 (1992)CrossRefMathSciNetGoogle Scholar
  13. Ignizio, J.P., Cavalier, T.P.: Linear Programming. Prentice-Hall, Englewood Cliffs (1993)Google Scholar
  14. Larsen, K.G., Steffen, B., Weise, C.: Continuous modelling of real time and hybrid systems. Technical report, Aalborg Universitet, BRICS Technical Report (2003)Google Scholar
  15. Møller, J., Lichternberg, J., Andersen, H.R., Hulgaard, H.: On the symbolic verification of timed systems. Technical report, Technical University of Denmark (2003)Google Scholar
  16. Møller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: CSL, pp. 111–125 (1999)Google Scholar
  17. Møller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Fully symbolic model checking of timed systems using difference decision diagrams. Electr. Notes Theor. Comput. Sci.vol 23(2) (1999)Google Scholar
  18. Muscettola, N., Smith, B., Chien, S., Fry, C., Rabideau, G., Rajan, K., Yan, D.: Inboard planning for autonomous spacecraft. In: The Fourth International Symposium on Artificial Intelligence, Robotics, and Automation for Space (i-SAIRAS) (July 1997)Google Scholar
  19. Muscettola, N., Morris, P., Pell, B., Smith, B.: Issues in temporal reasoning for autonomous control systems. In: The Second International Conference on Autonomous Agents, Minneapolis, MI (1998)Google Scholar
  20. Pallottino. S., Scutellam, M.G.: Dual algorithms for the shortest path tree problem. Networks: An International Journal 29 (1997)Google Scholar
  21. Pallottino, S.: Shortest path methods: Complexity, interrelations and new propositions. Networks: An International Journal 14, 257–267 (1984)zbMATHGoogle Scholar
  22. Pape, U.: Implementation and efficiency of moore algorithms for the shortest root problem. Mathematical Programming 7, 212–222 (1974)zbMATHCrossRefMathSciNetGoogle Scholar
  23. Pinedo, M.: Scheduling: theory, algorithms, and systems. Prentice-Hall, Englewood Cliffs (1995)zbMATHGoogle Scholar
  24. Rasmussen, J.I., Larsen, K.G., Subramani, K.: Resource-optimal scheduling using priced timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 220–235. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  25. Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with sat. In: CAV, pp. 209–222 (2002)Google Scholar
  26. Subramani, K.: An analysis of totally clairvoyant scheduling. Journal of Scheduling 8(2), 113–133 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  27. Subramani, K.: Stressing is better than relaxing for negative cost cycle detection in networks. In: Syrotiuk, V.R., Chávez, E. (eds.) ADHOC-NOW 2005. LNCS, vol. 3738, pp. 320–333. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  28. Subramani, K., Kovalchick, L.: A greedy strategy for detecting negative cost cycles in networks. Future Generation Computer Systems 21(4), 607–623 (2005)CrossRefGoogle Scholar
  29. Wall, A., Sandström, K., Mäki-Turja, J., Norström, C., Yi, W.: Verifying temporal constraints on data in multi-rate transactions using timed automata. In: RTCSA, pp. 263–270 (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • K. Subramani
    • 1
  • John Argentieri
    • 1
  1. 1.LDCSEEWest Virginia UniversityMorgantown

Personalised recommendations