Commutative Data Automata

Title: Commutative Data Automata
Speaker: Dr. Zhilin Wu (State Key Laboratory of Computer Science, ISCAS)
Time: 14:30, Thursday, May 10, 2012
Venue: Lecture room, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract: With momenta from XML document processing and verification of infinite-state
systems, formalisms over infinite alphabets have recently received much focus in the community of theoretical computer science.

Data automata is a formal model for words over infinite alphabets, which are the product of a finite set of labels and an infinite set of data values, proposed by Bojanczyk, Muscholl, Schwentick et. al. in 2006. A data automaton consists of two parts, a nondeterministic letter-to-letter transducer, and a class condition specified by a finite automaton over the output alphabet of the transducer, which acts as a condition on the subsequence of the outputs of the transducer in every class, namely, in every maximal set of positions with the same data value.

It is open whether the nonemptiness of data automata can be decided with elementary complexity, since the reachability problem of petri nets can be easily reduced to this problem. Very recently, a restriction of data automata with elementary complexity, called weak data automata, was proposed by Kara, Schwentick and Tan and its nonemptiness problem was shown to be in 2-NEXPTIME.  In weak data automata, the class conditions are specified by some simple constraints on the number of occurrences of labels occurring in every class.

The aim of this talk is to demonstrate that the commutativity of class conditions is the genuine reason accounting for the elementary complexity of weak data automata.

For this purpose, we define and investigate commutative data automata, which are data automata with class conditions restricted to commutative regular languages. We show that while the expressive power of commutative data automata is strictly stronger than that of weak data automata, the nonemptiness problem of this model can still be decided with elementary complexity, more precisely, in 3-NEXPTIME. In addition, we extend the results to data Omega-words and prove that the nonemptiness of commutative Buchi data automata can be decided in 4-NEXPTIME. We also provide logical characterizations for commutative (Buchi) data automata, similar to those for weak (Buchi) data automata.

Bio:
Zhilin Wu is an assistant researcher in SKLCS-ISCAS (State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences). His major research interests include automata and logic over infinite alphabets, and verification of infinite-state systems.

He obtained the Phd. Degree in 2007 from SKLCS-ISCAS. After that, he became a postdoc in the Netquest group of LIAMA (Sino-French Laboratory for computer science, automation and applied mathematics). From 2009 to 2010, he was a postdoc in the formal methods group of LaBRI, University Bordeaux 1. In August of 2010, he joined SKLCS-ISCAS and became an assistant researcher.

http://lcs.ios.ac.cn/~wuzl