I-LaSer

(Independent Language Server, v.4)

v.4 released in Oct. 2016; some things need to be fixed

I-LaSer answers questions about regular languages and independent properties---prefix code property, suffix code property,..., various error-detection and error-correction properties.
  • Satisfaction question: Given language L and property P, does L satisfy P?
  • Maximality question: Given language L and property P, is L maximal with respect to P?
  • Construction question: Given property P and integers N,k>0, return a language of N words of length k satisfying P.
Quick Notes (click on the "Technical Notes" tab for details): Languages are provided by automata; properties are either fixed, or provided by transducers or trajectory expressions. The alphabets of the given property and the language involved must be the same. The computation of the Construction question produces languages over an alphabet of the form {0,1,...,s} with 0< s < 10. For online-computation (via "Submit Request") the sizes of the automata and transducers involved are limited.
Which question do you want us to solve?

Input below the integers for the Construction question:
S (# of digits in the alphabet)
N (# of words to construct)
L (length of these words)

     

SOME TECHNICAL NOTES

What is this about? This server accepts the description of a regular language via a finite automaton and the description of a language property, and returns YES/NO, depending on whether the language satisfies the property. In case the answer is NO, appropriate counterexamples (also called witness words) are provided. If the language satisfies the property, the server can also return YES/NO, depending on whether the language is maximal with respect to the property. The Maximality question is PSPACE-hard. In the case of the Construction question [10], I-LaSer accepts the description of a property and three positive integers s, N, k, and generates a language of (up to) N words of length k satisfying the given property. The integer s must be less than 10 and specifies that the alphabet must be {'0','1',...,'s'}. See further below how to describe properties.

Online computation VS Program generation: When a user specifies a question to solve and the required input, ILaSer either computes the answer in real time, if the user clicks on "Submit Request", or it produces a zip file containing a self contained Python2.7 executable file, if the user clicks on "Generate Program". In the latter case, the executable file can produce the answer on the user's local machine.
Limits on online computations: Depending on the sizes of the given automaton and transducer, the underlying software could perform a great deal of processing before it returns an answer. For this reason, the following limits on processing requests are enforced.
  • Requests for the Satisfaction question are not processed, if the quantity N*N*M exceeds 500,000, where N and M are the numbers of transitions in the automaton and transducer, respectively.
  • Requests for the Construction question are not processed, if the quantity N*N*L*M exceeds 500,000, where N is the requested number of words, L is the requested length of these words, and M is, either the number of transitions in the transducer describing the property, or M=1 if the property is fixed.

Properties Examples of language properties are: prefix code, infix code, 1-substitution-error-detecting language [6,5,3]. These are examples of independences (independent properties). Roughly speaking, a language satisfies an independence if every subset of the language also satisfies that independence. Many independent properties have the following characteristic: a language L satisfies the property P if there are NO different words u,v in L such that v can result by performing a certain word operation on u--this word operation is what defines the property P. For example, prefix codes are defined by the word operation of removing any nonempty ending of the word u; and 1-substitution-detecting languages are defined by the operation that changes exactly 1 symbol in the word u. Certain transducers can conveniently be used to realize such operations, and we say that each such transducer describes a property. The method of trajectories is more limited in describing independences, but the descriptions are much simpler. I-LaSer supports the following independent properties.

  • Fixed properties These are (uniquely decipherable/decodable) code, prefix code, suffix code, infix code, outfix code, hypercode.
  • 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.
  • Input-altering Transducer properties [1] A transducer t is a nondeterministic automaton with output such that t(w) = the set of possible output words of t when the input is the word w. Note that t(w) could be empty for some words w. An input-altering transducer is one such that, for any input word w, the output is never equal to w. An input-altering transducer t describes the following property. All languages L such that t(L) ∩ L = EmptySet that is, the transducer t cannot take as input an L-word and also output an L-word. For example, the prefix code property can be described via a transducer that, on input w, returns all proper prefixes of w---see Format for transducers for more details.
  • Error-detecting properties [1,9] Such a property is described by an input-preserving transducer t as follows. All languages L such that y in t(x) implies y=x, for any words x, y in L; that is, on any input word x from L, the transducer t will never output another word in L. An input-preserving transducer, also called channel, is a transducer t that, on any input word w for which t(w) is nonempty, the set t(w) includes w; thus, t acts as a communication channel that receives a word w and can always return w (case of no error) or posiibly a word other than w (case of error). For example, the 1-subsitution-detection property can be described by a transducer that, on input w, returns either w or any word that obtains by changing 1 symbol of w---see Format for transducers for examples.
  • Error-correcting properties [9] Such a property is described by an input-preserving transducer t as follows. All languages L such that w in t(x) and w in t(y) implies y=x, for any words x, y in L and any word w; that is, the transducer cannot turn two different input words x, y from L into the same word. For example, the 1-subsitution-correction property can be described by a transducer that, on input w, returns either w or any word that obtains by changing 1 symbol of w.

Implementation: Based on FAdo, a set of Python libraries, which includes modules for automata, transducers, and code properties.

Some References

[1] K. Dudzinski and S. Konstantinidis. Formal descriptions of code properties: decidability, complexity, implementation. International Journal of Foundations of Computer Science 23:1 (2012), 67--85. Presented at DCFS 2010.
[2] M. Domaratzki. Trajectory-Based Codes. Acta Informatica, vol. 40, n. 6-7 (2004) 491-527.
[3] H. Jurgensen and S. Konstantinidis. Codes: In G. Rozenberg, A. Salomaa (eds): Handbook of Formal Languages, vol. I, 511-607. Springer-Verlag, Berlin, 1997.
[4] Jurgen Dassow. Comment following the presentation in [1].
[5] H.J. Shyr. Free monoids and languages. Hon Min Book Company, Taichung, Taiwan, 1991.
[6] H.J. Shyr and G. Thierrin. Codes and binary relations. Seminaire d'Algebre Paul Dubreil, Paris 1975--1976 (29\`eme Ann\'ee), Lecture Notes in Mathematics, 586, 1977, 180--188.
[7] FAdo: Tools for Formal Languages manipulation.
[8] Andre Almeida, Marco Almeida, Jose Alves, Nelma Moreira, and Rogerio Reis. Fado and guitar: tools for automata manipulation and visualization. In S. Maneth, editor, CIAA 2009: Fourteenth International Conference on Implementation and Application of Automata, volume 5642 of Lecture Notes on Computer Science, pages 65-74, Sydney, Australia, July 2009. Springer-Verlag.
[9] Konstantinidis S, Meijer C, Moreira N, Reis R. (2016). Implementation of Code Properties via Transducers. Lecture Notes in Computer Science 9705. 21st International Conference on the Implementation and Application of Automata (CIAA 2016), Seoul, Korea, Republic of (189-201). ArXiv version: Symbolic manipulation of code properties. arXiv:1504.04715v1, 2015
[10] Konstantinidis S, Moreira N, Reis R. (2016). Generating Error Control Codes with Automata and Transducers. OCG Proceedings. 8th Workshop on Non-Classical Models of Automata and Applications, Debrecen, Hungary.

ABOUT I-LaSer

(Names of I-LaSer versions are those of research students who contributed to their implementation)

Project initiator: Stavros Konstantinidis (http://cs.smu.ca/~stavros/)
-
Significant contributors:
Nelma Moreira & Rogerio Reis: as of version 3, LaSer's back end is based on FAdo
-
4: Abisola Adeniran (October 2016, current version)
Incorporating into LaSer the construction problem.
-
3: Casey Meijer (June 2014)
Deciding maximality of all available properties, generation of executable code
-
2: Meng Yang (June 2012)
Deciding satisfaction of: Input-preserving transducer, Error-detection, and Error-correction properties
-
1: Krystian Dudzinski (June 2010)
Deciding satisfaction of: Trajectory and Input-altering transducer properties

Format for Automata

One can use the Grail and FAdo formats for nondeterministic finite automata (those with nonempty transitions). The format of FAdo files must be as follows:
1. '#' begins a comment
2. @NFA, or @DFA, begins a new automaton (and determines its type) and must
     be followed by the list of the final states separated by blanks
3. Transitions are written one per line and consist of three fields separated by blanks: "state" "symbol" "new state"
4. The source state of the first transition is the initial state.


Here is an example of an automaton accepting ab* using both, Grail and FAdo formats:


Grail:                  FAdo:

(START) |- 1            @NFA 2
1 a 2                   1 a 2
2 b 2                   2 b 2
2 -| (FINAL)

More examples follow:

Automaton accepting aaa(aaa)*b + aa(ba)*a(aa(ba)*a)*b:

Grail:                  FAdo:

(START) |- 1            @NFA 8
1 a 2                   1 a 2
2 a 3                   2 a 3
3 b 2                   3 b 2
3 a 4                   3 a 4
4 a 2                   4 a 2
4 b 8                   4 b 8
1 a 5                   1 a 5
5 a 6                   5 a 6
6 a 7                   6 a 7
7 a 5                   7 a 5
7 b 8                   7 b 8
8 -| (FINAL)

Automaton accepting ab + bba:

Grail:                  FAdo:

(START) |- 1            @NFA 3
1 a 2                   1 a 2
2 b 3                   2 b 3
1 b 4                   1 b 4
4 b 5                   4 b 5
5 a 3                   5 a 3
3 -| (FINAL)


------------------------------------

Format for Transducers

As of June 2014, only the FAdo format of transducers is accepted, as the Grail-like format is not generally supported. Transducers must be in standard form, that is, having transitions of the form   p x y q, where p and q are states, and each of x and y is either a single alphabet symbol or the empty word. The empty word is written as @epsilon. The format of transducer FAdo files must be as follows:
1. '#' begins a comment
2. @Transducer begins a new transducer and must
     be followed by the list of the final states separated by blanks
3. Transitions are written one per line and must be in standard form as noted above.
4. The source state of the first transition is the initial state.

Please see the FAdo documentation for the full description of Transducer format.

Below is an example of an input-altering transducer describing the suffix code property over the alphabet {a, b}. The transducer outputs any proper suffix of a given input word.

@Transducer 2 3
1 a @epsilon 2
1 b @epsilon 2
2 a @epsilon 2
2 b @epsilon 2
2 a a 3
2 b b 3
3 a a 3
3 b b 3

More examples below:

Input-preserving transducer describing the 1-substitution-detecting property over the alphabet {0, 1}. On input w, the transducer outputs either w, or any word resulting by substituting 1 bit of w with a different bit.
-
@Transducer 0 1
0 0 0 0
0 1 1 0
0 0 1 1
0 1 0 1
1 0 0 1
1 1 1 1

Input-preserving transducer describing the 1-sid-detecting property over the alphabet {a, b}. On input w, the transducer outputs any word resulting by performing at most one symbol substitution/insertion/deletion operation on w.
-
@Transducer 0 1
0 a a 0
0 b b 0
0 a b 1
0 b a 1
0 a @epsilon 1
0 b @epsilon 1
0 @epsilon a 1
0 @epsilon b 1
1 a a 1
1 b b 1

Input-altering transducer describing the thin property (= all languages whose words are of different lengths). On input w, the transducer outputs any word of the same length as w, but different from w.
-
@Transducer 2
1 a a 1
1 b b 1
1 a b 2
1 b a 2
2 a a 2
2 b b 2
2 a b 2
2 b a 2

Format for Trajectory Expressions

Regular trajectory properties can be described by regular expressions in the FAdo format. For example,
the regular expression 1*0* describes the suffix code property;
the regular expression 1*0*1* describes the infix code property;
the regular expression 0*1* + 1*0* describes the bifix code property (being prefix and suffix code).