On checking timed automata for linear duration invariants

Mostrar todas las versiones(2)

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 tran...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, Victor Adrian, Van Hung, Dang
Formato: CONF
Materias:
Algebra
Linear programming
Real time systems
Duration calculus
Linear duration invariants
Timed automata
Automata theory
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_NIS02738_v_n_p264_Braberman
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_NIS02738_v_n_p264_Braberman
record_format dspace
spelling todo:paper_NIS02738_v_n_p264_Braberman2023-10-03T16:45:44Z On checking timed automata for linear duration invariants Braberman, Victor Adrian Van Hung, Dang Algebra Linear programming Real time systems Duration calculus Linear duration invariants Timed automata Automata theory 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. Fil:Braberman, Victor Adrian Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_NIS02738_v_n_p264_Braberman
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Algebra
Linear programming
Real time systems
Duration calculus
Linear duration invariants
Timed automata
Automata theory
spellingShingle Algebra
Linear programming
Real time systems
Duration calculus
Linear duration invariants
Timed automata
Automata theory
Braberman, Victor Adrian
Van Hung, Dang
On checking timed automata for linear duration invariants
topic_facet Algebra
Linear programming
Real time systems
Duration calculus
Linear duration invariants
Timed automata
Automata theory
description 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.
format CONF
author Braberman, Victor Adrian
Van Hung, Dang
author_facet Braberman, Victor Adrian
Van Hung, Dang
author_sort Braberman, Victor Adrian
title On checking timed automata for linear duration invariants
title_short On checking timed automata for linear duration invariants
title_full On checking timed automata for linear duration invariants
title_fullStr On checking timed automata for linear duration invariants
title_full_unstemmed On checking timed automata for linear duration invariants
title_sort on checking timed automata for linear duration invariants
url http://hdl.handle.net/20.500.12110/paper_NIS02738_v_n_p264_Braberman
work_keys_str_mv AT brabermanvictoradrian oncheckingtimedautomataforlineardurationinvariants
AT vanhungdang oncheckingtimedautomataforlineardurationinvariants
_version_ 1807323908752277504

Ejemplares similares