Базовая версия основных понятий теории множеств готова.

Author: gsvgit

tex/Context-Free_Languages.tex

@@ -538,42 +538,31 @@ \section{Нормальная форма Хомского}
 
     Первым шагом добавим новый нетерминал и сделаем его стартовым:
     \begin{align*}
-        S_0 & \to S                        \\
-        S   & \to a S b S \mid \varepsilon
+        S_0 & \to S                             \\
+        S   & \to a \ S \ b \ S \mid \varepsilon
     \end{align*}
     Заменим все терминалы на новые нетерминалы:
     \begin{align*}
-        S_0 & \to S                        \\
-        S   & \to L S R S \mid \varepsilon \\
-        L   & \to a                        \\
-        R   & \to b
+        S_0 & \to S                              & L & \to a  \\
+        S   & \to L \ S \ R \ S \mid \varepsilon & R & \to b
     \end{align*}
     Избавимся от длинных правил:
     \begin{align*}
-        S_0 & \to S                     \\
-        S   & \to L S' \mid \varepsilon \\
-        S'  & \to S S''                 \\
-        S'' & \to R S                   \\
-        L   & \to a                     \\
-        R   & \to b
+        S_0 & \to S                       & S'' & \to R \ S \\
+        S   & \to L \ S' \mid \varepsilon & L   & \to a   \\
+        S'  & \to S \ S''                 & R   & \to b
     \end{align*}
     Избавимся от $\varepsilon$-продукций:
     \begin{align*}
-        S_0 & \to S \mid \varepsilon \\
-        S   & \to L S'               \\
-        S'  & \to S'' \mid S S''     \\
-        S'' & \to R   \mid R S       \\
-        L   & \to a                  \\
-        R   & \to b
+        S_0 & \to S \mid \varepsilon & S'' & \to R   \mid R \ S\\
+        S   & \to L \ S'             & L   & \to a  \\
+        S'  & \to S'' \mid S \ S''   & R   & \to b
     \end{align*}
     Избавимся от цепных правил:
     \begin{align*}
-        S_0 & \to L S' \mid \varepsilon \\
-        S   & \to L S'                  \\
-        S'  & \to b \mid R S \mid S S'' \\
-        S'' & \to b \mid R S            \\
-        L   & \to a                     \\
-        R   & \to b
+        S_0 & \to L \ S' \mid \varepsilon   & S'' & \to b \mid R \ S \\
+        S   & \to L \ S'                    & L   & \to a \\
+        S'  & \to b \mid R \ S \mid S \ S'' & R   & \to b
     \end{align*}
 \end{example}
 

tex/FormalLanguageConstrainedReachabilityLectureNotes.bib

@@ -1996,126 +1996,142 @@ @inproceedings{10.1145/2949689.2949711
 }
 
 @article{chomsky1958finite,
-  title={Finite state languages},
-  author={Chomsky, Noam and Miller, George A},
-  journal={Information and control},
-  volume={1},
-  number={2},
-  pages={91--112},
-  year={1958},
-  publisher={Elsevier}
+  title     = {Finite state languages},
+  author    = {Chomsky, Noam and Miller, George A},
+  journal   = {Information and control},
+  volume    = {1},
+  number    = {2},
+  pages     = {91--112},
+  year      = {1958},
+  publisher = {Elsevier}
 }
 
-@article{OWENS_REPPY_TURON_2009, title={Regular-expression derivatives re-examined}, volume={19}, DOI={10.1017/S0956796808007090}, number={2}, journal={Journal of Functional Programming}, author={OWENS, SCOTT and REPPY, JOHN and TURON, AARON}, year={2009}, pages={173–190}} <div></div>
+@article{OWENS_REPPY_TURON_2009,
+  title   = {Regular-expression derivatives re-examined},
+  volume  = {19},
+  doi     = {10.1017/S0956796808007090},
+  number  = {2},
+  journal = {Journal of Functional Programming},
+  author  = {OWENS, SCOTT and REPPY, JOHN and TURON, AARON},
+  year    = {2009},
+  pages   = {173–190}
+} <div></div>
 
 @article{10.1145/363347.363387,
-author = {Thompson, Ken},
-title = {Programming Techniques: Regular expression search algorithm},
-year = {1968},
-issue_date = {June 1968},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {11},
-number = {6},
-issn = {0001-0782},
-url = {https://doi.org/10.1145/363347.363387},
-doi = {10.1145/363347.363387},
-abstract = {A method for locating specific character strings embedded in character text is described and an implementation of this method in the form of a compiler is discussed. The compiler accepts a regular expression as source language and produces an IBM 7094 program as object language. The object program then accepts the text to be searched as input and produces a signal every time an embedded string in the text matches the given regular expression. Examples, problems, and solutions are also presented.},
-journal = {Commun. ACM},
-month = {jun},
-pages = {419–422},
-numpages = {4},
-keywords = {match, regular expression, search}
+  author     = {Thompson, Ken},
+  title      = {Programming Techniques: Regular expression search algorithm},
+  year       = {1968},
+  issue_date = {June 1968},
+  publisher  = {Association for Computing Machinery},
+  address    = {New York, NY, USA},
+  volume     = {11},
+  number     = {6},
+  issn       = {0001-0782},
+  url        = {https://doi.org/10.1145/363347.363387},
+  doi        = {10.1145/363347.363387},
+  abstract   = {A method for locating specific character strings embedded in character text is described and an implementation of this method in the form of a compiler is discussed. The compiler accepts a regular expression as source language and produces an IBM 7094 program as object language. The object program then accepts the text to be searched as input and produces a signal every time an embedded string in the text matches the given regular expression. Examples, problems, and solutions are also presented.},
+  journal    = {Commun. ACM},
+  month      = {jun},
+  pages      = {419–422},
+  numpages   = {4},
+  keywords   = {match, regular expression, search}
 }
 
 @article{Glushkov1961,
-  title = {THE ABSTRACT THEORY OF AUTOMATA},
-  volume = {16},
-  ISSN = {1468-4829},
-  url = {http://dx.doi.org/10.1070/RM1961v016n05ABEH004112},
-  DOI = {10.1070/rm1961v016n05abeh004112},
-  number = {5},
-  journal = {Russian Mathematical Surveys},
+  title     = {THE ABSTRACT THEORY OF AUTOMATA},
+  volume    = {16},
+  issn      = {1468-4829},
+  url       = {http://dx.doi.org/10.1070/RM1961v016n05ABEH004112},
+  doi       = {10.1070/rm1961v016n05abeh004112},
+  number    = {5},
+  journal   = {Russian Mathematical Surveys},
   publisher = {Steklov Mathematical Institute},
-  author = {Glushkov,  V M},
-  year = {1961},
-  month = oct,
-  pages = {1–53}
+  author    = {Glushkov,  V M},
+  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},
-} 
+  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}
+}
 
 @article{10.1145/1075382.1075387,
-author = {Alur, Rajeev and Benedikt, Michael and Etessami, Kousha and Godefroid, Patrice and Reps, Thomas and Yannakakis, Mihalis},
-title = {Analysis of Recursive State Machines},
-year = {2005},
-issue_date = {July 2005},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {27},
-number = {4},
-issn = {0164-0925},
-url = {https://doi.org/10.1145/1075382.1075387},
-doi = {10.1145/1075382.1075387},
-abstract = {Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities.After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time O(nθ2) and space O(nθ), where n is the size of the recursive machine and θ is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node.},
-journal = {ACM Trans. Program. Lang. Syst.},
-month = {jul},
-pages = {786–818},
-numpages = {33},
-keywords = {model checking, program analysis, Software verification, temporal logic, context-free languages, recursive state machines, pushdown automata}
-}
+  author     = {Alur, Rajeev and Benedikt, Michael and Etessami, Kousha and Godefroid, Patrice and Reps, Thomas and Yannakakis, Mihalis},
+  title      = {Analysis of Recursive State Machines},
+  year       = {2005},
+  issue_date = {July 2005},
+  publisher  = {Association for Computing Machinery},
+  address    = {New York, NY, USA},
+  volume     = {27},
+  number     = {4},
+  issn       = {0164-0925},
+  url        = {https://doi.org/10.1145/1075382.1075387},
+  doi        = {10.1145/1075382.1075387},
+  abstract   = {Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities.After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time O(nθ2) and space O(nθ), where n is the size of the recursive machine and θ is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node.},
+  journal    = {ACM Trans. Program. Lang. Syst.},
+  month      = {jul},
+  pages      = {786–818},
+  numpages   = {33},
+  keywords   = {model checking, program analysis, Software verification, temporal logic, context-free languages, recursive state machines, pushdown automata}
+}
+
+@article{верещагин2000начала,
+  title   = {Начала теории множеств},
+  author  = {Верещагин, Николай Константинович and Шень, Александр},
+  journal = {Шень М.: МЦНМО},
+  year    = {2000}
+}