CoreFaudes

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.

Preliminaries

Alphabet. An alphabet Sigma is a set of symbols o ∈ 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 s ∈ Sigma*, let s epsilon := s = :epsilon s.

Prefix. A string s ∈ Sigma* is said to be a prefix of r ∈ Sigma* if there exists t ∈ 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 L ⊆ 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:N→Sigma. For w ∈ 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 B ⊆ Sigma^w. The set of all prefixes is denotet Prefix(B) = {s ∈ Sigma*| ∃ w ∈ B: s < w}. A formal language L ⊆ 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.

Literature

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.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings"

>>