An Automata-Theoretic Completeness Proof for Interval Temporal Logic

1. H. Bowman and S. J. Thompson. A complete axiomatization of Interval Temporal Logic with projection. Technical Report 6-00, Computing Lab., Univ. of Kent, UK, Jan. 2000.

   Google Scholar 

2. A. Cau and H. Zedan. Refining Interval Temporal Logic specifications. In M. Bertran and T. Rus, eds., Transformation-Based Reactive Systems Development, LNCS 1231, pp. 79–94. AMAST, Springer-Verlag, 1997.

   Google Scholar 

3. B. Dutertre. Complete proof systems for first order interval temporal logic. In Proc. 10th LICS, pp. 36–43. IEEE Computer Soc. Press, June 1995.

   Google Scholar 

4. M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194–211, Apr. 1979.

   Google Scholar 

5. R. W. S. Hale. Programming in Temporal Logic. PhD thesis, Computer Laboratory, Cambridge University, Cambridge, England, Oct. 1988.

   Google Scholar 

6. J. Halpern, Z. Manna, and B. Moszkowski. A hardware semantics based on temporal intervals. In J. Diaz, ed., Proc. ICALP’ 83, LNCS 154, pp. 278–291. Springer-Verlag, 1983.

   Google Scholar 

7. Y. Kesten and A. Pnueli. A complete proof system for QPTL. In Proc. 10th LICS, pp. 2–12. IEEE Computer Soc. Press, 1995.

   Google Scholar 

8. B. Moszkowski. Reasoning about Digital Circuits. PhD thesis, Dept. Computer Science, Stanford Univ., 1983. Tech. rep. STAN-CS-83-970.

   Google Scholar 

9. B. Moszkowski. A temporal logic for multi-level reasoning about hardware. In Proc. 6-th Int’l. Symp. on Computer Hardware Description Languages, pp. 79–90, Pittsburgh, Penn., May 1983. North-Holland Pub. Co.

   Google Scholar 

10. B. Moszkowski. A temporal logic for multilevel reasoning about hardware. Computer, 18:10–19, 1985.

    Article  Google Scholar 

11. B. Moszkowski. Executing Temporal Logic Programs. Cambridge U. Press, 1986.

    Google Scholar 

12. B. Moszkowski. Some very compositional temporal properties. In E.-R. Olderog, ed., Programming Concepts, Methods and Calculi, IFIP Transactions A-56, pp. 307–326. IFIP, Elsevier Science B.V (North-Holland), 1994.

    Google Scholar 

13. B. Moszkowski. Compositional reasoning about projected and infinite time. In Proc. 1st IEEE Int’l Conf. on Engineering of Complex Computer Systems (ICECCS’95), pp. 238–245. IEEE Computer Soc. Press, 1995.

    Google Scholar 

14. B. Moszkowski. Compositional reasoning using Interval Temporal Logic and Tempura. In W.-P. deRoever et al., eds., Compositionality: The Significant Difference, LNCS 1536, pp. 439–464. Springer-Verlag, 1998.

    Chapter  Google Scholar 

15. B. Moszkowski. A complete axiomatization of interval temporal logic with infinite time. In Proc. 15th Annual IEEE Symp. on Logic in Computer Science (LICS 2000). IEEE Computer Soc. Press, June 2000.

    Google Scholar 

16. B. Paech. Gentzen-systems for propositional temporal logics. In E. Börger et al., eds., Proc. 2nd Workshop on Computer Science Logic, Duisburg (FRG), LNCS 385, pp. 240–253. Springer-Verlag, Oct. 1988.

    Google Scholar 

17. V. R. Pratt. Semantical considerations on Floyd-Hoare logic. In 17-th Annual IEEE Symposium on Foundations of Computer Science, pp. 109–121, 1976.

    Google Scholar 

18. R. Rosner and A. Pnueli. A choppy logic. In Proc. 1st LICS, pp. 306–313. IEEE Computer Soc. Press, June 1986.

    Google Scholar 

19. D. Siefkes. Decidable Theories I: Büchi’s Monadic Second Order Successor Arithmetic, Lecture Notes in Mathematics 120. Springer-Verlag, Berlin, 1970.

    MATH  Google Scholar 

20. Wang Hanpin and Xu Qiwen. Temporal logics over infinite intervals. Technical Report 158, UNU/IIST, Macau, 1999.

    Google Scholar 

21. Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Inf. Process. Lett., 40(5):269–276, 1991.

    Article  MATH  MathSciNet  Google Scholar 

Download references