What is this about? This server accepts the description of a regular language via a (nondeterministic) automaton (see Format for automata) and the description of a language property via a transducer (see Format for transducers), or via a trajectory automaton (see Format for trajectory sets), and returns YES/NO, depending on whether the language satisfies the property. Moreover, if the answer is NO, the server also returns two words of the language violating the desired property -- this capability was suggested in [4]. Examples of properties are: prefix code, suffix code, infix code, outfix code, hypercode, thin language, etc. [6,5,3]. Each of these properties can be described via a transducer or, with few exceptions, via a regular expression over {0, 1} (a trajectory expression).
Regular trajectory properties [2] A regular expression e over {0, 1} describes the following property. All languages L in which no two words are related as expressed in e. In particular, when the zeros in e represent positions of a word v in L, then there can be no other word in L containg v as expressed in e. For example, 0*1* describes the prefix code property, since a prefix code cannot have a word u containing another word v as a prefix (v as 0* and u as 0*1*). Similarly, 1*0* describes the suffix code property.
Transducer properties [1] A transducer t describes the following property. All languages L such that
t(L) ∩ L = EmptySet
that is, on any input word from L, the transducer t will never return a word in L. For example, the prefix code property can be described by a transducer that, on input w, returns all proper prefixes of w -- see Format for transducers for more details.
A limit: Depending on the sizes of the automaton and the transducer, the underlying decision program could do a great deal of processing before it returns the YES/NO answer. Currently, the program could interrupt the computation and halt if the quantity N*N*M exceeds 500000, where N and M are the numbers of transitions in the automaton and transducer, respectively.
Future plans: Given a property and a number N, return a language of at least N words satisfying the given property.
Some References -- see [1] for more.
[1] K. Dudzinski and S. Konstantinidis. On formal descriptions of code properties. Presented at DCFS 2010. See also here for a technical report version.