Методы верификации программного обеспечения

Рисунок 5. Пример конечного автомата. 
Чтобы конечный автомат «заработал», ему нужно передать последовательность 
стимулов. Тогда автомат начинает считывать стимулы один за другим и 
выполнять переходы, помеченные этими стимулами, начиная с начального 
состояния. Выполнение перехода заключается в изменении текущего состояния 
и выдаче реакции, которой помечен данный переход. Так, если считать 
начальным состоянием показанного на Рис. 7 автомата состояние 0, то после 
подачи ему на вход последовательности abababab он перейдет в состояние 2 и 
выдаст последовательность реакций xyyyxxxy.
Можно считать, что каждый автомат реализует некоторое преобразование 
конечных последовательностей стимулов в конечные последовательности 
реакций. Помимо этого преобразования автомат задает и способ его реализации 
— одно и то же преобразование может быть реализовано разными конечными 
автоматами. 

Одним из обобщений конечных автоматов являются конечные системы 
помеченных переходов (или просто системы переходов, labeled transition systems, 
LTS) [126]. В системе переходов каждый переход помечен только одним 
символом — либо стимулом, либо реакцией (строго говоря, это верно для 
систем переходов со стимулами и реакциями, IOLTS, в случае общих LTS 
считается, что есть только один вид символов), либо может вообще не иметь 
метки (выполнение такого перехода никак не проявляется вовне). 
Любой автомат можно представить как систему переходов, на Рис. 6 слева 
показана система переходов, эквивалентная автомату, представленному на 
Рис. 5. Но системы переходов могут реализовывать более сложные 
0 
1 
2 
b/x 
b/y 
b/y 
a/y 
a/x 
a/x 

---

53 
преобразования последовательностей символов, и поэтому не всякая система 
переходов представима как автомат — пример представлен на Рис. 6 справа.