Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

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

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 2469))

  • 1180Accesses

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.

Similar content being viewed by others

Keywords

References

  1. 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 ofLecture Notes in Computer Science, pages 99–113. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  2. R.Alur AND D. L.Dill. A theory of timed automata.Theoretical Computer Science, 126(2):183–235, 1994.

    Article MATH MathSciNet  Google Scholar 

  3. 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. A.Biere, A.Cimatti,AND Y.Zhu. Symbolic model checking without BDDs. InTACAS’99, volume 1579 ofLecture Notes in Computer Science. Springer-Verlag, 1999.

    Google Scholar 

  5. 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 ofLecture Notes in Computer Science. Springer-Verlag, 1996 Jonsson and Parrow [JP96], pages 459–462.

    Google Scholar 

  6. 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 ofLecture Notes in Computer Science. Springer-Verlag, 1995.

    Google Scholar 

  7. 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 URLhttp://ca. informatik.uni-oldenburg.de/~fraenzle/diss. html.

    Google Scholar 

  8. M.Fränzle. Model-checking dense-time duration calculus. Accepted forFormal Aspects of Computing, to appear 2002.

    Google Scholar 

  9. M. R.Hansen. Model-checking discrete duration calculus.Formal Aspects of Computing, 6(6A):826–845, 1994.

    Article MATH  Google Scholar 

  10. M. R.Hansen AND Zhou Chaochen. Duration calculus: Logical foundations.Formal Aspects of Computing, 9(3):283–330, 1997.

    Article MATH  Google Scholar 

  11. B.Jonsson AND J.Parrow, eds.Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘96), volume 1135 ofLecture Notes in Computer Science. Springer-Verlag, 1996.

    Google Scholar 

  12. 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. H.Langmaack, W.-P.De Roever,AND J.Vytopil, eds.Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ‘94), volume 863 ofLecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

  14. B.Moszkowski. A temporal logic for multi-level reasoning about hardware.IEEE Computer, 18(2):10–19, 1985.

    Google Scholar 

  15. A. R.Meyer AND L.Stockmeyer. Nonelementary word problems in automata and logic. InProc. AMS Symposium on Complexity of Computation, April 1973.

    Google Scholar 

  16. 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. 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 ofLecture Notes in Computer Science. Springer-Verlag, 1996 Jonsson and Parrow [JP96], pages 148–167.

    Google Scholar 

  18. 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. D. A.Plaisted AND S.Greenbaum. A structure-preserving clause form translation.Journal of Symbolic Computation, 2:293–304, 1986.

    Article MATH MathSciNet  Google Scholar 

  20. 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.

    MATH  Google Scholar 

  21. 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. J. U.Skakkebæk. Liveness and fairness in duration calculus. In B. Jonsson and J. Parrow, eds.,CONCUR‘94, volume 836 ofLecture Notes in Computer Science, pages 283–298. Springer-Verlag, 1994.

    Google Scholar 

  23. 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. 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 ofLecture Notes in Computer Science. Springer-Verlag, 1994 Langmaack et al. [LdRV94], pages 660–679.

    Google Scholar 

  25. 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. Zhou Chaochen AND M. R.Hansen. Chopping a point. Handout at the 4th ProCoS Working Group Meeting, March 1996.

    Google Scholar 

  27. 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 ofLecture Notes in Computer Science, pages 256–266. Springer-Verlag, 1993.

    Chapter  Google Scholar 

  28. Zhou Chaochen, C. A. R.Hoare,AND A. P.Ravn. A calculus of durations.Information Processing Letters, 40(5):269–276, 1991.

    Article MATH MathSciNet  Google Scholar 

  29. 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 ofLecture Notes in Computer Science, pages 58–68. Springer-Verlag, 1993.

    Google Scholar 

  30. 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. 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 ofLecture Notes in Computer Science. Springer-Verlag, 1994 Langmaack et al. [LdRV94], pages 86–109.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Carl-von-Ossietzky Universität Oldenburg, P.O. Box 2503, D-26111, Oldenburg, Germany

    Martin Fränzle

Authors
  1. Martin Fränzle

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fachbereich Informatik, Universität Oldenburg, Ammerländer Herrstr. 114-118, 26129, Oldenburg, Germany

    Werner Damm  & Ernst -Rüdiger Olderog  & 

Rights and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fränzle, M. (2002). Take It NP-Easy: Bounded Model Construction for Duration Calculus. In: Damm, W., Olderog, E.R. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2002. Lecture Notes in Computer Science, vol 2469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45739-9_16

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp