A Nonarchimedian Discretization for Timed Languages

• Autorzy: Dima C.

Identyfikatory

DOI

10.3233/FI-2014-1021

• Języki publikacji: EN

Abstrakty

EN

We give a discretization of behaviors of timed automata, in which timed languages are represented as sets of words containing action symbols, a clock tick symbol 1, and two delay symbols δ⁻ (negative delay) and δ⁺ (positive delay). Unlike the region construction, our discretization commutes with intersection. We show that discretizations of timed automata are, in general, context-sensitive languages over Σ ∪ {1, δ⁺, δ⁻}, and give a class of counter automata that accepts exactly the class of languages that are discretizations of timed automata, and show that its emptiness problem is decidable.

Słowa kluczowe

EN

discretization method; programming languages; machine theory; set theory; computer science

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 131, nr 3-4
• Strony: 389--407
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

Dima C.

• Université Paris-Est, LACL (EA 4219), UPEC, 61 avenue du Général de Gaulle, 94010 Créteil Cedex, France

Bibliografia

• [1] Alur, R., Dill, D.: A theory of timed automata, Theoretical Computer Science, 126, 1994, 183–235.
• [2] Asarin, E.: Challenges in timed languages, Bulletin of EATCS, 83, 2004, 106–120.
• [3] Asarin, E., Caspi, P., Maler, O.: Timed regular expressions, Journal of the ACM, 49, 2002, 172–206.
• [4] Asarin, E., Dima, C.: Balanced timed regular expressions, Electronic Notes in Theoretical Computer Science, 68, 2002, 1–18.
• [5] Beauquier, D.: Pumping Lemmas for Timed Automata, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure (FoSSaCS’98), LNCS 1378, 1998, 81–94.
• [6] Bouyer, P., Petit, A.: Decomposition and composition of timed automata, Proceedings of 26th International Colloquium on Automata, Languages and Programming (ICALP’99), LNCS 1644, 1999, 210–219.
• [7] Bouyer, P., Petit, A.: A Kleene/Büchi-like theorem for clock languages, Journal of Automata, Languages and Combinatorics, 7(2), 2002, 167–186.
• [8] Bouyer, P., Petit, A., Th´erien, D.: An algebraic characterization of data and timed languages, Proceedings of the 12th International Conference on Concurrency Theory (CONCUR’2001), LNCS 2154, 2001, 248–261.
• [9] Dima, C.: Th´eorie alg´ebrique des langages formels temps r´eel, Ph.D. Thesis, Universit´e Joseph Fourier Grenoble, France, 2001.
• [10] Dima, C.: Computing reachability relations in timed automata, Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS’02), 2002, 177–186.
• [11] Dima, C.: A class of automata for computing reachability relations in timed systems, in: Proceedings of the NATO Advanced Research Workshop on Verification of Infinite State Systems with Applications to Security (VISSAS’05) (E. Clarke, M. Minea, F. L. T¸ iplea, Eds.), NATO ARW Series, IOS Press, 2006, 69–89.
• [12] D’Souza, D., Thiagarajan, P. S.: Product Interval Automata: A Subclass of Timed Automata, Proceedings of the 19th Conference on the Foundations of Software Technology and Theoretical Computer Science FSTTCS’99), 1738, 1999, 60–71.
• [13] Herrmann, P.: Timed Automata and Recognizability, Information Processing Letters, 65, 1998, 313–318.
• [14] Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages and Computation, Addison-Wesley/Narosa Publishing House, 1992.
• [15] Larsen, K. G., Pettersson, P., Yi,W.: UPPAAL: Status & Developments, Proceedings of the 9th International Conference on Computer Aided Verification (CAV’97), LNCS 1254, 1997, 456–459.
• [16] Yovine, S.: Model-checking timed automata, Lectures on Embedded Systems (G. Rozenberg, F. Vaandrager, Eds.), LNCS 1494, 1998, 114–152.