logo

SCIENCE CHINA Information Sciences, Volume 64 , Issue 9 : 192103(2021) https://doi.org/10.1007/s11432-019-2767-4

Learning real-time automata

More info
  • ReceivedJan 20, 2019
  • AcceptedDec 11, 2019
  • PublishedAug 5, 2021

Abstract


Acknowledgment

Jie AN and Miaomiao ZHANG have been supported partly by National Natural Science Foundation of China (Grant Nos. 61972284, 61472279). Jie AN, Lingtai WANG, Bohua ZHAN and Naijun ZHAN have been supported partly by National Natural Science Foundation of China (Grant Nos. 61625206, 61732001, 61872341). Bohua ZHAN has been partly supported by CAS Pioneer Hundred Talents Program (Grant No. Y9RC585036). The authors would like to thank the anonymous reviewers for their insightful comments and suggestions raised in the reviewing process.


References

[1] Angluin D. Learning regular sets from queries and counterexamples. Inf Computation, 1987, 75: 87-106 CrossRef Google Scholar

[2] Aarts F, Vaandrager F W. Learning I/O automata. In: Proceedings of the 21th International Conference on Concurrency Theory, Paris, 2010. 71--85. Google Scholar

[3] Howar F, Steffen B, Jonsson B, et al. Inferring canonical register automata. In: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation, Philadelphia, 2012. 251--266. Google Scholar

[4] Aarts F, Fiterau-Brostean P, Kuppens H, et al. Learning register automata with fresh value generation. In: Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing, 2015. 165--183. Google Scholar

[5] Cassel S, Howar F, Jonsson B. Active learning for extended finite state machines. Form Asp Comp, 2016, 28: 233-263 CrossRef Google Scholar

[6] Bollig B, Habermehl P, Kern C, et al. Angluin-style learning of NFA. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, 2009. 1004--1009. Google Scholar

[7] Farzan A, Chen Y, Clarke E M, et al. Extending automated compositional verification to the full class of omega-regular languages. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, 2008. 2--17. Google Scholar

[8] Li Y, Chen Y, Zhang L J, et al. A novel learning algorithm for büchi automata based on family of dfas and classification trees. In: Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, 2017. 208--226. Google Scholar

[9] Bollig B, Katoen J, Kern C, et al. libalf: the automata learning framework. In: Proceedings of the 22nd International Conference on Computer Aided Verification, Edinburgh, 2010. 360--364. Google Scholar

[10] Isberner M, Howar F, Steffen B. The open-source learnlib---a framework for active automata learning. In: Proceedings of the 27th International Conference on Computer Aided Verification, San Francisco, 2015. 487--495. Google Scholar

[11] Fiterau-Brostean P, Janssen R, Vaandrager F W. Combining model learning and model checking to analyze TCP implementations. In: Proceedings of the 28th International Conference on Computer Aided Verification, Toronto, 2016. 454--471. Google Scholar

[12] Verwer S, de Weerdt M, Witteveen C. Efficiently identifying deterministic real-time automata from labeled data. Mach Learn, 2012, 86: 295-333 CrossRef Google Scholar

[13] Dima C. Real-time automata. J Autom Languages Combinat, 2001, 6: 3--23. Google Scholar

[14] Verwer S, Weerdt M, Witteveen C. The efficiency of identifying timed automata and the power of clocks. Inf Computation, 2011, 209: 606-625 CrossRef Google Scholar

[15] Alur R, Fix L, Henzinger T A. Event-clock automata: a determinizable class of timed automata. Theor Comput Sci, 1999, 211: 253-273 CrossRef Google Scholar

[16] Grinchtein O, Jonsson B, Leucker M. Learning of event-recording automata. Theor Comput Sci, 2010, 411: 4029-4054 CrossRef Google Scholar

[17] Maler O, Mens I. Learning regular languages over large alphabets. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, 2014. 485--499. Google Scholar

[18] Drews S, D'Antoni L. Learning symbolic automata. In: Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, 2017. 173--189. Google Scholar

[19] Alur R, Dill D L. A theory of timed automata. Theor Comput Sci, 1994, 126: 183-235 CrossRef Google Scholar

[20] Stigge M, Ekberg P, Guan N, et al. The digraph real-time task model. In: Proceedings of the 17th IEEE Real-Time and Embedded Technology and Applications Symposium, Chicago, 2011. 71--80. Google Scholar

[21] Abdullah J, Dai G, Mohaqeqi M, et al. Schedulability analysis and software synthesis for graph-based task models with resource sharing. In: Proceedings of the 24th IEEE Real-Time and Embedded Technology and Applications Symposium, Porto, 2018. 261--270. Google Scholar

[22] Denning D E, Sacco G M. Timestamps in key distribution protocols. Commun ACM, 1981, 24: 533-536 CrossRef Google Scholar

[23] Verwer S, Weerdt M D, Witteveen C. An algorithm for learning real-time automata. Electrical Engineering Mathematics & Computer Science, 2007. Google Scholar

[24] Tappler M, Aichernig B K, Larsen K G, et al. Learning timed automata via genetic programming. 2018,. arXiv Google Scholar

[25] Learning probabilistic real-time automata from multi-attribute event logs. IDA, 2013, 17: 93-123 CrossRef Google Scholar

[26] Berg T, Grinchtein O, Jonsson B, et al. On the correspondence between conformance testing and regular inference. In: Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering, Edinburgh, 2005. 175--189. Google Scholar

[27] Hopcroft J E, Ullman J D. Introduction to Automata Theory, Languages, and Computation. Boston: Addison-Wesley Publishing Company, 1979. Google Scholar

[28] Ouaknine J, Worrell J. On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science, Turku, 2004. 54--63. Google Scholar

[29] Wang L, Zhan N, An J. The Opacity of Real-Time Automata. IEEE Trans Comput-Aided Des Integr Circuits Syst, 2018, 37: 2845-2856 CrossRef Google Scholar

  • Figure 1

    (Color online) (a) A DRTA $\mathcal{A}$ and (b) the corresponding CRTA $\mathbb{A}$. An initial state is indicated by `Start' and an accepting state is represented by a double cycle in this paper.

  • Figure 2

    The real-time observation table ${{\boldsymbol~T}_7}$, the corresponding DFA ${M}_7$, and the hypothesis $\mathcal{H}_7$ in Examples example:T_to_Mand example:M_To_H.

  • Figure 3

    The new table ${\boldsymbol~T}'_5$ after adding the counterexample $((a,0)(a,5.8),-)$ directly and the generated DFA ${M}_5'$.

  • Figure 4

    The real-time observation tables for the illustrative example.

  • Figure 5

    The DFAs and hypotheses for the illustrative example.

  • Figure 6

    (Color online) (a) The relation between $|Q|$ and the number of membership queries; (b) the relation between $m$ and the number of membership queries; (c) the relation between $k$ and the number of membership queries; (d) the relation between $|Q|$ and the number of equivalence queries; (e) the relation between $m$ and the number of equivalence queries; protectłinebreak(f) the relation between $k$ and the number of equivalence queries.

  •   

    Algorithm 1 equivalence_query($\mathcal{H}$)

    Require:a hypothesis $\mathcal{H}$.

    Output:equivalent : a Boolean value to identify whether $\mathcal{L}(\mathcal{H})~=~\mathcal{L}(\mathbb{A})$, where CRTA $\mathbb{A}$ recognizes the target language; ctx : a counterexample.

    equivalent $\leftarrow$ $\bf{false}$; ctx $\leftarrow$ $\epsilon$;

    ${\rm~flag}_{-},{\rm~flag}_{+}~\leftarrow$ $\bf{true}$;

    if $\mathcal{L}(\mathcal{H})~\cap~\overline{\mathcal{L}(\mathbb{A})}\neq\emptyset$ then

    ${\rm~flag}_{-}$ $\leftarrow$ $\bf{false}$;

    Select a timed word $\boldsymbol{\omega}$ from $\mathcal{L}(\mathcal{H})\cap\overline{\mathcal{L}(\mathbb{A})}$; //Negative counterexample

    ${\rm~ctx}_{-}$ $\leftarrow$ $(\boldsymbol{\omega},~-)$;

    end if

    if $\overline{\mathcal{L}(\mathcal{H})}~\cap~\mathcal{L}(\mathbb{A})\neq\emptyset$ then

    ${\rm~flag}_{+}$ $\leftarrow$ $\bf{false}$;

    Select a timed word $\boldsymbol{\omega}'$ from $\overline{\mathcal{L}(\mathcal{H})}\cap\mathcal{L}(\mathbb{A})$; //Positive counterexample

    ${\rm~ctx}_{+}$ $\leftarrow$ $(\boldsymbol{\omega}',~+)$;

    end if

    equivalent $\leftarrow$ ${\rm~flag}_{-}~\wedge~{\rm~flag}_{+}$;

    if equivalent = $\bf{false}$ then

    ctx $\leftarrow$ select a counterexample from ${\rm~ctx}_{+}$ and ${\rm~ctx}_{-}$;

    end if

    return equivalent, ctx.

  • Table 1  

    Table 1The information of the experiments in which the alphabet size $|\Sigma|=k=4$ and the maximal partition size $m~=~4~\geq~|\Psi_{q,\sigma}^{\lambda^c}|$ and the number of states $|Q|=n$ ranges in $\{5,7,9,11,13,15\}$

    Case ID $|Q|$ $|\Delta|_{\text{mean}}$ MembershipEquivalence$t_{\text{mean}}$
    $N_{\text{min}}$ $N_{\text{mean}}$ $N_{\text{median}}$ $N_{\text{max}}$ $N_{\text{min}}$ $N_{\text{mean}}$ $N_{\text{median}}$ $N_{\text{max}}$
    4_4_4 5 35.8 248 295.5 278 376 17 28.1 28 38 3.4
    6_4_4 7 54.6 505 699.8 708 948 33 45.4 46 65 29.0
    8_4_4 9 68.0 888 1138.2 1130 1488 40 54.0 54 66 40.7
    10_4_4 11 83.7 1225 1824.6 1864 2560 50 68.4 69 90 145.1
    12_4_4 13 99.6 1561 2476.8 2620 3278 64 79.9 79 97 280.0
    14_4_4 15 117.6 2376 3258.7 3050 4914 78 97.9 98 114 500.1
  • Table 2  

    Table 2The information of the experiments in which the alphabet size $|\Sigma|=k=4$ and the number of states $|Q|=n=8$ and the maximal partition size $m~\geq~|\Psi_{q,\sigma}^{\lambda^c}|$ ranges from 2 to 7

    Case ID $m$ $|\Delta|_{\text{mean}}$ MembershipEquivalence$t_{\text{mean}}$
    $N_{\text{min}}$ $N_{\text{mean}}$ $N_{\text{median}}$ $N_{\text{max}}$ $N_{\text{min}}$ $N_{\text{mean}}$ $N_{\text{median}}$ $N_{\text{max}}$
    7_4_2 2 45.7 435 629.0 629 861 18 22.8 22 29 8.9
    7_4_3 3 51.1 495 666.4 654 861 26 31.0 30 38 14.9
    7_4_4 4 58.1 575 787.8 771 1022 36 45.4 45 66 30.1
    7_4_5 5 60.6 610 864.9 837 1162 34 49.7 49 67 28.2
    7_4_6 6 78.6 715 1160.6 1167 1554 58 83.0 83 106 97.5
    7_4_7 7 83.2 900 1322.7 1357 1694 70 93.4 95 124 142.4
  •   

    Algorithm 2 Learning real-time automaton

    Require:the real-time observation table ${\boldsymbol~T}~=~(\Sigma,~\boldsymbol{\Sigma},~\boldsymbol{S},~\boldsymbol{R},~\boldsymbol{E},~f,~{\rm~row})$.

    Output:the hypothesis $\mathcal{H}$ recognizing the target language.

    $\boldsymbol{S}\leftarrow\{\boldsymbol{\epsilon}\}$; $\boldsymbol{R}\leftarrow\{(\sigma,~0)~\,~|\,\sigma~\in~\Sigma~\}$; $\boldsymbol{E}\leftarrow\{\boldsymbol{\epsilon}\}$;

    Fill ${\boldsymbol~T}$ by membership queries;

    equivalent $\leftarrow$ $\bf{false}$;

    while equivalent = $\bf{false}$ do

    prepared $\leftarrow$ is_prepared(${\boldsymbol~T}$); // Whether the table is prepared

    while prepared = $\bf{false}$ do

    if ${\boldsymbol~T}$ is not closed then

    make_closed(${\boldsymbol~T}$);

    end if

    if ${\boldsymbol~T}$ is not consistent then

    make_consistent(${\boldsymbol~T}$);

    end if

    if ${\boldsymbol~T}$ is not evidence-closed then

    make_evidence_closed(${\boldsymbol~T}$);

    end if

    if ${\boldsymbol~T}$ is not prefixed-closed then

    make_prefix_closed(${\boldsymbol~T}$);

    end if

    prepared $\leftarrow$ is_prepared(${\boldsymbol~T}$);

    end while

    $\mathcal{H}~\leftarrow$ build_hypothesis(${\boldsymbol~T}$); // Constrcuting a hypothesis $\mathcal{H}$

    equivalent, ctx $\leftarrow$ equivalence_query($\mathcal{H}$);

    if equivalent = $\bf{false}$ then

    ctx_processing(${\boldsymbol~T}$, ctx); //The counterexample processing

    end if

    end while

    return $\mathcal{H}$.

  • Table 3  

    Table 3The information of the experiments in which the number of states $|Q|=n=8$ and the maximal partition size $m=4\geq|\Psi_{q,\sigma}^{\lambda^c}|$ and the alphabet size $|\Sigma|=k$ ranges from 2 to 7

    Case ID $k$ $|\Delta|_{\text{mean}}$ MembershipEquivalence$t_{\text{mean}}$
    $N_{\text{min}}$ $N_{\text{mean}}$ $N_{\text{median}}$ $N_{\text{max}}$ $N_{\text{min}}$ $N_{\text{mean}}$ $N_{\text{median}}$ $N_{\text{max}}$
    7_2_4 2 33.7 296 568.7 570 798 23 31.0 33 37 7.8
    7_3_4 3 45.1 420 649.0 648 980 25 36.9 36 56 14.2
    7_4_4 4 58.1 575 787.8 771 1022 36 45.4 45 66 30.1
    7_5_4 5 73.1 695 1034.6 1060 1428 43 56.3 53 79 83.7
    7_6_4 6 86.0 870 1127.5 1104 1589 48 64.1 62 89 88.4
    7_7_4 7 100.8 1020 1308.7 1299 1743 48 74.0 77 99 202.2
qqqq

Contact and support