A Finite Representation of Durational Action Timed Automata Semantics
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 p...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-12-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/12/24/4008 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1846103777884504064 |
|---|---|
| author | Ahmed Bouzenada Djamel Eddine Saidouni Gregorio Díaz |
| author_facet | Ahmed Bouzenada Djamel Eddine Saidouni Gregorio Díaz |
| author_sort | Ahmed Bouzenada |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-46388619dd9546228743de23ccb61dbe |
| institution | Kabale University |
| issn | 2227-7390 |
| language | English |
| publishDate | 2024-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj-art-46388619dd9546228743de23ccb61dbe2024-12-27T14:38:17ZengMDPI AGMathematics2227-73902024-12-011224400810.3390/math12244008A Finite Representation of Durational Action Timed Automata SemanticsAhmed Bouzenada0Djamel Eddine Saidouni1Gregorio Díaz2MISC Laboratory, University of Abdelhamid Mehri Constantine 2, Constantine 25016, AlgeriaMISC Laboratory, University of Abdelhamid Mehri Constantine 2, Constantine 25016, AlgeriaInstituto de Investigación en Informática, Escuela Superior de Ingeniería Informática, Universidad de Castilla-La Mancha, 02071 Albacete, SpainDurational 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.https://www.mdpi.com/2227-7390/12/24/4008timed automatareal-time systemsaction durationmaximality-based semantics |
| spellingShingle | Ahmed Bouzenada Djamel Eddine Saidouni Gregorio Díaz A Finite Representation of Durational Action Timed Automata Semantics Mathematics timed automata real-time systems action duration maximality-based semantics |
| title | A Finite Representation of Durational Action Timed Automata Semantics |
| title_full | A Finite Representation of Durational Action Timed Automata Semantics |
| title_fullStr | A Finite Representation of Durational Action Timed Automata Semantics |
| title_full_unstemmed | A Finite Representation of Durational Action Timed Automata Semantics |
| title_short | A Finite Representation of Durational Action Timed Automata Semantics |
| title_sort | finite representation of durational action timed automata semantics |
| topic | timed automata real-time systems action duration maximality-based semantics |
| url | https://www.mdpi.com/2227-7390/12/24/4008 |
| work_keys_str_mv | AT ahmedbouzenada afiniterepresentationofdurationalactiontimedautomatasemantics AT djameleddinesaidouni afiniterepresentationofdurationalactiontimedautomatasemantics AT gregoriodiaz afiniterepresentationofdurationalactiontimedautomatasemantics AT ahmedbouzenada finiterepresentationofdurationalactiontimedautomatasemantics AT djameleddinesaidouni finiterepresentationofdurationalactiontimedautomatasemantics AT gregoriodiaz finiterepresentationofdurationalactiontimedautomatasemantics |