Работаем над регулярными языками.

Author: gsvgit

tex/FormalLanguageConstrainedReachabilityLectureNotes.bib

@@ -2041,4 +2041,61 @@ @article{Glushkov1961
   year = {1961},
   month = oct,
   pages = {1–53}
-}
+}
+
+@book{DBLP:books/ems/21/P2021,
+  editor       = {Jean{-}{\'{E}}ric Pin},
+  title        = {Handbook of Automata Theory},
+  publisher    = {European Mathematical Society Publishing House, Z{\"{u}}rich,
+                  Switzerland},
+  year         = {2021},
+  url          = {https://doi.org/10.4171/Automata},
+  doi          = {10.4171/AUTOMATA},
+  isbn         = {978-3-98547-006-8},
+  timestamp    = {Mon, 11 Apr 2022 14:12:30 +0200},
+  biburl       = {https://dblp.org/rec/books/ems/21/P2021.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@ARTICLE{6771467,
+  author={Mealy, George H.},
+  journal={The Bell System Technical Journal}, 
+  title={A method for synthesizing sequential circuits}, 
+  year={1955},
+  volume={34},
+  number={5},
+  pages={1045-1079},
+  keywords={},
+  doi={10.1002/j.1538-7305.1955.tb03788.x}
+  }
+
+@Inbook{Alagar2011,
+author="Alagar, V. S.
+and Periyasamy, K.",
+title="Extended Finite State Machine",
+bookTitle="Specification of Software Systems",
+year="2011",
+publisher="Springer London",
+address="London",
+pages="105--128",
+abstract="The FSM models we have considered, in spite of many extensions to basic automaton, fall short in many aspects. They have to be extended further, as broadly outlined below, in order to model complex system behavior.",
+isbn="978-0-85729-277-3",
+doi="10.1007/978-0-85729-277-3_7",
+url="https://doi.org/10.1007/978-0-85729-277-3_7"
+}
+
+@Article{ foster.ea:efsm:2020,
+	abstract	= 	{In this AFP entry, we provide a formalisation of extended finite state machines (EFSMs) where models are represented as finite sets of transitions between states. EFSMs execute traces to produce observable outputs. We also define various simulation and equality metrics for EFSMs in terms of traces and prove their strengths in relation to each other. Another key contribution is a framework of function definitions such that LTL properties can be phrased over EFSMs. Finally, we provide a simple example case study in the form of a drinks machine.},
+	author	= 	{Michael Foster and Achim D. Brucker and Ramsay G. Taylor and John Derrick},
+	date	= 	{2020-09-07},
+	file	= 	{https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-outline-2020.pdf},
+	filelabel	= 	{Outline},
+	issn	= 	{2150-914x},
+	journal	= 	{Archive of Formal Proofs},
+	month	= 	{sep},
+	note	= 	{\url{http://www.isa-afp.org/entries/Extended_Finite_State_Machines.html}, Formal proof development},
+	pdf	= 	{https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-2020.pdf},
+	title	= 	{A Formal Model of Extended Finite State Machines},
+	url	= 	{https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2020},
+	year	= 	{2020},
+} 

tex/FormalLanguageTheoryIntro.tex

@@ -107,7 +107,7 @@ \section{Теоретико-множественные операции над 
 
 \begin{definition}[TODO: ???]
     Пусть дано множество $S$ с определённой на нём операцией $\odot: S \times S \to S$, $S_1 \subseteq S$, тогда
-    \[S_1^n = \{ \underbrace{s_1 \odot s_1 \odot \dots \odot s_1}_{\text{n раз}} \mid s_1 \in S_1\}.\]
+    \[S_1^n = \{ \underbrace{s_1 \odot s_1 \odot \dots \odot s_1}_{\text{$n$ раз}} \mid s_1 \in S_1\}.\]
     При этом $S_1^0 = \{\varepsilon\}$%
     \sidenote{В данном случае нулевая степень даёт единицу, как мы и привыкли.}.
 \end{definition}