CFP last date
16 December 2024
Call for Paper
January Edition
IJAIS solicits high quality original research papers for the upcoming January edition of the journal. The last date of research paper submission is 16 December 2024

Submit your paper
Know more
The week's pick
Responsive image
Ordered Frequent Itemsets Matrix Based On Fp-Tree Structure And Apriori Algorithm

Abdulkader M. Al-Badani Abdualmajed A. Al-Khulaidi
Random Articles
Reseach Article

Durational Actions Timed Automata: Determinization and Expressiveness

by Ilham Kitouni, Hiba Hachichi, Kenza Bouarroudj, Djamel-eddine Saidouni
journal cover thumbnail

International Journal of Applied Information Systems
Foundation of Computer Science (FCS), NY, USA
Volume 4 - Number 2
Year of Publication: 2012
Authors: Ilham Kitouni, Hiba Hachichi, Kenza Bouarroudj, Djamel-eddine Saidouni
10.5120/ijais12-450609

Ilham Kitouni, Hiba Hachichi, Kenza Bouarroudj, Djamel-eddine Saidouni . Durational Actions Timed Automata: Determinization and Expressiveness. International Journal of Applied Information Systems. 4, 2 ( September 2012), 1-11. DOI=10.5120/ijais12-450609

@article{ 10.5120/ijais12-450609,
author = { Ilham Kitouni, Hiba Hachichi, Kenza Bouarroudj, Djamel-eddine Saidouni },
title = { Durational Actions Timed Automata: Determinization and Expressiveness },
journal = { International Journal of Applied Information Systems },
issue_date = { September 2012 },
volume = { 4 },
number = { 2 },
month = { September },
year = { 2012 },
issn = { 2249-0868 },
pages = { 1-11 },
numpages = {9},
url = { https://www.ijais.org/archives/volume4/number2/270-0609/ },
doi = { 10.5120/ijais12-450609 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2023-07-05T10:46:55.240417+05:30
%A Ilham Kitouni
%A Hiba Hachichi
%A Kenza Bouarroudj
%A Djamel-eddine Saidouni
%T Durational Actions Timed Automata: Determinization and Expressiveness
%J International Journal of Applied Information Systems
%@ 2249-0868
%V 4
%N 2
%P 1-11
%D 2012
%I Foundation of Computer Science (FCS), NY, USA
Abstract

In this paper we present durational actions timed automata, DATA*, as a sub class of timed automata. In the contrast of T. A, the underling semantic of DATA* is the maximality semantics which claim that actions have durations and true concurrency is captured differently from choice. DATA* model is in one hand useful for modeling and validating reel aspects of systems. In the other hand, it is determinizable and closed under all Boolean operations. As result, the language inclusion problem is decidable. Then, we compare a durational actions timed automata to event recording automata, which is a determinizable sub class of the classical timed automata. Next, we propose a simple framework to aggregate region of DATA* for reducing its space state. This study is based on an aggregation region automata procedure to reduce the combinatorial explosion of regions. Finally, we discuss equivalence and validation of systems.

References
  1. R. Alur , D. L. Dill, A theory of timed automata, Theoretical Computer Science, 126(2):183-235,1994.
  2. R. Alur, L. Fix, and T. A. Henzinger. Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science, 211(1–2):253–273, 1999.
  3. N. Belala, Timed Models and Interest in Formal Verification of Real-Time Systems. PHD's theses, Mentouri University, 25000 Constantine, Algeria, Jun 2010.
  4. F. Laroussinie, N. Markey, and P. Schnoebelen. Model checking timed automata with one or two clocks. In Proceedings of the 15th international Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 387–401. Springer, August 2004.
  5. S. Lasota and I. Walukiewicz. Alternating timed automata. ACM Trans. Comput. Logic, 9(2):1–27, 2008.
  6. J. Ouaknine and J. Worrell. On the language inclusion problem for timed automata: Closing a decidability gap. In LICS '04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pages 54–63, Washington, DC, USA, 2004.
  7. H. Hachichi, I . Kitouni, D. E. Saïdouni, "A Graph Grammar Approach for calculation of Aggregate Regions Automata", The International Arab Conference on Information Technology (ACIT), 2011, Naif Arab University for Security Science (NAUSS) Riyadh, Saudi Arabia (December 11-14, 2011).
  8. J. Ouaknine and J. Worrell. On the decidability of metric temporal logic. In LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, pages 188–197, Washington, DC, USA, 2005.
  9. I. Kitouni, Determinization of Timed Automata With Action Duration for Formal Test. Aggregation Master's thesis, Mentouri University, 25000 Constantine, Algeria, Jun 2008.
  10. P. A. Abdulla, J. Ouaknine, K. Quaas, and J. Worrell. Zone-based universality analysis for single-clock timed automata. In Proc. FSEN'07, IPM International Symposium on Fundamentals of Software Engineering, Lecture Notes in Computer Science 1790, pages 98–112. Springer-Verlag, 2007.
  11. P. V. Suman, P. K. Pandya, S. Narayanan Krishna L. Manasa. G: Determinization of Timed Automata with Integral Resets. Technical Report TIFR-PPVS-GM-2007.
  12. D. E. Saïdouni , J. P. Courtiat, " Prise en Compte des Durées d'Action dans les Algèbres de Processus par l'Utilisation de la Sémantique de Maximalité" ,In CFIP. 2003. Hermes, France, (2003).
  13. D. E. Saïdouni, N. Belala, " Actions duration in timed models", The International Arab Conference on Information Technology (ACIT), (2006).
  14. D. E. Saïdouni, I. Kitouni , H. Hachichi , Formalization of aggregated region automata associated to durational action timed automata. MISC REPORT 11001, Mentouri University, 25000 Constantine, Algeria, (2011).
  15. J. Springntveld, F. Vaandrager, P. D'Argenio , "Testing timed automata". Theoretical Computer Science, 254, (2001).
  16. R. Alur, C. Courcoubetis, and D. Dill, Model Checking in Dense Real-Time. Information and Computation, 104(1):2–34. (1993)
  17. B. Bérard, S. Haddad, and M. Sassolas. Interrupt Timed Automata: Verification and Expressiveness. Formal Methods in System Design, (2012).
  18. P. Bouyer, Forward Analysis of Updatable Timed Automata, Formal Methods in System Design, vol. 24, n°3, p. 281–320. (2004)
  19. S. Tripakis. Fault diagnosis for timed automata. In FTRTFT'02. LNCS 2469, Springer, 2002.
  20. P. V Suman, P. K. Pandya, S. N Krishna, and L. Manasa: Timed automata with integer resets: Language inclusion and expressiveness. In FORMATS, pages 78–92. Springer, (2008). LNCS 5215.
  21. H. Bowman and R. Gomez: Concurrency Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems. ISBN-10: 1-85233-895-4 ISBN-13: 978-1-85233-895-4 Springer-Verlag (2006).
  22. R. Barbuti, N. De Francesco, L. Tesei : Timed Automata with non-instantaneous Actions. Fundamenta Informaticae 46 (2001) 1–15 1, IOS Press.
  23. R. Alur, C. Courcoubetis, Halbwachs, N. , Dill, D. L. and Wong-Toi, H. Minimization of Timed Transition Systems. Proc. CONCUR 1992, Springer LNCS 630, 340–354.
  24. S. Tripakis, Folk theorems on the determinization and minimization of timed automata, in: Formal Modeling and Analysis of Timed Systems (FORMATS'03), in: Lecture Notes in Computer Science, vol. 2791, Springer, Berlin. (2004)
  25. I. Kitouni, H. Hachichi, D. E. Saidouni : A Simple Approach for Reducing Timed Automata. In: The 2nd IEEE International Conference on Information Technology and e-Services (ICITeS 2012). Sousse, Tunisia (March 24-26, 2012).
  26. R. Alur. Timed automata. In Nicolas Halbwachs and Doron Peled, editors, Proceedings of the 11th Internation Conference on Computer Aided Verification (CAV 1999), volume 1633 of Lecture Notes in Computer Science, pages 8–22. Springer-Verlag, 1999.
  27. B. Nielsen, , A. Skou,: Automated test generation from timed automata. In 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01. LNCS vol 2031, pp 343-357. Springer (2001).
  28. H. Hachichi, I. Kitouni, D. E. Saidouni. Transforming DATA* with Dotty Format to Aggregate Region Automaton. International Journal of Computer Applications,vol 37(10), pp 35-42 (2012).
  29. J. Ouaknine and J. Worrell, On the decidability and complexity of metric temporal logic over finite words. Logical Methods in Computer Science, 3(1:8). (2007).
  30. C. Baier, Bertrand, N. Bouyer, P. and Brihaye, T. When are timed automata determinizable? Seminaire LaBRI. (2009)
  31. M. Mao Zheng, V. Alagar and O. Ormandjieva, Automated generation of test suites from formal specifications of real-time reactive systems In The Journal of Systems and Software vol. 81 p. 286–304 (2008).
Index Terms

Computer Science
Information Sciences

Keywords

Formal timed models durational actions timed automata determinizable models expressiveness reduction approach

Powered by PhDFocusTM