×

zbMATH — the first resource for mathematics

A succinct canonical register automaton model. (English) Zbl 1304.68097
Summary: We present a novel canonical automaton model, based on register automata, that can be used to specify protocol or program behavior. Register automata have a finite control structure and a finite number of registers (variables), and process sequences of terms that carry data values from an infinite domain. We consider register automata that compare data values for equality. A major contribution is the definition of a canonical automaton representation of any language recognizable by a deterministic register automaton, by means of a Nerode congruence. This canonical form is well suited for modeling, e.g., protocols or program behavior. Our model can be exponentially more succinct than previous proposals, since it filters out ‘accidental’ relations between data values. This opens the way to new practical applications, e.g., in automata learning.
MSC:
68Q45 Formal languages and automata
Software:
XMPP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 183-235, (1994) · Zbl 0803.68071
[2] Angluin, D., Learning regular sets from queries and counterexamples, Inf. Comput., 75, 87-106, (1987) · Zbl 0636.68112
[3] Benedikt, M.; Ley, C.; Puppis, G., What you must remember when processing data words, (Laender, A. H.F.; Lakshmanan, L. V.S., AMW, CEUR Workshop Proceedings, vol. 619, (2010), CEUR-WS.org)
[4] Björklund, H.; Schwentick, T., On notions of regularity for data languages, Theor. Comput. Sci., 411, 702-715, (2010) · Zbl 1183.68240
[5] Bojanczyk, M.; David, C.; Muscholl, A.; Schwentick, T.; Segoufin, L., Two-variable logic on data words, ACM Trans. Comput. Log., 12, 27, (2011) · Zbl 1352.03041
[6] Bojanczyk, M.; Klin, B.; Lasota, S., Automata with group actions, (LICS, (2011), IEEE Computer Society), 355-364
[7] Bouyer, P., A logical characterization of data languages, Inf. Process. Lett., 84, 75-85, (2002) · Zbl 1042.68544
[8] Cassel, S.; Howar, F.; Jonsson, B.; Merten, M.; Steffen, B., A succinct canonical register automaton model, (Bultan, T.; Hsiung, P. A., ATVA, LNCS, vol. 6996, (2011), Springer), 366-380 · Zbl 1348.68095
[9] Cassel, S.; Jonsson, B.; Howar, F.; Steffen, B., A succinct canonical register automaton model for data domains with binary relations, (Chakraborty, S.; Mukund, M., ATVA, LNCS, vol. 7561, (2012), Springer), 57-71 · Zbl 1374.68256
[10] Francez, N.; Kaminski, M., An algebraic characterization of deterministic regular languages over infinite alphabets, Theor. Comput. Sci., 306, 155-175, (2003) · Zbl 1059.68059
[11] Gold, E. M., Language identification in the limit, Inf. Control, 10, 447-474, (1967) · Zbl 0259.68032
[12] Hopcroft, J. E.; Ullman, J. D., Introduction to automata theory, languages and computation, (1979), Addison-Wesley · Zbl 0426.68001
[13] Howar, F.; Steffen, B.; Jonsson, B.; Cassel, S., Inferring canonical register automata, (Kuncak, V.; Rybalchenko, A., VMCAI, LNCS, vol. 7148, (2012), Springer), 251-266 · Zbl 1326.68168
[14] Kaminski, M.; Francez, N., Finite-memory automata, Theor. Comput. Sci., 134, 329-363, (1994) · Zbl 0938.68711
[15] Kanellakis, P. C.; Smolka, S. A., CCS expressions, finite state processes, and three problems of equivalence, Inf. Comput., 86, 43-68, (1990) · Zbl 0705.68063
[16] Lazic, R.; Nowak, D., A unifying approach to data-independence, (Palamidessi, C., CONCUR, LNCS, vol. 1877, (2000), Springer), 581-595 · Zbl 0999.68126
[17] Nerode, A., Linear automaton transformations, Proc. Am. Math. Soc., 9, 541-544, (1958) · Zbl 0089.33403
[18] Paige, R.; Tarjan, R. E., Three partition refinement algorithms, SIAM J. Comput., 16, 973-989, (1987) · Zbl 0654.68072
[19] Petrenko, A.; Boroday, S.; Groz, R., Confirming configurations in EFSM testing, IEEE Trans. Softw. Eng., 30, 29-42, (2004) · Zbl 0952.68092
[20] Rivest, R. L.; Schapire, R. E., Inference of finite automata using homing sequences, Inf. Comput., 103, 299-347, (1993) · Zbl 0786.68082
[21] P. Saint-Andre, Extensible Messaging and Presence Protocol (XMPP): Instant Messaging and Presence, RFC 6121 (Proposed Standard), 2011.
[22] Segoufin, L., Automata and logics for words and trees over an infinite alphabet, (Ésik, Z., CSL, LNCS, vol. 4207, (2006), Springer), 41-57 · Zbl 1225.68103
[23] Wilke, T., Specifying timed state sequences in powerful decidable logics and timed automata, (Langmaack, H.; de Roever, W. P.; Vytopil, J., FTRTFT, LNCS, vol. 863, (1994), Springer), 694-715
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.