Advertisement

Abstract

The Mean-Value Calculus, MVC, of Zhou and Li [19] is extended with the least and the greatest fixed point operators. The resulting logic is called μMVC. Timed behaviours with naturally recursive structure can be elegantly specified in this logic. Some examples of such usage are given. The expressive power of the logic is also studied. It is shown that the propositional fragment of the logic, even with discrete time, is powerful enough to encode the computations of nondeterministic turing machines. Hence, the satisfiability of propositional μMVC over both dense and discrete times is undecidedable.

Keywords

Point Operator Temporal Logic Expressive Power Proof Rule Open Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Henzinger, T.A.: A Really Temporal Logic. Jour. ACM 41(1) (1994)Google Scholar
  2. 2.
    Banieqbal, B., Barringer, H.: Temporal Logic with Fixed Points. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398. Springer, Heidelberg (1989)Google Scholar
  3. 3.
    Emerson, E.: Real-time and the Mu Calculus. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600. Springer, Heidelberg (1992)Google Scholar
  4. 4.
    Emerson, E., Clarke, E.: Characterising Correctness Properties of Parallel Programs using Fixed-points. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85. Springer, Heidelberg (1980)Google Scholar
  5. 5.
    Hansen, M.R., Pandya, P.K.: Zhou Chaochen. Finite Divergence. Theoretical Computer Science 138, 113–139 (1994)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Hansen, M.R., Zhou, C.: Chaochen Zhou. Duration calculus: Logical foundations. Formal Aspects of Computing 9(3), 283–330 (1997)zbMATHCrossRefGoogle Scholar
  7. 7.
    Kozen, D.: Results on Propositional Mu-calculus. Thoeretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Li, X.: A Mean Value Calculus. Ph.D. Thesis, Software Institute, Academia Sinica (1994)Google Scholar
  9. 9.
    Moszkowski, B.: A Temporal Logic for Multi-level Reasoning about Hardware. IEEE Computer 18(2), 10–19 (1985)Google Scholar
  10. 10.
    Pandya, P.K.: Some Extensions to Mean-Value Calculus: Expressiveness and Decidability. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092. Springer, Heidelberg (1996)Google Scholar
  11. 11.
    Pandya, P.K., Hung, D.V.: Duration Calculus of Weakly Monotonic Time. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, p. 55. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  12. 12.
    Pandya, P.K., Ramakrishna, Y.S.: A Recursive Mean Value Calculus. Technical Report TCS-95/3, Computer Science Group, TIFR, Bombay (1995)Google Scholar
  13. 13.
    Pandya, P.K., Ramakrishna, Y.S., Shyamasundar, R.K.: A Compositional Semantics of Esterel in Duration Calculus. In: Proc. Second AMAST workshop on Real-time Systems: Models and Proofs, Bordeux (June 1995)Google Scholar
  14. 14.
    Pandya, P.K., Wang, H., Xu, Q.: Towards a Theory of Sequential Hybrid Programs. In: de Roever, W.P., Gries, D. (eds.) Proc. PROCOMET 1998, Shelter Island, New York. Chapman & Hall, Boca Raton (1998)Google Scholar
  15. 15.
    Skakkebaek, J.U., Shankar, N.: Towards a Duration Calculus Proof Assistant in PVS. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863. Springer, Heidelberg (1994)Google Scholar
  16. 16.
    Stirling, C.: Modal and Temporal logics. In: Handbook of Logic in Computer Science, vol. 2, pp. 476–563. Clarendon Press, Oxford (1995)Google Scholar
  17. 17.
    Schneider, G., Xu, Q.: Towards Formal Semantics of Verilog using Duration Calculus. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, p. 282. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Zhou, C., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Processing Letters 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Zhou, C., Li, X.: A Mean Value Calculus of Durations. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 431–451. Prentice Hall International, Englewood Cliffs (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Paritosh K. Pandya
    • 1
  • Y. S. Ramakrishna
    • 1
  1. 1.Tata Institute of Fundamental ResearchMumbaiIndia

Personalised recommendations