On reduced forms of initialized Finite State Machines with timeouts
https://doi.org/10.15514/ISPRAS-2020-32(2)-10
Abstract
Trace models such as Finite State Machines (FSMs) are widely used in the area of analysis and synthesis of discrete event systems. FSM minimization is a well-known optimization problem which allows to reduce the number of FSM states by deriving the canonical form that is unique up to isomorphism. In particular, the latter is a base for FSM-based ‘black-box’ test derivation methods such as W-method and its modifications. Since nowadays the behavior of many software and hardware systems significantly depends on time aspects, classical FSMs are extended by clock variables including input and output timeouts. The minimization of a Timed Finite State Machine (TFSM) includes both state and time aspects reduction. Existing approaches allow to derive the canonical representation for non-initialized deterministic TFSMs while for initialized TFSMs, i.e., TFSMs with the designated initial state, several pair-wise non-isomorphic minimal forms can exist. In this paper, we determine initialized TFSM classes for which the minimal form is unique up to isomorphism.
Supporting agencies: This work is partly supported by RFFR Project No. 19-07-00327
About the Authors
Aleksander Sergeevitch TVARDOVSKII
National Research Tomsk State University
Russian Federation
Ph.D. student
Russian Federation
Ph.D. student
Nina Vladimirovna YEVTUSHENKO
Ivannikov Institute for System Programming of the Russian Academy of Sciences,
National Research University Higher School of Economics
Russian Federation
Doctor of technical sciences, professor, a leading researcher of ISP RAS, professor at HSE
Russian Federation
Doctor of technical sciences, professor, a leading researcher of ISP RAS, professor at HSE
References
1. A. Gill. Introduction to the Theory of Finite-State Machines, McGraw Hill, 1962, 207 p.
2. D. Lee, M. Yannakakis Principles and methods of testing finite state machines-a survey. Proceedings of the IEEE, vol. 84, no. 8, 1996, pp. 1090-1123.
3. T.E. Murphy, X.-J. Geng, and J. Hammer. On the control of asynchronous machines with races. IEEE Transactions on Automatic Control, vol. 48, no. 6, 2003, pp. 1073-1081.
4. Kumar Ratnesh, Garg Vijay K. Modeling and control of logical discrete event systems. The Springer International Series in Engineering and Computer Science, 1995, 143 p.
5. C. C. Cassandras, S. Lafortune. Introduction to discrete event systems. Springer, 1999, 828 p.
6. Rita Dorofeeva et al. FSM-based conformance testing methods: A survey an-notated with experimental evaluation. Information and Software Technology, vol. 52, issue 12, 2010, pp. 1286-1297.
7. Maxim Zhigulin, Nina Yevtushenko, Stéphane Maag, Ana R. Cavalli. FSM-Based Test Derivation Strategies for Systems with Time-Outs. In Proc. of the 11th International Conference on Quality Software, 2011, pp. 141-149.
8. Tripakis S. Folk theorems on the determinization and minimization of timed automata. Information Processing Letters, vol. 99, no. 6, 2006, pp. 222-226.
9. Merayo M., Nunez M., Rodriguez I. Formal testing from timed finite state machines, Computer Networks, vol. 52, issue 2, 2008, pp. 432-460.
10. Gromov M., El-Fakih K., Shabaldina N., and Yevtushenko N. Distinguishing non-deterministic timed fnite state machines. In Formal Techniques for Distributed Systems. Lecture Notes in Computer Science. vol. 5522, 2009, pp.137-151.
11. R.M. Hierons, M.G. Merayo, M. Nunez. Testing from a Stochastic Timed System with a Fault Model / // Journal of Logic and Algebraic Programming, vol. 72, issue 8, 2009, pp. 98-115.
12. Bresolin D., El-Fakih K., Villa T., Yevtushenko N. Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power. In Proc. of the 5th International Symposium on Games, Automata, Logics and Formal Verification (GandALF2014), 2014, pp. 203–216..
13. Tvardovskii A.S., Yevtushenko N.V., Gromov M.L. Minimizing Finite State Machines with time guards and timeouts. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 4, 2017 г., pp. 139-154 (in Russian). DOI: 10.15514/ISPRAS-2017-29(4)-8 / Твардовский А.С., Евтушенко Н.В., Громов М.Л. Минимизация автоматов с таймаутами и временными ограничениями. Труды ИСП РАН, том 29, вып. 4, 2017 г., стр. 139-154.
14. Khaled El-Fakih, Nina Yevtushenko, Hacène Fouchal. Testing Timed Finite State Machines with Guaranteed Fault Coverage. Lecture Notes in Computer Science book series, vol. 5826, 2009. pp. 66-80.
15. Tvardovskiy A. On the minimization of timed Finite State Machines. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 6, 2014, pp. 77-84 (in Russian). DOI: 10.15514/ISPRAS-2014-26(6)-7 / Твардовский А.С. К минимизации автоматов с таймаутами, том 26, вып. 6, 2014 г., стр. 77-84.
16. Tvardovskiy A.S., Yevtushenko N.V. Minimizing Timed Finite State Machines. Tomsk State University Journal of Control and Computer Science, № 4(29), 2014, pp. 77-83 (in Russian) / Твардовский А.С., Евтушенко Н.В. К минимизации автоматов с временными ограничениями // Вестник Томского государственного университета. Управление, вычислительная техника и информатика, 2014 г., № 4(29), стр. 77–83.
Review
For citations:
TVARDOVSKII A.S., YEVTUSHENKO N.V. On reduced forms of initialized Finite State Machines with timeouts. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(2):125-134. https://doi.org/10.15514/ISPRAS-2020-32(2)-10
Email this article 