A Finite Representation of Durational Action Timed Automata Semantics

Ahmed Bouzenada, Djamel Eddine Saidouni and Gregorio Díaz ()
Additional contact information
Ahmed Bouzenada: MISC Laboratory, University of Abdelhamid Mehri Constantine 2, Constantine 25016, Algeria
Djamel Eddine Saidouni: MISC Laboratory, University of Abdelhamid Mehri Constantine 2, Constantine 25016, Algeria
Gregorio Díaz: Instituto de Investigación en Informática, Escuela Superior de Ingeniería Informática, Universidad de Castilla-La Mancha, 02071 Albacete, Spain

Mathematics, 2024, vol. 12, issue 24, 1-20

Abstract: Durational action timed automata (daTAs) are state transition systems like timed automata (TAs) that capture information regarding the concurrent execution of actions and their durations using maximality-based semantics. As the underlying semantics of daTAs are infinite due to the modeling of time progress, conventional model checking techniques become impractical for systems specified using daTAs. Therefore, a finite abstract representation of daTA behavior is required to enable model checking for such system specifications. For that, we propose a finite abstraction of the underlying semantics of a daTA-like region abstraction of timed automata. In addition, we highlight the unique benefits of daTAs by illustrating that they enable the verification of properties concerning concurrency and action duration that cannot be verified using the traditional TA model. We demonstrate mathematically that the number of states in durational action timed automata becomes significantly smaller than the number of states in timed automata as the number of actions increases, confirming the efficiency of daTAs in modeling behavior with action durations.

Keywords: timed automata; real-time systems; action duration; maximality-based semantics (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2024
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/12/24/4008/pdf (application/pdf)
https://www.mdpi.com/2227-7390/12/24/4008/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:12:y:2024:i:24:p:4008-:d:1548815

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().