Rajeev Alur
- ~ALUR, R., COURCOUBETIS, C., AND DILL, D. L. 1993. Model checking in dense real time. inf. ~ Comput. 104, 1, 2-34. Google Scholar
- ~At.ug, R., AND DILL, D. L. 1994. A theory of timed automata. Theoret. Comput. Sci., 126, ~ 183-235. Google Scholar
- ~ALUR, R., AND HEr~ZaN6ER, T. A. 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. Rozenbeg, eds. ~ Lecture Notes in Computer Science, vol. 600. Springer-Verlag, New York, pp. 74-106. Google Scholar
- ~ALUR, R., AND HENZI~'t3ER, T. A. 1993. Real-time logics: complexity and expressiveness. Inf. ~ Comput. 104, 1, 35- 77. Google Scholar
- ~ALUg, R., AND HENZaNGEg, T. A. 1994. A really temporal logic. J. ACM 41, 1 (Jan.), 181-204. Google Scholar
- ~CLAm~, E. M., EME~OS, E. A., ANt) SISTLA, A. P. 1986. Automatic verification of finite-state ~ concurrent systems using temporal-logic specifications. A CM Trans. Prog. Lang. Syst. 8, 2, ~ 244-263. Google Scholar
- ~EMERSON, E. A., Mot, A. K., SISTLA, A. P., AND SRtmVASAr~, J. 1990. Quantitative temporal ~ reasoning. CAV 90: Computer-aided Verij~cation, R. P. Kurshan and E. M. Clarke, eds., Lecture ~ Notes in Computer Science, vol. 531. Springer-Verlag, New York, pp. 136-145. Google Scholar
- ~HArU~L, E., LlcrrrEr~sTrraN, O., AND ~ELI, A. 1990. Explicit-clock temporal logic. In Proceeak'ngs ~ of the 5th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, New ~ York, pp. 402-413.Google Scholar
- ~HENZtNt3ER, T. A., NICOLL~, X., SIFAraS, J., AND Yovtr~E, S. 1994. Symbolic model checking for ~ real-time systems. Inf. Comput. 111, 2, 193-244. Google Scholar
- ~HAREL, D., PincH, A., AND STAVl, J. 1983. Propositional dynamic logic of regular programs. J. ~ Comp. Syst. Sci. 26, 2, 222-243.Google Scholar
- ~JAnANtm~, F., AND Mog, A. K. 1986. Safety analysis of timing properties in real-time systems. ~ IEEE Trans. Softw. Eng. SE-12, 9, 890-904. Google Scholar
- ~KoYMASS, R. 1990. Specifying real-time properties with metric temporal logic. Real-time Syst. 2, ~ 4, 255-299. Google Scholar
- ~LEWlS, H. R. 1990. A logic of concrete time intervals. In Proceedings of the 5th Annual ~ Symposium on Logic in Computer Science. IEEE Computer Society Press, New York, pp. ~ 380-389.Google Scholar
- LICHTENSTEIN, O., AND PNUELI, A. 1985. Checking that finite-state concurrent programs satisfy ~ their linear specification. In Proceedings of the 12th Symposium on Principles of Programming ~ Languages (New Orleans, La., Jan. 14-16). ACM, New York, pp. 97-107. Google Scholar
- `MAN~A, Z., AND PNUELI, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: ~ Specification. Springer-Verlag, New York. Google Scholar
- ~OSTROFF, J. S. 1990. Temporal Logic of Real-time Systems. Research Studies Press, Taunton, UK. Google Scholar
- ~ROGERS, H. JR. 1967. Theory of Recursive Functions and Effective Computability. McGraw-Hill, ~ New York. Google Scholar
- ~SlSTLA, A. P., AND ~, E. M. 1985. The complexity of propositional linear temporal logics. ~ J. ACM 32, 3 (July), 733-749. Google Scholar
- THOMAS, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, ~ volume B, J. van Leeuwen, ed. Elsevier Science Publishers (North-Holland), Amsterdam, The ~ Netherlands, pp. 133-191. Google Scholar
Index Terms
- The benefits of relaxing punctuality
Recommendations
Regular model checking for LTL(MSO)
Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
Context-free timed formalisms: Robust automata and linear temporal logics
AbstractThe paper focuses on automata and linear temporal logics for real-time pushdown reactive systems bridging tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though ...
Presburger liveness verification of discrete timed automata
Using an automata-theoretic approach, we investigate the decidability of liveness properties (called Presburger liveness properties) for timed automata when Presburger formulas on configurations are allowed. While the general problem of checking a ...
Comments