libFAUDES addresses discrete event systems that can be modelled by regular languages or, equivalently, by finite automata. This section of the user reference provides some background and documents general purpose functions on generators. It is organized follows:

Copyright (C) 2006 Bernd Opitz.
Copyright (C) 2008, 2009 Thomas Moor, Klaus Schmidt, Sebastian Perk.
Copyright (C) 2010 - 2017 Thomas Moor, Klaus Schmidt.


Alphabet. An alphabet Sigma is a set of symbols  Sigma. If not otherwise noted, we assume alphabets to be finite.

Strings. A string s over an alphabet Sigma is a finite sequence of symbols, denoted s = o1 o2 ... o_n, with o_i  Sigma. We write |s| = n for the length of the string. Symbols of Sigma are identified with strings of length 1.

Empty string. The empty string is denoted epsilon. Its length is zero, i.e. |epsilon| = 0.

Set of all strings. The set of all strings of symbols from an alphabet Sigma with length greater than zero is denoted Sigma+. We write Sigma* = Sigma+  {epsilon}.

Concatenation. Given s = o1 o2 ... o_n and r = t1 t2 ... t_k  Sigma*, let s r denote the concatenation of s and r, i.e. s r = o1 o2 ... o_n t1 t2 ... t_k. For all  Sigma*, let s epsilon := s = :epsilon s.

Prefix. A string  Sigma* is said to be a prefix of  Sigma* if there exists  Sigma* such that s t = r. We write s ≤ r to indicate that s is a prefix of r. If in addition s ≠ r, we say that s is a strict prefix of r and write s < r.

Formal languages. A formal language over an alphabet Sigma is a subset  Sigma*. A formal language that can be represented by a finite automata is said to be regular; see also Generator.

Infinite length strings. Given an alphabet Sigma, let Sigma^w denote the set of all infinite sequences w:NSigma. For  Sigma^w, we write w_i  Sigma*, w_i < w, for the prefix consisting of the first i symbols.

Omega languages. An omega language over an alphabet Sigma is a subset  Sigma^w. The set of all prefixes is denotet Prefix(B) = {s  Sigma*|  w  B: s < w}. A formal language  Sigma* can be extended to an omega-language by the limit operator

B(L) = {w  Sigma^w| w has infinitely many prefixes in L };

see also Generator.


Background and algorithms presented in this section are fairly common and by no means specific to the control of discrete event systems. Relevant literature includes:

[C1] W.M. Wonham: Supervisory Control of Discrete-Event Systems, available at University of Toronto, 2009 (revised).

[C2] C.G. Cassandras, S. Lafortune: Introduction to Discrete Event Systems, 2007 (2nd ed).

[C3] E. Hopcroft, J.D. Ullman: Introduction to Automata Theory, Languages, and Computation, 1979.

[C4] R. Malik, H.. Flordal: Compositional verification in supervisory control, SIAM Journal of Control and Optimization, 2009.

libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings"