Geodesic
Using BALM-II for deriving cascade parallel composition of timed finite state machines
Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 715-728.

Voir la notice de l'article provenant de la source Math-Net.Ru

In this paper, we consider the problem of deriving a cascade parallel composition of timed finite state machines (TFSMs). In order to build such a composition we can derive the corresponding binary parallel compositions step-by-step. It is known that if each component of a binary parallel composition is TFSM with output delays that are natural numbers or zero, the result of the composition can be TFSM with output delays that are sets of linear functions. So, the problem of deriving a cascade composition of TFSMs with constant output delays is reduced to the problem of deriving several binary parallel compositions of TFSMs with output delays that are sets of constants or linear functions. In this work, we refine the definition of TFSM and pay special attention to the description of an output delay function. As a tool for deriving the composition we consider BALM-II, and in consequence we study the ways of constructing the corresponding automaton for TFSM with output delays as a set of linear functions. We suggest a new procedure for constructing such an automaton, and unlike the known procedure our procedure does not require further determinization of the derived automaton. Moreover, we describe step by step how to build the composition of the derived automaton by using BALM-II, and discuss a procedure of reverse transformation from the global automaton to TFSM in case when the components are TFSMs with output delays that are sets of linear functions. We use an application example in order to illustrate derivation of the cascade parallel composition of TFSMs.
Keywords: timed finite state machines, cascade parallel composition, BALM-II. 
@article{MAIS_2016_23_6_a3,
     author = {M. L. Gromov and N. V. Shabaldina},
     title = {Using {BALM-II} for deriving cascade parallel composition of timed finite state machines},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {715--728},
     publisher = {mathdoc},
     volume = {23},
     number = {6},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a3/}
}
TY  - JOUR
AU  - M. L. Gromov
AU  - N. V. Shabaldina
TI  - Using BALM-II for deriving cascade parallel composition of timed finite state machines
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2016
SP  - 715
EP  - 728
VL  - 23
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a3/
LA  - ru
ID  - MAIS_2016_23_6_a3
ER  - 
%0 Journal Article
%A M. L. Gromov
%A N. V. Shabaldina
%T Using BALM-II for deriving cascade parallel composition of timed finite state machines
%J Modelirovanie i analiz informacionnyh sistem
%D 2016
%P 715-728
%V 23
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a3/
%G ru
%F MAIS_2016_23_6_a3
M. L. Gromov; N. V. Shabaldina. Using BALM-II for deriving cascade parallel composition of timed finite state machines. Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 715-728. http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a3/

[1] Moore E. F., “Gedanken-experiments on Sequential Machines”, Automata Studies, Annals of Mathematical Studies, 34, Princeton University Press, Princeton, N.J., 1956, 129–153 | MR

[2] Gill A., Introduction to the theory of finite-state machines, McGraw-Hill, New-York, 1962, 207 pp. | MR

[3] Yevtushenko N., Villa T., Brayton R., Petrenko A., Sangiovanni-Vincentelli A., “Solution of parallel language equations for logic synthesis”, The Proceedings of the International Conference on Computer-Aided Design, 2001, 103–110

[4] Castagnetti G., Piccolo M., Villa T., Yevtushenko N., Mishchenko A., 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

[5] Alur R., Dill D. L., “A theory of timed automata”, Theoretical computer science, 126:2 (1994), 183–235 | DOI | MR | Zbl

[6] El-Fakih K., Gromov M, Shabaldina N., Yevtushenko N., “Distinguishing Experiments for Timed Non-Deterministic Finite State Machines”, Acta Cybernetica, 21:2 (2013), 205–222 | DOI | MR | Zbl

[7] Kondratyeva O., Yevtushenko N., Cavalli A., “Parallel composition of nondeterministic finite state machines with timeouts”, Journal of Control and Computer Science of Tomsk State University, 2014, no. 2(27), 73–81

[8] Kondratyeva O., Yevtushenko N., Cavalli A., “Solving parallel equations for Finite State Machines with Timeouts”, The Proceedings of ISP RAS, 26:6 (2014), 85–98 | DOI

[9] http://www.uppaal.com/

[10] Zhigulin M., Yevtushenko N., Maag S., Cavalli A. R., “FSM-based test derivation strategies for systems with timeouts.”, Proceedings of the international conference QSIC, 2011, 141–149

[11] Gromov M., Shabaldina N., “Using BALM-II for deriving parallel composition of timed finite state machines with outputs delays and timeouts: work-in-progress”, System Informatics, 8 (2016), 33–42

[12] Springintveld J., Vaandrager F., D'Argenio P. R., “Testing timed automata”, Theoretical Computer Science, 254:1–2, March (2001), 225–257 | DOI | MR | Zbl