In this work, we address the problem of verifying a Timed Automaton for a real-time property written in Duration Calculus in the form of Linear Duration Invariants. We present a conservative method for solving the problem using the linear programming techniques. First, we provide a procedure to translate Timed Automata into a sort of regular expressions for timed languages. Then, we extend the linear programming-based approaches in [10] to this algebraic notation for the timed automata. Our results in this paper are more general than the ones presented in [10]. Namely, Timed Automata are our starting point, and we can provide an accurate answer to the problem for a larger class of them.
| Documento: | Conferencia |
| Título: | On checking timed automata for linear duration invariants |
| Autor: | Braberman, Victor Adrian; Van Hung, Dang |
| Ciudad: | Piscataway, NJ, United States; Madrid, Spain |
| Filiación: | FCEyN-UBA, Argentina |
| Palabras clave: | Algebra; Linear programming; Real time systems; Duration calculus; Linear duration invariants; Timed automata; Automata theory |
| Año: | 1998 |
| Página de inicio: | 264 |
| Página de fin: | 273 |
| Título revista: | Proceedings of the 1998 19th IEEE Real-Time Systems Symposium |
| Título revista abreviado: | Proc Real Time Syst Symp |
| CODEN: | PRSYE |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS02738_v_n_p264_Braberman |
