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.

- 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.

__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.

[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.

[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.

**Project initiator**: Stavros Konstantinidis (http://cs.smu.ca/~stavros/)

Nelma Moreira & Rogerio Reis: as of version 3, LaSer's back end is based on FAdo

5: Matthew Rafuse (January 2018, **current version**)

Incorporating into LaSer satisfaction of DNA properties, introducing text areas for entering user input, and making the views.py code modular.

4: Abisola Adeniran (October 2016)

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

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:

- '#' begins a comment
**@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- Transitions are written one per line and consist of three fields separated by blanks: "state" "symbol" "new state"
- 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)
```

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:

- '#' begins a comment
**@Transducer**begins a new transducer and must be followed by the list of the final states separated
by blanks
- Transitions are written one per line and must be in standard form as noted above.
- 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
```

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
```

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).

Theta Antimorphisms are used to answer questions about DNA properties.

Below is an example of an antimorphism describing the *DNA* antimorphism over the DNA alphabet. There is no need to add the inverses as LaSer does this automatically.

```
@Theta
a t
g c
```