You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
author = {Alur, Rajeev and Benedikt, Michael and Etessami, Kousha and Godefroid, Patrice and Reps, Thomas and Yannakakis, Mihalis},
2105
+
title = {Analysis of Recursive State Machines},
2106
+
year = {2005},
2107
+
issue_date = {July 2005},
2108
+
publisher = {Association for Computing Machinery},
2109
+
address = {New York, NY, USA},
2110
+
volume = {27},
2111
+
number = {4},
2112
+
issn = {0164-0925},
2113
+
url = {https://doi.org/10.1145/1075382.1075387},
2114
+
doi = {10.1145/1075382.1075387},
2115
+
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.},
2116
+
journal = {ACM Trans. Program. Lang. Syst.},
2117
+
month = {jul},
2118
+
pages = {786–818},
2119
+
numpages = {33},
2120
+
keywords = {model checking, program analysis, Software verification, temporal logic, context-free languages, recursive state machines, pushdown automata}
Copy file name to clipboardExpand all lines: tex/LinearAlgebra.tex
+27-30Lines changed: 27 additions & 30 deletions
Original file line number
Diff line number
Diff line change
@@ -414,7 +414,6 @@ \section{Матрицы и вектора}
414
414
415
415
Примерами структурных операций является \emph{транспонирование}, \emph{взятие подматрицы} и \emph{взятие элемента по индексу}.
416
416
417
-
\marginnote{
418
417
\begin{example}
419
418
Транспонирование матрицы.
420
419
\[
@@ -429,7 +428,7 @@ \section{Матрицы и вектора}
429
428
\end{pmatrix}
430
429
\]
431
430
\end{example}
432
-
}
431
+
433
432
\begin{definition}[Транспонирование матрицы]
434
433
Пусть дана матрица $M_{n \times m}$.
435
434
Тогда результат её \emph{транспонирования}, это такая матрица $M'_{m \times n}$, что $M'[i,j] = M[j,i]$ для всех $i \in [0\rng m - 1]$ и $j \in [0\rng n - 1]$.
@@ -450,41 +449,39 @@ \section{Матрицы и вектора}
450
449
Где 0 обозначает нулевой блок. Прямая сумма обозначается $L = M \oplus N$.
451
450
\end{definition}
452
451
453
-
\marginnote{
454
-
\begin{example}
455
-
Взятие подматрицы.
456
-
\begin{multline*}
457
-
\begin{pmatrix}
458
-
"a" & "ba" & "cb"\\
459
-
"ac" & "bab" & "b"
460
-
\end{pmatrix} [0 \rng 1, 1 \rng 2] = \\
461
-
= \begin{pmatrix}
462
-
"ba" & "cb"\\
463
-
"bab" & "b"
464
-
\end{pmatrix}
465
-
\end{multline*}
466
-
\end{example}
467
-
}
468
452
\begin{definition}[Взятие подматрицы]
469
453
Пусть дана матрица $M_{n\times m}$.
470
454
Тогда $M_{n \times m}[i_0\rng i_1, j_0\rng j_1]$~--- это такая $M'_{(i_1 - i_0 + 1) \times (j_1 - j_0 + 1)}$, что $M'[i, j] = M[i_0 + i, j_0 + j]$ для всех $i \in [0\rng i_1 - i_0 + 1]$ и $j \in [0\rng j_1 - j_0 + 1]$.
471
455
\end{definition}
472
456
473
-
\marginnote{
474
-
\begin{example}
475
-
Взятие элемента по индексу.
476
-
\[
477
-
\begin{pmatrix}
478
-
"a" & "ba" & "cb"\\
479
-
"ac" & "bab" & "b"
480
-
\end{pmatrix}[0, 1] = "ba"
481
-
\]
482
-
\end{example}
483
-
}
457
+
\begin{example}
458
+
Взятие подматрицы.
459
+
\begin{multline*}
460
+
\begin{pmatrix}
461
+
"a" & "ba" & "cb"\\
462
+
"ac" & "bab" & "b"
463
+
\end{pmatrix} [0 \rng 1, 1 \rng 2] =
464
+
\begin{pmatrix}
465
+
"ba" & "cb"\\
466
+
"bab" & "b"
467
+
\end{pmatrix}
468
+
\end{multline*}
469
+
\end{example}
470
+
484
471
\begin{definition}[Взятие элемента по индексу]
485
472
\emph{Взятие элемента по индексу}~--- это частный случай взятия подматрицы, когда начало и конец \enquote{среза} совпадают: $M[i, j] = M[i \rng i, j \rng j]$.
486
473
\end{definition}
487
474
475
+
\begin{example}
476
+
Взятие элемента по индексу.
477
+
\[
478
+
\begin{pmatrix}
479
+
"a" & "ba" & "cb"\\
480
+
"ac" & "bab" & "b"
481
+
\end{pmatrix}[0, 1] = "ba"
482
+
\]
483
+
\end{example}
484
+
488
485
Из алгебраических операций над матрицами нас в дальнейшем будут интересовать \emph{поэлементные операции}, \emph{скалярные операции}, \emph{матричное умножение}, \emph{произведение Кронекера}.
489
486
490
487
\begin{definition}[Поэлементные операции]
@@ -587,7 +584,7 @@ \section{Матрицы и вектора}
587
584
Пусть $G = (S, \circ)$~--- полугруппа, $M_{m \times n}$ и $N_{p \times q}$~--- две матрицы над этой полугруппой.
588
585
Тогда \emph{произведение Кронекера} или \emph{тензорное произведение} матриц $M$ и $N$~--- это блочная матрица $K$ размера $mp \times nq$, вычисляемая следующим образом:
589
586
\begin{multline*}
590
-
K = M \otimes N = \\
587
+
K = M \otimes N =
591
588
\begin{pmatrix}
592
589
(M[0,0] \circ N & \cdots & M[0,n-1] \circ N \\
593
590
\vdots & \ddots & \vdots\\
@@ -598,7 +595,7 @@ \section{Матрицы и вектора}
598
595
599
596
\begin{remark}
600
597
\label{note:KronIsNotCommutative}
601
-
Произведение Кронекера не является коммутативным.
598
+
Произведение Кронекера не является коммутативным\sidenote{Показать это можно по определению: найти пример, для которого $M \otimes N \neq N \otimes M$.}.
602
599
При этом всегда существуют две матрицы перестановок $P$ и $Q$ такие, что $A \otimes B = P(B \otimes A)Q$.
0 commit comments