research-article

Completeness of the accumulation calculus

Authors:

Huiqun Yu,

Guoxin Song,

Yongqiang SunAuthors Info & Claims

Journal of Computer Science and Technology, Volume 13, Issue 1

Pages 25 - 31

https://doi.org/10.1007/BF02946611

Published: 22 March 2023 Publication History

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.

References

[1]

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

Google Scholar

[2]

Lamport L Temporal Logic of Actions 1991 USA Systems Research Center of DEC

Google Scholar

[3]

Manna Z and Pnueli A Models for reactivity Acta Informatica 1993 30 609-678

Crossref

Google Scholar

[4]

Moszkowski B A temporal logic for multi-level reasoning about hard ware IEEE Computer 1985 18 2 10-19

Google Scholar

[5]

Zhou Chaochen, Hoare C A R, and Ravn A P A calculus of durations Information Processing Letters 1991 40 5 269-276

Crossref

Google Scholar

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

Google Scholar

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

Google Scholar

Recommendations

Completeness of temporal logics over infinite intervals
Discrete mathematics and theoretical computer science (DMTCS)

Interval temporal logics over infinite intervals are studied. First, the ordinary possible worlds models are extended to infinite possible world models. Accordingly, an axiomatic system is proposed and it has been proved complete. Secondly, infinite ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Soundness and Completeness Proofs by Coinductive Methods

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Computer Science and Technology

Journal of Computer Science and Technology Volume 13, Issue 1

Jan 1998

96 pages

ISSN:1000-9000

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 March 2023

Revision received: 20 December 1996

Received: 25 May 1996

Author Tags

Qualifiers

Research-article

Recommendations

Completeness of temporal logics over infinite intervals

Completeness and decidability of converse PDL in the constructive type theory of Coq

Soundness and Completeness Proofs by Coinductive Methods

Comments

Published In

Publisher

Publication History

Author Tags

Qualifiers

Other Metrics

Article Metrics

Other Metrics

Abstract

References

Recommendations

Completeness of temporal logics over infinite intervals

Completeness and decidability of converse PDL in the constructive type theory of Coq

Soundness and Completeness Proofs by Coinductive Methods

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations