К проверке строго детерминированного поведения временных конечных автоматов

Конечные автоматы широко применяются в качестве математических моделей при решении многочисленных задач в области программирования, проектирования микроэлектронных схем и телекоммуникационных систем. Для описания поведения систем реального времени модель конечного автомата может быть расширена добавлением в неё часов - параметра непрерывного времени, моделируемого вещественной переменной. В автоматах реального времени для входных и выходных сигналов указывается время их поступления и выдачи, а переходы автомата снабжены описанием задержек, связанных с ожиданием входных сигналов и формированием выходных сигналов. Так же, как и для классических автоматов дискретного времени, задача минимизации конечных автоматов реального времени возникает во многих приложениях этой модели вычислений. Для классической модели автоматов реального времени эта задача уже подробно рассмотрена. В нашей работе мы предлагаем более сложную модель: в ней порядок следования выходных сигналов определяется не только порядком поступления входных сигналов, но также и задержкой, связанной с их обработкой. В этой модели при выполнении одной и той же последовательности переходов выходные сигналы могут выдаваться в разном порядке в зависимости от времени поступления входных сигналов. В новой модели автоматов реального времени решению задачи минимизации должно предшествовать изучение вопроса строгой детерминированности - однозначности поведения автомата на одних и тех же последовательностях переходов. В представленной статье приведены и обоснованы необходимые и достаточные условия строгой детерминированности автоматов реального времени, а также исследованы вопросы, связанные с решением задачи минимизации этой разновидности автоматов.

конечные временные автоматы, строго детерминированное поведение

1. Alur R., Dill D. A Theory of Timed Automata. Theoretical Computer Science, vol. 126, 1994, pp. 183-235.

2. Alur R., Madhusudan P. Decision Problems for Timed Automata: A Survey. In Proceedings of the 4-th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM’04), 2004, pp. 1-24.

3. Alur R., Fix L., Henzinger Th. A. A Determinizable Class of Timed Automata. In Proceedings of the 6-th International Conference on Computer Aided Verification (CAV’94), 1994, p 1-13.

4. Baier C., Bertrand N., Bouyer P., Brihaye T. When are Timed Automata Determinizable? In Proceedings of the 36-th International Colloquium on Automata, Languages, and Programming (ICALP 2009), 2009, p. 43-54.

5. Bresolin D., El-Fakih K., Villa T., Yevtushenko N. Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power. In Proceedings of the International Conference GANDALF, 2014, p. 203-216.

6. Cardell-Oliver R. Conformance Tests for Real-Time Systems with Timed Automata Specifications. Formal Aspects of Computing, vol. 12, no. 5, 2000, p. 350–371.

7. Cormen T. H., Leiserson C. E., Rivest R. L., Stein C. 35.5: The subset-sum problem. Introduction to Algorithms (2-nd ed.), 2001.

8. Finkel O. Undecidable Problems about Timed Automata. In Proceedings of 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’06), 2006, p. 187-199.

9. Fletcher J. G., Watson R. W. Mechanism for Reliable Timer-Based Protocol. Computer Networks, vol. 2, 1978, pp. 271-290.

10. Merayo M.G., Nuunez M., Rodriguez I. Formal Testing from Timed Finite State Machines. Computer Networks, vol. 52, no 2, 2008, pp. 432-460.

11. Ouaknine J., Worrell J. On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In Proceedings of the 19-th Annual Symposium on Logic in Computer Science (LICS’04), 2004, pp. 54-63.

12. Suman P.V., Pandya P.K., Krishna S.N., Manasa L. Timed Automata with Integer Resets: Language Inclusion and Expressiveness. In Proceedings of the 6-th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’08), 2008, pp. 78–92.

13. А.С. Твардовский, Н.В. Евтушенко. К минимизации автоматов с временными ограничениями. Вестник Томского государственного университета. Управление, вычислительная техника и информатика, vol. 29, no 4, 2014, pp. 77-83.

14. Твардовский А.С., Евтушенко Н.В., Громов М.Л. Минимизация автоматов с таймаутами и временными ограничениями. Труды ИСП РАН, том 29, вып. 4, 2017 г., стр. 139-154. DOI: 10.15514/ISPRAS-2017-29(4)-8..

15. Zhigulin M., Yevtushenko N., Maag S., Cavalli A. FSM-Based Test Derivation Strategies for Systems with Timeouts. In Proceedings of the 11-th International Conference on Quality Software, 2011, p. 141-149.