Derivation of the Cascade Parallel Composition of Timed Finite State Machines Using BALM-II
The paper considers the problem of deriving a cascade parallel composition of timed finite state machines (TFSMs). It can be reduced to a step-by-step derivation of a binary parallel composition. It is known that if each component of the binary parallel composition is a TFSM with constant output delays, then the composition can result in a TFSM with an infinite set of output delays given by a finite set of linear functions. Therefore, the problem of deriving a cascade composition of TFSMs with constant output delays is reduced to deriving a series of binary parallel compositions of TFSMs with output delays given either as constants or as a set of linear functions. In this paper, we refine the definition of the TFSM with particular attention to the description of the output delay. BALM-II is used as an instrument for deriving the composition. Therefore, we consider the transition from a TFSM with output delays given as a set of linear functions to the corresponding automaton. We propose a new procedure for deriving an automaton. Unlike the known procedure, it does not require subsequent determinization of the derived automaton. In addition, we provide a step-by-step description of how to derive the composition of the corresponding automata using BALM-II, discuss the procedure of reverse transformation from the automaton of the composition to the TFSM, and note some aspects associated with the composition of TFSMs with output delays as a set of linear functions. An example that illustrates the derivation of the cascade parallel composition of TFSMs is given.
Keywordstimed finite state machines cascade parallel composition BALM-II
Unable to display preview. Download preview PDF.
- 3.Yevtushenko, N., Villa, T., Brayton, R., Petrenko, A., and Sangiovanni-Vincentelli, A., Solution of parallel language equations for logic synthesis, The Proceedings of the International Conference on Computer-Aided Design, 2001, pp. 103–110.Google Scholar
- 4.Castagnetti, G., Piccolo, M., Villa, T., Yevtushenko, N., Mishchenko, A., and Brayton, R.K., Solving Parallel Equations with BALM-II, Technical Report No UCB/EECS-2012-181, Electrical Engineering and Computer Sciences University of California at Berkeley, 2012. http://www.eecs.berkeley.edu/Pubs/TechRpts/2012/EECS-2012-181.pdf.Google Scholar
- 7.Kondratyeva, O., Yevtushenko, N., and Cavalli, A., Parallel composition of nondeterministic finite state machines with timeouts, J. Control Comput. Sci. Tomsk State Univ., 2014, vol. 2, no. 27, pp. 73–81.Google Scholar
- 9.http://www.uppaal.com/.Google Scholar
- 10.Zhigulin, M., Yevtushenko, N., Maag, S., and Cavalli, A.R., FSM-based test derivation strategies for systems with timeouts, Proceedings of the International Conference QSIC, 2011, pp. 141–149.Google Scholar
- 11.Gromov, M. and Shabaldina, N., Using BALM-II for deriving parallel composition of timed finite state machines with outputs delays and timeouts: work-in-progress, Syst. Inf., 2016, vol. 8, pp. 33–42.Google Scholar