Advertisement

Take It NP-Easy: Bounded Model Construction for Duration Calculus

  • Martin Fränzle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)

Abstract

Following the recent successes of bounded model-checking, we reconsider the problem of constructing models of discrete-time Duration Calculus formulae. While this problem is known to be non-elementary when arbitrary length models are considered [Han94], it turns out to be only NP-complete when constrained to bounded length.

As a corollary we obtain that model construction is in NP for the formulae actually encountered in case studies using Duration Calculus, as these have a certain small-model property.

First experiments with a prototype implementation of the procedures demonstrate a competitive performance.

Keywords

Discrete-time Duration Calculus Model construction Bounded model construction Complexity 

References

  1. AB00.
    A. Ayari AND D. Basin. Bounded model construction for monadic second-order logics. In E. A. Emerson and A. P. Sistla, eds., Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes in Computer Science, pages 99–113. Springer-Verlag, 2000.CrossRefGoogle Scholar
  2. AD94.
    R. Alur AND D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  3. Bär01.
    O. Bär. Übersetzung von SMI in um lineare Arithmetik erweiterte CNF. Diplomarbeit, Fachbereich Informatik der Carl v. Ossietzky Universität Oldenburg, Germany, December 2001.Google Scholar
  4. BCZ99.
    A. Biere, A. Cimatti, AND Y. Zhu. Symbolic model checking without BDDs. In TACAS’99, volume 1579 of Lecture Notes in Computer Science. Springer-Verlag, 1999.Google Scholar
  5. BKR96.
    M. Biehl, N. Klarlund, AND T. Rauhe. Mona: Decidable arithmetic in practice. In J. Parrow, eds. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘96), volume 1135 of Lecture Notes in Computer Science. Springer-Verlag, 1996 Jonsson and Parrow [JP96], pages 459–462.Google Scholar
  6. BLR95.
    A. Bouajjani, Y. Lakhnech, AND R. Robbana. From duration calculus to linear hybrid automata. In P. Wolper, ed., Computer Aided Verification (CAV ‘95), volume 939 of Lecture Notes in Computer Science. Springer-Verlag, 1995.Google Scholar
  7. Frä97.
    M. Fränzle. Controller Design from Temporal Logic: Undecidability need not matter. Dissertation, Technische Fakultät der Christian-Albrechts-Universität Kiel, Germany, 1997. Available as Bericht Nr. 9710, Institut für Informatik und Prakt. Mathematik der Christian-Albrechts-Universität Kiel, Germany, and via WWW under URL http://ca. informatik.uni-oldenburg.de/~fraenzle/diss. html.Google Scholar
  8. Frä02.
    M. Fränzle. Model-checking dense-time duration calculus. Accepted for Formal Aspects of Computing, to appear 2002.Google Scholar
  9. Han94.
    M. R. Hansen. Model-checking discrete duration calculus. Formal Aspects of Computing, 6(6A):826–845, 1994.zbMATHCrossRefGoogle Scholar
  10. HZ97.
    M. R. Hansen AND Zhou Chaochen. Duration calculus: Logical foundations. Formal Aspects of Computing, 9(3):283–330, 1997.zbMATHCrossRefGoogle Scholar
  11. JP96.
    B. Jonsson AND J. Parrow, eds. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘96), volume 1135 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  12. Lak96.
    Y. Laknech. Specification and Verification of Hybrid and Real-Time Systems. Dissertation, Technische Fakultät der Christian-Albrechts-Universität Kiel, Germany, 1996.Google Scholar
  13. LdRV94.
    H. Langmaack, W.-P. De Roever, AND J. Vytopil, eds. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘94), volume 863 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  14. Mos85.
    B. Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10–19, 1985.Google Scholar
  15. MS73.
    A. R. Meyer AND L. Stockmeyer. Nonelementary word problems in automata and logic. In Proc. AMS Symposium on Complexity of Computation, April 1973.Google Scholar
  16. NW99.
    A. Nonnengart AND C. Weidenbach. Computing small clause normal forms. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning. Elsevier Science B.V., 1999.Google Scholar
  17. Pan96.
    P. K. Pandya. Weak chop inverses and liveness in mean-value calculus. In J. Parrow, eds. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘96), volume 1135 of Lecture Notes in Computer Science. Springer-Verlag, 1996 Jonsson and Parrow [JP96], pages 148–167.Google Scholar
  18. Pan00.
    P. Pandya. Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. Technical report TCS00-PKP-1, Tata Institute of Fundamental Research, India, 2000.Google Scholar
  19. PG86.
    D. A. Plaisted AND S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2:293–304, 1986.zbMATHMathSciNetCrossRefGoogle Scholar
  20. Rav95.
    A. P. Ravn. Design of Embedded Real-Time Computing Systems. Doctoral dissertation, Department of Computer Science, Danish Technical University, Lyngby, DK, October 1995. Available as technical report ID-TR: 1995-170.zbMATHGoogle Scholar
  21. RRH93.
    A. P. Ravn, H. Rischel, AND K. M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41–55, January 1993.Google Scholar
  22. Ska94.
    J. U. Skakkebæk. Liveness and fairness in duration calculus. In B. Jonsson and J. Parrow, eds., CONCUR‘94, volume 836 of Lecture Notes in Computer Science, pages 283–298. Springer-Verlag, 1994.Google Scholar
  23. SS94a.
    J. U. Skakkebæk AND P. Sestoft. Checking validity of duration calculus formulas. ProCoS Technical Report ID/DTH JUS 3/1, Technical University of Denmark, March 1994.Google Scholar
  24. SS94b.
    J. U. Skakkebæk AND N. Shankar. Towards a duration calculus proof assistant in PVS. In W.-P. De Roever, AND J. Vytopil, eds. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘94), volume 863 of Lecture Notes in Computer Science. Springer-Verlag, 1994 Langmaack et al. [LdRV94], pages 660–679.Google Scholar
  25. Tse68.
    G. Tseitin. On the complexity of derivations in propositional calculus. In A. Slisenko, ed., Studies in Constructive Mathematics and Mathematical Logics, 1968.Google Scholar
  26. ZH96.
    Zhou Chaochen AND M. R. Hansen. Chopping a point. Handout at the 4th ProCoS Working Group Meeting, March 1996.Google Scholar
  27. Zho93.
    Zhou Chaochen. Duration calculi: An overview. In D. Bjørner, M. Broy, and I. V. Pottosin, eds., Formal Methods in Programming and Their Applications, volume 735 of Lecture Notes in Computer Science, pages 256–266. Springer-Verlag, 1993.CrossRefGoogle Scholar
  28. ZHR91.
    Zhou Chaochen, C. A. R. Hoare, AND A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  29. ZHS93.
    Zhou Chaochen, M. R. Hansen, AND P. Sestoft. Decidability and undecidability results for duration calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, eds., Symposium on Theoretical Aspects of Computer Science (STACS 93), volume 665 of Lecture Notes in Computer Science, pages 58–68. Springer-Verlag, 1993.Google Scholar
  30. ZL94.
    Zhou Chaochen AND Li Xiaoshan. A mean value calculus of durations. In A. W. Roscoe, ed., A Classical Mind — Essays in Honour of C.A.R. Hoare, chapter 25, pages 431–451. Prentice-Hall Intl., 1994.Google Scholar
  31. ZZYL94.
    Zhou Chaochen, Zhang Jingzhong, Yang Lu, AND Li Xiaoshan. Linear duration invariants. In W.-P. De Roever, AND J. Vytopil, eds. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘94), volume 863 of Lecture Notes in Computer Science. Springer-Verlag, 1994 Langmaack et al. [LdRV94], pages 86–109.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Martin Fränzle
    • 1
  1. 1.Department of Computer ScienceCarl-von-Ossietzky Universität OldenburgOldenburgGermany

Personalised recommendations