Advertisement

Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Completeness of the accumulation calculus

  • 17 Accesses

Abstract

The accumulation calculus (AC for short) is an interval based temporal logic to specify and reason about hybrid real-time systems. This paper presents a formal proof system for AC, and proves that the system is complete relative to that of Interval Temporal Logic (ITL for short) on real domain.

This is a preview of subscription content, log in to check access.

References

  1. [1]

    Pnueli A. The temporal logic of programs. In18th Ann. IEEE Symp. on Foundations of Computer Science, 1977, pp.46–57.

  2. [2]

    Lamport L. Temporal Logic of Actions. Technical Report 79, Systems Research Center of DEC, USA, 1991.

  3. [3]

    Manna Z, Pnueli A. Models for reactivity.Acta Informatica, 1993, 30: 609–678.

  4. [4]

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

  5. [5]

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

  6. [6]

    Yu Huiqun, Pandya P K, Sun Yongqiang. A calculus for hybrid sampled data systems. InFormal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, Langmaack H, de Rover W P, Vytopil J (eds.), Springer Verlag, 1994, pp.716–737.

  7. [7]

    Hansen M R, Zhou Chaochen. Semantics and completeness of duration calculus. InReal-Time: Theory in Practice, LNCS 600, de Bakker J W, Huizing C, de Roever W P, Rozenberg G (eds.), Springer-Verlag, 1992, pp.209–225.

Download references

Author information

Correspondence to Huiqun Yu.

Additional information

This work is supported partially by the National Natural Science Foundation of China under the grant No.69703008.

Yu Huiqun received his Ph.D. degree in computer science from Shanghai Jiaotong University. He is currently an Associate Professor in the Department of Computer Science and Engineering at East China University of Science and Technology, Shanghai. His research interests are formal methods, concurrency, reliable real-time systems, semantics of programming languages.

Song Guoxin is a Professor in the Department of Computer Science and Engineering at East China University of Science and Technology, Shanghai. His current research interests are formal methods, object-oriented programming and concurrent engineering.

Sun Yongqiang is a Professor in the Department of Computer Science and Engineering at Shanghai Jiaotong University. His current research interests are formal technique of software development, new paradigm of programming languages, and parallel processing.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Yu, H., Song, G. & Sun, Y. Completeness of the accumulation calculus. J. of Comput. Sci. & Technol. 13, 25–31 (1998). https://doi.org/10.1007/BF02946611

Download citation

Keywords

  • Interval Temporal Logic
  • accumulation calculus
  • real-time system
  • completeness