IDEAS home Printed from https://ideas.repec.org/a/gam/jmathe/v12y2024i24p4008-d1548815.html
   My bibliography  Save this article

A Finite Representation of Durational Action Timed Automata Semantics

Author

Listed:
  • 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)

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.

Suggested Citation

  • Ahmed Bouzenada & Djamel Eddine Saidouni & Gregorio Díaz, 2024. "A Finite Representation of Durational Action Timed Automata Semantics," Mathematics, MDPI, vol. 12(24), pages 1-20, December.
    • Handle: RePEc:gam:jmathe:v:12:y:2024:i:24:p:4008-:d:1548815
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/2227-7390/12/24/4008/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/2227-7390/12/24/4008/
    Download Restriction: no
    ---><---

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:gam:jmathe:v:12:y:2024:i:24:p:4008-:d:1548815. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: MDPI Indexing Manager (email available below). General contact details of provider: https://www.mdpi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.