A really temporal logic
Tóm tắt
Từ khóa
Tài liệu tham khảo
~ABADI , M. , AND LAMPORT , L. 1992. An old-fashioned recipe for real time . In Real Time: Theo~ ~in Practice. J. W. de Bakker, K. Huizing, W.-P . de Roever, and G. Rozenberg, eds. Lecture ~Notes in Computer Science, vol. 600 . Springer-Verlag , New York, pp. 1 - 27 . ~ABADI, M., AND LAMPORT, L. 1992. An old-fashioned recipe for real time. In Real Time: Theo~ ~in Practice. J. W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, eds. Lecture ~Notes in Computer Science, vol. 600. Springer-Verlag, New York, pp. 1-27.
~ALUR , R. , COURCOUBET t S, C ., AND DILL , D. L. 1990 . Model checking for real-time systems. In ~Proceedings of the 5th Annual Sympostum on Logic in Computer Science, IEEE Computer Society ~Press , New York , pp. 414 - 425 . ~ALUR, R., COURCOUBETtS, C., AND DILL, D. L. 1990. Model checking for real-time systems. In ~Proceedings of the 5th Annual Sympostum on Logic in Computer Science, IEEE Computer Society ~Press, New York, pp. 414-425.
~ALUR , R. , FEDER , T. , AND HENZINGER , T. A. 1991 . The benefits of relaxing punctuality. In ~Proceedings of the lOth Annual Symposium on Principles of Distributed Computing, (Montreal, ~Que., Canada, Aug. 19-21) . ACM , New York , pp. 139 - 152 . 10.1145/112600.112613 ~ALUR, R., FEDER, T., AND HENZINGER, T. A. 1991. The benefits of relaxing punctuality. In ~Proceedings of the lOth Annual Symposium on Principles of Distributed Computing, (Montreal, ~Que., Canada, Aug. 19-21). ACM, New York, pp. 139-152. 10.1145/112600.112613
~ALUR , R. , AND HENZINGER , T. A. 1989 . A really temporal logic . In Proceedings of the 30th ~Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, New ~York , pp. 164 - 169 . ~ALUR, R., AND HENZINGER, T. A. 1989. A really temporal logic. In Proceedings of the 30th ~Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, New ~York, pp. 164-169.
~ALUR , R. , AND HENZINGER , T. A. 1990 . Real-time logics: Complexity and expressiveness. In ~Proceedings of the 5th Annual Symposium on Logic in Computer Science. IEEE Computer Society ~Press , New York , pp. 390 - 401 . ~ALUR, R., AND HENZINGER, T. A. 1990. Real-time logics: Complexity and expressiveness. In ~Proceedings of the 5th Annual Symposium on Logic in Computer Science. IEEE Computer Society ~Press, New York, pp. 390-401.
~ALUR , R. , AND HENZINGER , T. m ., 1992 . Logics and models of real time: A survey. In Real Time: ~Theory in Practice. J. W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, eds. ~Lecture Notes in Computer Science, vol. 600 . Springer-Verlag , New York, pp. 74 - 106 . ~ALUR, R., AND HENZINGER, T. m., 1992. Logics and models of real time: A survey. In Real Time: ~Theory in Practice. J. W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, eds. ~Lecture Notes in Computer Science, vol. 600. Springer-Verlag, New York, pp. 74-106.
~BEN - Am, M ., MANNA , Z. , AND PNUELI , A. 1981 . The temporal logic of branching time. In ~Proceedings of the 8th Annual Symposium on Prmciples of Programming Languages (Williamsburg, ~Va., Jan. 26-28) . ACM , New York , pp. 164 - 176 . 10.1145/567532.567551 ~BEN-Am, M., MANNA, Z., AND PNUELI, A. 1981. The temporal logic of branching time. In ~Proceedings of the 8th Annual Symposium on Prmciples of Programming Languages (Williamsburg, ~Va., Jan. 26-28). ACM, New York, pp. 164-176. 10.1145/567532.567551
~BERNSTEIN , h., AND HARTER , P. K. , JR. 1981 . Proving real-time properties of programs with ~temporal logic . In Proceedings of the 8th Annual Symposium on Operating System Principles ~(Pacific Grove, Calif., Dec. 14-16) . ACM, New York , pp. 1 - 11 . 10.1145/800216.806585 ~BERNSTEIN, h., AND HARTER, P. K., JR. 1981. Proving real-time properties of programs with ~temporal logic. In Proceedings of the 8th Annual Symposium on Operating System Principles ~(Pacific Grove, Calif., Dec. 14-16). ACM, New York, pp. 1-11. 10.1145/800216.806585
~EMERSON , E. A. , MOK , h. K ., SISTLA, h. P., AND SRIN1VASAN, J. 1990 . Quantitative temporal ~reasoning. In CAV 90: Computer-aided Verification. E. M. Clarke and R. P. Kurshan, eds. ~Lecture Notes in Computer Science, vol. 531 . Springer-Verlag , New York, pp. 136 - 145 . ~EMERSON, E. A., MOK, h. K., SISTLA, h. P., AND SRIN1VASAN, J. 1990. Quantitative temporal ~reasoning. In CAV 90: Computer-aided Verification. E. M. Clarke and R. P. Kurshan, eds. ~Lecture Notes in Computer Science, vol. 531. Springer-Verlag, New York, pp. 136-145.
~GABBAY , D. , PNUEL {, A., SHELAH , S. , AND STAVI , J. 1980 . On the temporal analysis of fairness. In ~ Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages (Las ~Vegas, Nev., Jan 28-30) . ACM , New York , pp. 163 - 173 . 10.1145/567446.567462 ~GABBAY, D., PNUEL{, A., SHELAH, S., AND STAVI, J. 1980. On the temporal analysis of fairness. In ~ Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages (Las ~Vegas, Nev., Jan 28-30). ACM, New York, pp. 163-173. 10.1145/567446.567462
~HALPERN J. Y. 1991. Presburger arithmetic with unary predicates is II}-complete. J. Symb. ~Logic 56 2 637-642. 10.2307/2274706 ~HALPERN J. Y. 1991. Presburger arithmetic with unary predicates is II}-complete. J. Symb. ~Logic 56 2 637-642. 10.2307/2274706
~HAREL E. 1988. Temporal analysis of real-time systems. Master's thesis The Weizmann ~Institute of Science Rehovot Israel. ~HAREL E. 1988. Temporal analysis of real-time systems. Master's thesis The Weizmann ~Institute of Science Rehovot Israel.
~HAREL , E. , LICHTENSTEIN , O. , AND PNUELI , h. 1990 . Explicit-clock temporal logic . In Proceedings ~of the 5th Annual Symposium on Logic in Computer Sctence. IEEE Computer Society Press, New ~York , pp. 402 - 413 . ~HAREL, E., LICHTENSTEIN, O., AND PNUELI, h. 1990. Explicit-clock temporal logic. In Proceedings ~of the 5th Annual Symposium on Logic in Computer Sctence. IEEE Computer Society Press, New ~York, pp. 402-413.
~HAREL , D. , PNUELI , h., AND STAVI , J. 1983 . Propositional dynamic logic of regular programs. J. ~Comput . Syst. Sct. , 26 , 2 , 222 - 243 . ~HAREL, D., PNUELI, h., AND STAVI, J. 1983. Propositional dynamic logic of regular programs. J. ~Comput. Syst. Sct., 26, 2, 222-243.
HENZINGER , T. h. 1990 . Half-order modal logic: How to prove real-time properties. In Proceed- ~ings of the 19th Annual ACM Symposium on Principles of Distributed Computing (Quebec City, ~Que., Canada, Aug. 22-24) . ACM , New York , pp. 281 - 286 . 10.1145/93385.93429 HENZINGER, T. h. 1990. Half-order modal logic: How to prove real-time properties. In Proceed- ~ings of the 19th Annual ACM Symposium on Principles of Distributed Computing (Quebec City, ~Que., Canada, Aug. 22-24). ACM, New York, pp. 281-286. 10.1145/93385.93429
~HENZINGER , T. A. , MANNA , g., AND PNUELI, h . 1992 . What good are digital clocks? In ICALP ~92: Automata, Languages, and Programming. W. Kuich, ed. Lecture Notes in Computer Science, ~vol. 623. Springer-Verlag , New York, pp. 545 - 558 . ~HENZINGER, T. A., MANNA, g., AND PNUELI, h. 1992. What good are digital clocks? In ICALP ~92: Automata, Languages, and Programming. W. Kuich, ed. Lecture Notes in Computer Science, ~vol. 623. Springer-Verlag, New York, pp. 545-558.
~HOPCROFT , J. E. , AND ULLMAN , J. D. 1979. Introduction to Automata Theoty, Languages, and ~Computation . Addison-Wesley , Reading, Mass . ~HOPCROFT, J. E., AND ULLMAN, J. D. 1979. Introduction to Automata Theoty, Languages, and ~Computation. Addison-Wesley, Reading, Mass.
~JAHANIAN , F. , AND MOK , h. K. 1986 . Safety analysis of timing properties in real-time systems. ~IEEE Trans. Softw. Eng. SE-12 , 9 , 890 - 904 . ~JAHANIAN, F., AND MOK, h. K. 1986. Safety analysis of timing properties in real-time systems. ~IEEE Trans. Softw. Eng. SE-12, 9, 890-904.
~KOYMANS R. 1990. Specifying real-time properties with metric temporal logic. Real-time Systems ~ 2 4 255-299. 10.1007/BF01995674 ~KOYMANS R. 1990. Specifying real-time properties with metric temporal logic. Real-time Systems ~ 2 4 255-299. 10.1007/BF01995674
~LICHTENSTEIN , O. , AND PNUELI , A. 1985 . Checking that finite state concurrent programs satisfy ~their linear specification . In Proceedings of the 12th Annual ACM Symposium on Prmciples of ~ProgrammmgLanguages (New Orleans, La., Jan. 14-16) . ACM, New York , pp. 97 107. 10.1145/318593.318622 ~LICHTENSTEIN, O., AND PNUELI, A. 1985. Checking that finite state concurrent programs satisfy ~their linear specification. In Proceedings of the 12th Annual ACM Symposium on Prmciples of ~ProgrammmgLanguages (New Orleans, La., Jan. 14-16). ACM, New York, pp. 97 107. 10.1145/318593.318622
~MANNA , Z. , AND PNUEL i, A. 1992. The Temporal Logic of Reactit,e and Concurrent Systems: ~ Specification . Springer-Verlag , New York . ~MANNA, Z., AND PNUELi, A. 1992. The Temporal Logic of Reactit,e and Concurrent Systems: ~ Specification. Springer-Verlag, New York.
~OSTROFF , J. S. 1990. Temporal Logic of Real-Time Systems . Research Studies Press , Taunton , ~England. ~OSTROFF, J. S. 1990. Temporal Logic of Real-Time Systems. Research Studies Press, Taunton, ~England.
PNUEU , A. 1977 . The temporal logic of programs . In Proceedings of the 18th Annual Symposmm on Foundations of Computer Science. IEEE Computer Society Press , New York , pp. 46 - 57 . PNUEU, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposmm on Foundations of Computer Science. IEEE Computer Society Press, New York, pp. 46-57.
~PNUELL A. , AND HAREL , E. 1988. Applications of temporal logic to the specification of real-time ~systems . In Formal Techmques in Real-Time and Fault-Tolerant Systems . M. Joseph, ed Lecture ~Notes m Computer Science, vol. 331 . Springer-Verlag , New York, pp. 84 - 93 . ~PNUELL A., AND HAREL, E. 1988. Applications of temporal logic to the specification of real-time ~systems. In Formal Techmques in Real-Time and Fault-Tolerant Systems. M. Joseph, ed Lecture ~Notes m Computer Science, vol. 331. Springer-Verlag, New York, pp. 84-93.
~PRAT t, V. R. 1980 . A near-optimal method for reasoning about action . J. Comput. Syst. Sci. 20, ~2 , 231 - 254 . ~PRATt, V. R. 1980. A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20, ~2, 231-254.
~ROGERS , H. , JR . 1967. Theory of Recursive Functions and Effectwe Computabdtty . McGraw-Hill , ~New York. ~ROGERS, H., JR. 1967. Theory of Recursive Functions and Effectwe Computabdtty. McGraw-Hill, ~New York.
~SMULLYAN , R. M. 1968. First-Order Logic . Springer-Verlag , New York . ~SMULLYAN, R. M. 1968. First-Order Logic. Springer-Verlag, New York.
~WANG , F. , MOK , h. K ., AND EMERSON, E. h. 1992 . Asynchronous propositional temporal logic. ~In Proceedings of the 12th hzternatlonal Conference of Software Engmeenng . ~WANG, F., MOK, h. K., AND EMERSON, E. h. 1992. Asynchronous propositional temporal logic. ~In Proceedings of the 12th hzternatlonal Conference of Software Engmeenng.