Advertisement

Bounded Validity Checking of Interval Duration Logic

  • Babita Sharma
  • Paritosh. K. Pandya
  • Supratik Chakraborty
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

Abstract

A rich dense-time logic, called Interval Duration Logic (IDL), is useful for specifying quantitative properties of timed systems. The logic is undecidable in general. However, several approaches can be used for checking validity (and model checking) of IDL formulae in practice. In this paper, we propose bounded validity checking of IDL formulae by polynomially reducing this to checking unsatisfiability of lin-sat formulae. We implement this technique and give performance results obtained by checking the unsatisfiability of the resulting lin-sat formulae using the ICS solver. We also perform experimental comparisons of several approaches for checking validity of IDL formulae, including (a) digitization followed by automata-theoretic analysis, (b) digitization followed by pure propositional SAT solving, and (c) lin-sat solving as proposed in this paper. Our experiments use a rich set of examples drawn from the Duration Calculus literature.

Keywords

Model Check Auxiliary Variable Propositional Variable Propositional Formula Validity Check 
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.

References

  1. 1.
    Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded Model Checking for Timed Systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Ayari, A., Basin, D.: Bounded Model Construction for Monadic Second-Order Logics. In: CAV. LNCS, vol. 1855. Springer, Heidelberg (2000)Google Scholar
  3. 3.
    Bierre, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Bjørner, D.: Trusted computing systems: The procos experience. In: ICSE, pp. 15–34 (1992)Google Scholar
  5. 5.
    Bouajjani, A., Lakhnech, Y., Robbana, R.: From Duration Calculus to Linear Hybrid Automata. In: CAV. LNCS, vol. 939. Springer, Heidelberg (1995)Google Scholar
  6. 6.
    Chakravorty, G., Pandya, P.K.: Digitizing Interval Duration Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 167–179. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Filliâtre, J., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 246. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Fränzle, M.: Model-Checking Dense-Time Duration Calculus. In: Hansen, M.R. (ed.) Duration Calculus: A Logical Approach to Real-Time Systems Workshop proceedings of ESSLLI X (1998)Google Scholar
  9. 9.
    Fränzle, M.: Take it NP-easy: Bounded Model Construction for Duration Calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 245. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Fränzle, M., Herde, C.: Efficient SAT engines for concise logics: Accelerating proof search for zero-one linear constraint systems. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 302–316. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    IDLVALID: Model Checking Dense-time Duration Logics. WWW page (2004), http://www.tcs.tifr.res.in/~pandya/idlvalid.html
  12. 12.
    Karmarkar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4(4), 373–395 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Liu, Z.: Specification and Verification in the Duration Calculus. In: Joseph, M. (ed.) Real-time Systems: Specification, Verification and Analysis, pp. 182–228. Prentice Hall, Englewood Cliffs (1996)Google Scholar
  14. 14.
    Pandya, P.K.: Specifying and Deciding Quantified Discrete-Time Duration Dalculus Formulae using DCVALID. In: Pettersson, P., Yi, W. (eds.) RTTools. Uppsala University Technical Report Series (2000)Google Scholar
  15. 15.
    Pandya, P.K.: Model checking CTL[DC]. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 559. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  16. 16.
    Pandya, P.K.: Interval Duration Logic: Expressiveness and Decidability. In: Asarin, E., Maler, O., Yovine, S. (eds.) TPTS 2002. ENTCS, vol. 65. Elsevier Science Publishers, Amsterdam (2002)Google Scholar
  17. 17.
    Sharma, B.: SAT Based Validity Checking of Interval Duration Logic Formuale. M.Tech Dissertation, Dept. of Computer Science and Engineering, IIT Bombay (June 2004)Google Scholar
  18. 18.
    Skakkebæk, J.U., Sestoft, P.: Checking Validity of Duration Calculus Formulas. ESPRIT project PROCOS II. Technical report, Department of Computer Science, Technical University of Denmark (1996)Google Scholar
  19. 19.
    Zhou, C., Hansen, M.R.: Duration Calculus. Springer, Heidelberg (2003)Google Scholar
  20. 20.
    Zhou, C., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Processing Letters 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Zhou, C., Ravn, A., Hansen, M.R.: An Extended Duration Calculus for Hybrid Real-Time Systems. In: Hybrid Systems, pp. 36–59. Springer, Heidelberg (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Babita Sharma
    • 1
  • Paritosh. K. Pandya
    • 2
  • Supratik Chakraborty
    • 1
  1. 1.Indian Institute of TechnologyBombayIndia
  2. 2.Tata Institute of Fundamental ResearchIndia

Personalised recommendations