×

On pebble automata for data languages with decidable emptiness problem. (English) Zbl 1208.68142

Summary: We study a subclass of pebble automata (PA) for data languages for which the emptiness problem is decidable. Namely, we show that the emptiness problem for weak 2-pebble automata is decidable, while the same problem for weak 3-pebble automata is undecidable. We also introduce the so-called top view weak PA. Roughly speaking, top view weak PA are weak PA where the equality test is performed only between the data values seen by the two most recently placed pebbles. The emptiness problem for this model is still decidable. It is also robust: alternating, non-deterministic and deterministic top view weak PA have the same recognition power; and are strong enough to accept all data languages expressible in Linear Temporal Logic with the future-time operators, augmented with one register freeze quantifier.

MSC:

68Q45 Formal languages and automata
03B25 Decidability of theories and sets of sentences
03D05 Automata and formal grammars in connection with logical questions
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, Parosh Aziz; Jonsson, Bengt; Nilsson, Marcus; Saksena, Mayank, A survey of regular model checking, (Proceedings of the 15th International Conference on Concurrency Theory (CONCUR) 2004. Proceedings of the 15th International Conference on Concurrency Theory (CONCUR) 2004, Lecture Notes in Comput. Sci., vol. 3170 (2004), Springer), 35-48 · Zbl 1099.68055
[2] Arenas, Marcelo; Fan, Wenfei; Libkin, Leonid, Consistency of XML specifications, (Inconsistency Tolerance [Dagstuhl Seminar]. Inconsistency Tolerance [Dagstuhl Seminar], Lecture Notes in Comput. Sci., vol. 3300 (2005), Springer), 15-41 · Zbl 1111.68662
[3] Björklund, Henrik; Schwentick, Thomas, On notions of regularity for data languages, (Proceedings of the 16th International Symposium on Fundamentals of Computation Theory (FCT) 2007. Proceedings of the 16th International Symposium on Fundamentals of Computation Theory (FCT) 2007, Lecture Notes in Comput. Sci., vol. 4639 (2007), Springer), 88-99 · Zbl 1135.68451
[4] Bojanczyk, Mikolaj; Muscholl, Anca; Schwentick, Thomas; Segoufin, Luc; David, Claire, Two-variable logic on words with data, (Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS) 2006 (2006), IEEE Computer Society), 7-16 · Zbl 1352.03041
[5] Bojanczyk, Mikolaj; Samuelides, Mathias; Schwentick, Thomas; Segoufin, Luc, Expressive power of pebble automata, (Proceedings of Automata, Languages and Programming, 33rd International Colloquium (ICALP) 2006. Proceedings of Automata, Languages and Programming, 33rd International Colloquium (ICALP) 2006, Lecture Notes in Comput. Sci., vol. 4051 (2006), Springer), 157-168 · Zbl 1223.68065
[6] Demri, Stéphane; Lazic, Ranko, LTL with the freeze quantifier and register automata, (Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS) 2006 (2006), IEEE Computer Society), 17-26 · Zbl 1351.68158
[8] Hopcroft, John; Ullman, Jeffrey, Introduction to Automata Theory, Languages and Computation (1979), Addison-Wesley · Zbl 0426.68001
[9] Kaminski, Michael; Francez, Nissim, Finite-memory automata, Theoret. Comput. Sci., 134, 2, 329-363 (1994) · Zbl 0938.68711
[10] Kaminski, Michael; Tan, Tony, A note on two-pebble automata over infinite alphabets, Fund. Inform., 98, 4, 379-390 (2010) · Zbl 1200.03026
[11] Mayr, Richard, Undecidable problems in unreliable computations, Theoret. Comput. Sci., 297, 1-3, 337-354 (2003) · Zbl 1044.68119
[12] Neven, Frank, Automata, logic, and XML, (Proceedings of the 11th Annual Conference of the EACSL Computer Science Logic (CSL) 2002. Proceedings of the 11th Annual Conference of the EACSL Computer Science Logic (CSL) 2002, Lecture Notes in Comput. Sci., vol. 2471 (2002), Springer), 2-26 · Zbl 1020.68044
[13] Neven, Frank; Schwentick, Thomas; Vianu, Victor, Finite state machines for strings over infinite alphabets, ACM Trans. Comput. Log., 5, 3, 403-435 (2004) · Zbl 1367.68175
[14] Schnoebelen, Philippe, Verifying lossy channel systems has nonprimitive recursive complexity, Inform. Process. Lett., 83, 5, 251-261 (2002) · Zbl 1043.68016
[15] Segoufin, Luc, Automata and logics for words and trees over an infinite alphabet, (Proceedings of the 15th Annual Conference of the EACSL Computer Science Logic (CSL) 2006. Proceedings of the 15th Annual Conference of the EACSL Computer Science Logic (CSL) 2006, Lecture Notes in Comput. Sci., vol. 4207 (2006), Springer), 41-57 · Zbl 1225.68103
[16] Tan, Tony, Graph reachability and pebble automata over infinite alphabets, (Proceedings of the 24th IEEE Symposium on Logic in Computer Science (LICS) 2009 (2009), IEEE Computer Society), 157-166 · Zbl 1353.68172
[17] Tan, Tony, On pebble automata for data languages with decidable emptiness problem, (Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science (MFCS) 2009. Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science (MFCS) 2009, Lecture Notes in Comput. Sci., vol. 5734 (2009), Springer), 712-723 · Zbl 1200.68150
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.