Behaviour examples for synthesizing automaton models by temporal formulas. Nexo Revista Científica. 2021;34(01):61-73. doi:10.5377/nexo.v34i01.11285