Перевірка несуперечності початкових описів кінцевих автоматів

Ю.М. Вишняков

У 60-70-х роках на теорію кінцевих автоматів (КА), як універсальний інструментарій опису та синтезу цифрових схем, покладали великі надії. Проте можливості технологічного базису та інформаційні технології того часу обмежили практичне використання теорії КА тільки рамками структурного синтезу. Абстрактний синтез так і залишився предметом теоретичних досліджень. Сьогодні в автоматизованому проектуванні відбувається інтенсивний перехід до інтегрованим інструментальним засобам, що здійснює наскрізну розробку проектів на всіх рівнях. У таких системах поряд зі стандартними засобами проектування топології і моделювання повинні бути присутнім і засоби реалізація проектних процедур логічного синтезу. Таким чином сьогодні сформовані практичні потреби і є всі умови, щоб абстрактна теорія КА зайняла гідне місце в автоматизованому проектуванні. Однак у цьому плані вона повинна бути перероблена в контексті наскрізного автоматизованого проектування.

В рамках цієї мети пропонована робота розвиває абстрактний синтез в частині побудови несуперечливих описів КА мовою регулярних виразів.

Нехай задані вхідний X = (X1, X2 ,..., Xn) і вихідний Y = (Y1, Y2 ,..., Ym) алфавіти. КА переробляє вхідні слова (ланцюжки) a