What is this about? This server allows a user to specify one of 4 questions about properties of regular languages and provides an answer to the specified question.
-
The Satisfaction question: The user enters the description of a regular
language via a finite automaton or a regular expression, and the description of a language property, and returns YES/NO, depending on whether the
language satisfies the property. If the answer is NO, appropriate counterexamples (also called witness words) are provided.
-
The Maximality question: If a language satisfies a property, the user can ask the server to decide whether the language is maximal with respect to the property. Being maximal means that if any new words are added to the language the resulting language would violate the property. If the language is not maximal then the server returns a word that can be added to the language. The Maximality question is PSPACE-hard, which means that for certain inputs the server would need a very long time to produce the answer.
-
The Construction question: The user enters 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 [KoMoRe]. The integer s must be less than 10 and specifies that the alphabet must be {'0','1',...,'s'}.
-
The Approximate Maximality question: As the Maximality question is hard, the server also provides an answer to the Approximate Maximality question based on the PRAX algorithms in [KoMaMoRe].
The main idea behind Approximate Maximality of a language (with respect to a property) is as follows: if a sample of words is generated, and if every generated word violates the property when it is added to the given language then the language is probably close to being maximal. The user enters a regular language and a property as above, and an approximation tolerance ε, with 0<ε<1, and the server returns, either that the language is not maximal (providing also a word that can be added), or that the language is probably (1-ε) close to being maximal. The size of the sample of words depends on ε (smaller ε implies larger size). Each word is sampled in 2 steps: first the length is selected according to the Dirichlet distribution D(t), [Gol,KoMaMoRe], and then the letters of the word according to the unifirm distribution on the alphabet. The parameter t must be > 1; however, the closer t is to 1 the longer the sampled words can be, and the algorithm would be slower. When t=2 the sampled words are not very long but the selected length would be biased.
See further below how to describe properties.
Properties. Examples of language properties are: prefix code, infix code, 1-substitution-error-detecting language [ShyThi,Shyr,JuKon]. 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. Transducers can conveniently be used to realize many 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 UD code (uniquely decipherable/decodable code), prefix code, suffix code, bifix code, infix code, outfix code, hypercode.
- Regular trajectory properties [Dom]:
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 [DuKon]:
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.
-
Input-preserving Transducer properties (also called Error-detecting properties) [DuKon,KoMeMoRe]: 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 [KoMeMoRe]: 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.
-
DNA-type transducer properties [KaKoKo]: Such a property is described by
a transducer t and an antimorphic involution θ as follows.
All languages L such that
t(L) ∩ θ(L) = EmptySet,
that is, the transducer cannot turn a word in L to a word in θ(L).
Implementation: Based on
FAdo, a package of Python libraries, which includes modules for automata, transducers,
and code properties.
[AAAMR] Andre Almeida, Marco Almeida, Jose Alves, Nelma Moreira, and Rogério Reis (2009):
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.
[Dass] Jürgen Dassow. Comment following the presentation in [DuKon].
[Dom] M. Domaratzki (2004):
Trajectory-Based Codes.
Acta Informatica, vol. 40, n. 6-7 (2004) 491-527.
[DuKon] K. Dudzinski and S. Konstantinidis (2010):
Formal descriptions of code properties: decidability, complexity, implementation.
International Journal of Foundations of Computer Science 23:1 (2012), 67--85. Presented at
DCFS 2010.
[FAdo]
FAdo: Tools for Formal Languages
manipulation.
[Gol] Solomon W. Golomb (1970): A class of probability distributions on the integers.
Journal of Number Theory 2 (1970) 189–192.
[JuKon] H. Jürgensen and S. Konstantinidis (1997): Codes.
In G. Rozenberg, A. Salomaa (eds):
Handbook of Formal Languages, vol. I,
511-607. Springer-Verlag, Berlin, 1997.
[KaKoKo]
Lila Kari, Stavros Konstantinidis, Steffen Kopecki (2018).
Transducer descriptions of DNA code properties and undecidability of antimorphic problems.
Inform. Comput. 259(2): 237-258 (2018).
Also presented in: DCFS 2015, University of Waterloo, Canada.
[KoMaMoRe]
Stavros Konstantinidis, Mitja Mastnak, Nelma Moreira, Rogério Reis (2022, 2023):
Approximate NFA universality and related problems motivated by information theory.
Theor. Comput. Sci. (2023).
Also: Approximate NFA universality motivated by information theory.
LNCS 13439: DCFS 2022 142-154, Debrecen, Hungary, August 29-31, 2022.
[KoMeMoRe] Stavros Konstantinidis, Casey Meijer, Nelma Moreira, Rogério Reis (2016,2018):
Symbolic Manipulation of Code Properties”.
J. Autom. Lang. Comb. 23 (2018).
Also: 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). Also: Symbolic manipulation of code properties. arXiv:1504.04715v1, 2015.
[KoMoRe] Stavros Konstantinidis, Nelma Moreira, Rogério Reis (2016, 2018):
Randomized generation of error control codes with automata and transducers.
RAIRO Theor. Informatics Appl. 52(2-3-4): 169-184 (2018).
Also: Generating Error Control Codes with Automata and Transducers.
8th Workshop on Non-Classical Models of Automata and Applications, Debrecen, Hungary, OCG Proceedings.
[Shyr] H.J. Shyr.
Free monoids and languages. Hon Min Book Company, Taichung, Taiwan, 1991.
[ShyThi] 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.