{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T14:33:28Z","timestamp":1781102008420,"version":"3.54.1"},"reference-count":25,"publisher":"IGI Global Scientific Publishing","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,4,1]]},"abstract":"<p>The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.<\/p>","DOI":"10.4018\/ijertcs.2014040103","type":"journal-article","created":{"date-parts":[[2015,1,8]],"date-time":"2015-01-08T12:59:46Z","timestamp":1420721986000},"page":"22-42","source":"Crossref","is-referenced-by-count":1,"title":["True Concurrency Semantics"],"prefix":"10.4018","volume":"5","author":[{"given":"Souad","family":"Guellati","sequence":"first","affiliation":[{"name":"Universit\u00e9 Constantine II, Constantine, Algeria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilham","family":"Kitouni","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Constantine II, Constantine, Algeria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Riad","family":"Matmat","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Constantine II, Constantine, Algeria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Djamel-Eddine","family":"Saidouni","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Constantine II, Constantine, Algeria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"ijertcs.2014040103-0","doi-asserted-by":"crossref","unstructured":"Alpern, B., & Schneider, F.B. (1985). Defining liveness, 21(4): 181\u2013185.","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"ijertcs.2014040103-1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"ijertcs.2014040103-2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ijertcs.2014040103-3","first-page":"I","author":"C.Baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ijertcs.2014040103-4","doi-asserted-by":"publisher","DOI":"10.4018\/jertcs.2013040104"},{"key":"ijertcs.2014040103-5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9"},{"key":"ijertcs.2014040103-6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_5"},{"key":"ijertcs.2014040103-7","first-page":"119","article-title":"Time and action lock freedom properties for timed automata.","author":"H.Bowman","year":"2001","journal-title":"Proceedings of FORTE 2001"},{"key":"ijertcs.2014040103-8","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., & Emerson, E. A. (1981). Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. in Proceedings of IBM Workshop on Logics of Programs, 131, 52-71, Springer-Verlag.","DOI":"10.1007\/BFb0025774"},{"key":"ijertcs.2014040103-9","author":"E. M.Clarke","year":"2000","journal-title":"Model Checking"},{"key":"ijertcs.2014040103-10","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"ijertcs.2014040103-11","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0185-4"},{"key":"ijertcs.2014040103-12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_3"},{"key":"ijertcs.2014040103-13","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"ijertcs.2014040103-14","doi-asserted-by":"crossref","unstructured":"Kitouni, I., Hachichi, H., Bouaroudj, K., & Saidouni, D. E. (2012). Durational Actions Timed Automata: Determinization and Expressiveness. In International Journal of Applied Information Systems (IJAIS), Published by Foundation of Computer Science, 4 (2): 1-11.","DOI":"10.5120\/ijais12-450609"},{"key":"ijertcs.2014040103-15","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"S. A.Kripke","year":"1963","journal-title":"Acta Philosophica Fennica"},{"key":"ijertcs.2014040103-16","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"ijertcs.2014040103-17","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"ijertcs.2014040103-18","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (1977). The temporal logic of programs, In Proceeding of the 18th IEEE Symposium Foundations of Computer Science, FOCS\u201977, 46 - 57.","DOI":"10.1109\/SFCS.1977.32"},{"key":"ijertcs.2014040103-19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"ijertcs.2014040103-20","doi-asserted-by":"crossref","unstructured":"Rushby, J. M. (2001). Theorem Proving for Verification. In Proc. Modelling and verification of parallel processes, 2067, 39-57,LNCS, Springer-Verlag.","DOI":"10.1007\/3-540-45510-8_2"},{"key":"ijertcs.2014040103-21","article-title":"Actions duration in timed models.","author":"D. E.Saidouni","year":"2006","journal-title":"Proceedings of International Arab Conference on Information Technology (ACIT\u20192006)"},{"key":"ijertcs.2014040103-22","first-page":"6","article-title":"Aggregation of transitions in marking graph generation based on maximality semantics for Petri nets.","author":"D. E.Saidouni","year":"2008","journal-title":"Proceeding of the Second international conference on Verification and Evaluation of Computer and Communication Systems (VECoS\u201908)"},{"key":"ijertcs.2014040103-23","article-title":"Prise en compte des dur\u00e9es d\u2019action dans les alg\u00e8bres de processus par l\u2019utilisation de la s\u00e9mantique de maximalit\u00e9.","author":"D. E.Saidouni","year":"2003","journal-title":"Proceedings of CFIP\u20192003"},{"key":"ijertcs.2014040103-24","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"}],"container-title":["International Journal of Embedded and Real-Time Communication Systems"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=121727","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T17:55:18Z","timestamp":1654106118000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/ijertcs.2014040103"}},"subtitle":["Towards a Verification of Timed Systems"],"short-title":[],"issued":{"date-parts":[[2014,4,1]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"URL":"https:\/\/doi.org\/10.4018\/ijertcs.2014040103","relation":{},"ISSN":["1947-3176","1947-3184"],"issn-type":[{"value":"1947-3176","type":"print"},{"value":"1947-3184","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,1]]}}}