This is work I mostly did during my Ph.D. thesis although some is quite recent (e.g., last timed Buchi automata paper). The goal has been to develop and improve model-checking and controller-synthesis techniques for timed automata. Most of this work has been implemented in the model-checkers Kronos and Open-Kronos.

Related papers (read the copyright note)

1. S. Tripakis. Checking Timed Buchi Automata Emptiness on Simulation Graphs. In ACM Transactions on Computational Logic. PDF.


2. S. Tripakis, S. Yovine and A. Bouajjani. Checking Timed Buchi Automata Emptiness Efficiently. In Formal Methods in System Design, 26(3):267-292, May 2005. PDF.


3. K. Altisen and S. Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. PDF.


4. S. Tripakis and S. Yovine. Analysis of Timed Systems using Time-abstracting Bisimulations. In Formal Methods in System Design, 18(1):25-68, January 2001. Kluwer Academic Publishers. Postscript.


5. P. Niebert, S. Tripakis and S. Yovine. Minimum-Time Reachability for Timed Automata. In Mediterranean Conference on Control and Automation, 2000. Postscript.


6. K. Altisen, G. Goessler, A. Pnueli, J. Sifakis, S. Tripakis and S. Yovine. A Framework for Scheduler Synthesis. In IEEE Real-Time Systems Symposium, RTSS'99, 1999. Postscript.


7. S. Tripakis and K. Altisen. On-the-Fly Controller Synthesis for Discrete and Timed Systems. In World Congress on Formal Methods, FM'99, 1999. Postscript.


8. M. Bozga, O. Maler and S. Tripakis. Efficient Verification of Timed Automata using Dense and Discrete Time Semantics. In CHARME'99, 1999. Postscript.


9. S. Tripakis. Verifying Progress in Timed Systems. In ARTS'99, Bamberg, Germany, 1999. Postscript.


10. S. Tripakis. Timed Diagnostics for Reachability Properties. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'99, Amsterdam, Holland, 1999. Postscript.


11. S. Tripakis and S .Yovine. Verification of the Fast-Reservation Protocol with Delayed Transmission using the tool Kronos. In 4th IEEE Real-Time Technology and Applications Symposium, RTAS'98, Denver, Colorado, 1998. Postscript.


12. M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. KRONOS: a model-checking tool for real-time systems. In Computer Aided Verification, CAV'98, 1998. Postscript.


13. C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'98, Lisbon, Portugal, LNCS 1384, 1998. Postscript.


14. S. Bornot, J. Sifakis and S. Tripakis. Modeling Urgency in Timed Systems. In Compositionality: the significant difference, COMPOS'97, LNCS 1536. Postscript.


15. A. Bouajjani, S. Tripakis and S. Yovine. On-the-fly Symbolic Model checking for Real-time Systems. In 18th IEEE Real-Time Systems Symposium, RTSS'97, San Francisco, CA, 1997. Postscript.


16. S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Computer-Aided Verification, CAV'96, Rutgers, NJ, LNCS 1102, 1996. PDF.


17. C. Daws, A. Olivero, S. Tripakis and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, LNCS 1066, 1996. PDF.


18. S. Tripakis and C. Courcoubetis. Extending PROMELA and SPIN for Real Time. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'96, Passau, Germany, LNCS 1055, 1996. PDF.


19. S. Tripakis. The analysis of timed systems in practice, PhD thesis, December 1998. Joseph Fourier University, Grenoble, France. In full (about 200 pages). In half (about 100 pages, saves paper). Slides (in Powerpoint format).

Back to home page of Stavros Tripakis