Минимизация автоматов с таймаутами и временными ограничениями

Конечные автоматы широко используются для анализа и синтеза управляющих систем. При описании систем, поведение которых зависит от времени, конечный автомат расширяется введением временных аспектов и вводится понятие временного автомата. В настоящей работе мы рассматриваем проблему минимизации автоматов с таймаутами и временными ограничениями, поскольку сложность многих задач в теории автоматов существенно зависит от размеров исследуемой системы. Поведение временного автомата может быть достаточно точно описано соответствующим конечным автоматом, и предлагаемый метод минимизации числа состояний системы основан на использовании такой конечно автоматной абстракции. Более того, далее мы минимизируем и временные аспекты автоматного описания, сокращая продолжительность таймаутов и число переходов с временными ограничениями. Мы также показываем, что для полностью определённого детерминированного временного автомата существует единственная минимальная (каноничная) форма, т. е. единственный приведённый по состояниям и временным аспектам автомат с таймаутами и временными ограничениями, поведение которого совпадает с исходным временным автоматом; например, такая минимальная форма может быть использована при построении проверяющих тестов для проверки функциональных и нефункциональных требований к тестируемой реализации. Предложенный метод к минимизации временных аспектов на основе конечно автоматной абстракции может быть применён и для частных случаев рассматриваемой модели, т. е. для минимизации детерминированных полностью определенных автоматов только с таймаутами или только с временными ограничениями.