Advertisement

A Theory of Duration Calculus with Application

  • Michael Reichhardt Hansen
  • Dang Van Hung
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4710)

Abstract

In this chapter we will present selected central elements in the theory of Duration Calculus and we will give examples of applications. The chapter will cover syntax, semantics and proof system for the basic logic. Furthermore, results on decidability, undecidability and model-checking will be presented. A few extensions of the basic calculus will be described, in particular, Hybrid Duration Calculus and Duration Calculus with iterations. Furthermore, a case study: the bi-phase mark protocol, is presented. We will not attempt to be exhaustive in our coverage of topics; but we will provide references for further study.

Keywords

Real-time systems metric-time temporal logic duration calculus decidability model-checking application 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Asarin, E., Caspi, P., Maler, O.: A Kleene Theorem for Timed Automata. In: LICS 1997. International Symposium on Logics in Computer Science, pp. 160–171. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  2. 2.
    Allen, J.F.: Towards a general theory of action and time. Artificial Intelligence 23, 123–154 (1984)zbMATHCrossRefGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Comput. Sci. 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal – a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) Hybrid Systems III. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  5. 5.
    Bjørner, D.: Trusted computing systems: the ProCoS experience. In: Proceedings of the 14th international conference on Software engineering, Melbourne, Australia, pp. 15–34. ACM Press, New York (1992)Google Scholar
  6. 6.
    Bjørner, D., Hensson, M. (eds.): Logics of Specification Languages. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (to appear 2007)Google Scholar
  7. 7.
    Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge (2001)Google Scholar
  8. 8.
    Bolander, B., Hansen, J.U., Hansen, M.R.: Decidability of hybrid duration calculus. ENTCS 174(6), 113–133 (2006)Google Scholar
  9. 9.
    Braberman, V.A., Hung, D.V.: On checking timed automata for linear duration invariants. In: Proceedings of the 19th IEEE Real-Time Systems Symposium, pp. 264–273. IEEE Computer Society Press, Los Alamitos (1998)CrossRefGoogle Scholar
  10. 10.
    Buchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66–92 (1960)CrossRefMathSciNetGoogle Scholar
  11. 11.
    Chan, P., Hung, D.V.: Duration calculus specification of scheduling for tasks with shared resources. In: Kanchanasut, K., Levy, J.-J. (eds.) Algorithms, Concurrency and Knowledge. LNCS, vol. 1023, pp. 365–380. Springer, Heidelberg (1995)Google Scholar
  12. 12.
    Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Tenth Annual IEEE Symp. on Logic in Computer Science, pp. 36–43. IEEE Press, Los Alamitos (1995)CrossRefGoogle Scholar
  13. 13.
    Dutertre, B.: On first order interval temporal logic. Technical report, Report no. CSD-TR-94-3, Department of Computer Science, Royal Holloway, University of London, Eghan, Surrey TW20 0EX, England (1995)Google Scholar
  14. 14.
    Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society 98, 21–52 (1961)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Fränzle, M., Hansen, M.R.: A Robust Interpretation of Duration Calculus. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 257–271. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Fränzle, M., Hansen, M.R.: Deciding an Interval Logic with Accumulated Durations. In: Grumberg, O., Huth, M.D.V. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 201–215. Springer, Heidelberg (2007)Google Scholar
  17. 17.
    Fränzle, M.: Synthesizing controllers from duration calculus. In: Jonsson, B., Parrow, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 1135, pp. 168–187. Springer, Heidelberg (1996)Google Scholar
  18. 18.
    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, pp. 245–264. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  19. 19.
    Guelev, D.P., Van Hung, D.: On the completeness and decidability of duration calculus with iteration. Theor. Comput. Sci. 337(1-3), 278–304 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Guelev, D.P.: A Complete Proof System for First Order Interval Temporal Logic with Projection. Technical Report 202, UNU-IIST, P.O.Box 3058, Macau (June 2000) (A revised version of this report was published in the Journal of Logic and Computation 14(2), 215–249, Oxford University Press (April 2004))Google Scholar
  21. 21.
    Guelev, D.P.: A calculus of durations on abstract domains: Completeness and extensions. Technical report, UNU/IIST 139 (1998)Google Scholar
  22. 22.
    Guelev, D.P., Hung, D.V.: On the completeness and decidability of duration calculus with iteration. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 139–150. Springer, Heidelberg (1999)Google Scholar
  23. 23.
    Halpern, J., Moskowski, B., Manna, Z.: A hardware semantics based on temporal intervals. In: Díaz, J. (ed.) Automata, Languages and Programming. LNCS, vol. 154, pp. 278–291. Springer, Heidelberg (1983)CrossRefGoogle Scholar
  24. 24.
    Halpern, J., Shoham, Y.: A propositional modal logic of time intervals. Journal of the ACM 33(4), 935–962 (1991)CrossRefMathSciNetGoogle Scholar
  25. 25.
    Hansen, M.R.: Duration Calculus. Chapter in [6], pp. 293–441 (2007)Google Scholar
  26. 26.
    Hansen, M.R.: Model-checking discrete duration calculus. Formal Aspects of Computing 6A, 826–845 (1994)CrossRefGoogle Scholar
  27. 27.
    Hansen, M.R., Zhou, C.: Semantics and completeness of duration calculus. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) Real-Time: Theory in Practice. LNCS, vol. 600, pp. 209–225. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  28. 28.
    Hansen, M.R., Zhou, C.: Duration calculus: Logical foundations. Formal Aspects of Computing 9, 283–330 (1997)zbMATHCrossRefGoogle Scholar
  29. 29.
    Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  30. 30.
    Hoenicke: Combination of Processes, Data and Time. Dissertation, Carl von Ossietzky Universität, Oldenburg, Germany (2006)Google Scholar
  31. 31.
    Van Hung, D.: Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus. Research Report 377, UNU-IIST, P.O.Box 3058, Macau (June 2007)Google Scholar
  32. 32.
    Hung, D.V., Il, K.-K.: Verification via Digitized Model of Real-Time Systems. Research Report 54, UNU-IIST, P.O.Box 3058, Macau (February 1996) (published in the Proceedings of Asia-Pacific Software Engineering Conference 1996 (APSEC 1996), pp. 4–15, IEEE Computer Society Press (1996))Google Scholar
  33. 33.
    Hung, D.V.: Modelling and verification of biphase mark protocols in duration calculus using pvs/dc. In: CSD 1998. Application of Concurrency to System Design, pp. 88–98. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  34. 34.
    Hung, D.V., Thai, P.H.: Checking a Regular Class of Duration Calculus Models for Linear Duration Invariants. Technical Report 118, UNU/IIST, P.O.Box 3058, Macau (July 1997) (presented at and published in Kramer, B., Uchihira, N., Croll, P., Russo, S. (eds.) The Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE’98), April 20-21, 1998, Kyoto, Japan, pp. 61–71. IEEE Computer Society Press (1998))Google Scholar
  35. 35.
    Hung, D.V., Giang, P.H.: A sampling semantics of duration calculus. In: Jonsson, B., Parrow, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 1135, pp. 188–207. Springer, Heidelberg (1996)Google Scholar
  36. 36.
    Hung, D.V., Guelev, D.P.: Completeness and decidability of a fragment of duration calculus with iteration. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 139–150. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  37. 37.
    Hung, D.V., Ji, W.: On design of hybrid control systems using i/o automata models. In: Chandru, V., Vinay, V. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 1180, pp. 156–167. Springer, Heidelberg (1996)Google Scholar
  38. 38.
    Zhao, J., Hung, D.V.: On checking real-time parallel systems for linear duration properties. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 241–250. Springer, Heidelberg (1998)Google Scholar
  39. 39.
    Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S.: Integration graphs: A class of decidable hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) Hybrid Systems. LNCS, vol. 736, pp. 179–208. Springer, Heidelberg (1993)Google Scholar
  40. 40.
    Klarlund, N., Moller, A.: MONA Version 1.4: User Manual. BRICS, Department of Computer Science, University of Aarhus, Denmark (2001)Google Scholar
  41. 41.
    Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 230–244. Springer, Heidelberg (2005)Google Scholar
  42. 42.
    Li, X.: A Mean Value Calculus. PhD Thesis, Software Institute, Academia Sinica (1993)Google Scholar
  43. 43.
    Li, X., Hung, D.V.: Checking linear duration invariants by linear programming. In: Jaffar, J., Yap, R.H.C. (eds.) ASIAN 1996. LNCS, vol. 1179, pp. 321–332. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  44. 44.
    Li, X., Hung, D.V., Zheng, T.: Checking hybrid automata for linear duration invariants. In: Suciu, D., Vossen, G. (eds.) WebDB 2000. LNCS, vol. 1997, pp. 166–180. Springer, Heidelberg (2001)Google Scholar
  45. 45.
    Mao, X., Xu, Q., Hung, D.V., Wang, J.: Towards a proof assistant for interval logics. Technical report, UNU/IIST Report No. 77, UNU/IIST, International Institute for Software Technology, Macau (1996)Google Scholar
  46. 46.
    Moszkowski,: A temporal logic for multilevel reasoning about hardware. IEEE Computer 18(2), 10–19 (1985)Google Scholar
  47. 47.
    Olderog, E.R., Dierks, H.: Decomposing real-time specifications. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, Springer, Heidelberg (1998)CrossRefGoogle Scholar
  48. 48.
    Pandya, P.K., Krishna, S.N., Loya, K.: On Sampling Abstraction of Continuous Time Logic with Duration Calculus. Technical Report TIFR-PKP-GM-2006/1, Tata Institute of Fundamental Research, India (2006)Google Scholar
  49. 49.
    Pandya, P.K.: Some extensions to propositional mean value calculus: Expressiveness and decidability. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 434–451. Springer, Heidelberg (1996)Google Scholar
  50. 50.
    Pandya, P.K.: Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. Tata Institute of Fundamental Research, India. Technical report, TCS00-PKP-1 (2000)Google Scholar
  51. 51.
    Pandya, P.K.: Dcvalid 1.3: The user manual. Technical report, Computer Science Group, TIFR, Bombay, Technical Report TCS-99/1 (1999)Google Scholar
  52. 52.
    Rabinovich, A.: Non-elementary lower bound for propositional duration calculus. Information Processing Letters, pp. 7–11 (1998)Google Scholar
  53. 53.
    Rabinovich, A.: On the decidability of continuous time specification formalism. Journal of logic and computation 8(5), 669–678 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  54. 54.
    Rasmussen, T.M.: Automated proof support for interval logics. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 317–326. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  55. 55.
    Rasmussen, T.M.: Labelled natural deduction for interval logics. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 308–323. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  56. 56.
    Rasmussen, T.M.: Interval Logic: Proof Theory and Theorem Proving. PhD Thesis, Informatics and Mathematical Modelling, Technical University of Denmark (2002)Google Scholar
  57. 57.
    Ravn, A.P.: Design of Embedded Real-Time Computing Systems. Doctoral Dissertation, Department of Computer Science, Technical University of Denmark (1995)Google Scholar
  58. 58.
    Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng. 19(1), 41–55 (1993)CrossRefGoogle Scholar
  59. 59.
    Satpathy, M., Hung, D.V., Pandya, P.K.: Some results on the decidability of duration calculus under synchronous interpretation. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 186–197. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  60. 60.
    Skakkebæk, J.U.: A Verification Assistant for a Real-Time Logic. PhD Thesis, Department of Computer Science, Technical University of Denmark (1994)Google Scholar
  61. 61.
    Skakkebæk, J.U., Sestoft, P.: Checking validity of duration calculus formulas. Technical report, ProCoS II, ESPRIT BRA 7071, report no. ID/DTH JUS 3/1, Department of Computer Science, Technical University of Denmark (1994)Google Scholar
  62. 62.
    Skakkebæk, J.U., Shankar, N.: Towards a duration calculus proof assistant in pvs. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 863, pp. 660–679. Springer, Heidelberg (1994)Google Scholar
  63. 63.
    Sørensen, E.V., Ravn, A.P., Rischel, H.: Control program for a gas burner: Part 1: Informal requirements, procos case study 1. Technical report, ProCoS Rep. ID/DTH EVS2 (1990)Google Scholar
  64. 64.
    Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, California (1948)Google Scholar
  65. 65.
    Thai, P.H., Hung, D.V.: Verifying Linear Duration Constraints of Timed Automata. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 295–309. Springer, Heidelberg (2005)Google Scholar
  66. 66.
    Wang, F., Mok, A.K., Emerson, E.A.: Distributed Real-Time System Specification and Verification in APTL. ACM Transactions on Software Engineering and Methodology 2(4), 346–378 (1993)CrossRefGoogle Scholar
  67. 67.
    Zheng, Y., Zhou, C.: A formal proof of the deadline driven scheduler. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 863, pp. 756–775. Springer, Heidelberg (1994)Google Scholar
  68. 68.
    Zhou, C., Hansen, M.R.: An adequate first order logic of intervals. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 584–608. Springer, Heidelberg (1998)Google Scholar
  69. 69.
    Zhou, C., Hansen, M.R., Ravn, A.P., Rischel: Duration specifications for shared processors. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 571, pp. 21–32. Springer, Heidelberg (1991)Google Scholar
  70. 70.
    Zhou, C., Hansen, M.R.: Duration Calculus: A formal approach to real-time systems. Springer, New York (2004)zbMATHGoogle Scholar
  71. 71.
    Zhou, C., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 93. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993)Google Scholar
  72. 72.
    Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  73. 73.
    Zhou, C., Zhang, J., Yang, L., Li, X.: Linear duration invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 863, pp. 86–109. Springer, Heidelberg (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Michael Reichhardt Hansen
    • 1
  • Dang Van Hung
    • 2
  1. 1.Informatics and Math. Modelling, Technical University of Denmark, Ricard Petersens Plads, DK-2800 LyngbyDenmark
  2. 2.United Nations University, Institute of Software Technology, Casa Silva Mendes, Est. do Engenheiro Trigo No. 4, Macao 

Personalised recommendations