DKL: an efficient algorithm for learning deterministic Kripke structures
- PDF / 2,391,474 Bytes
- 41 Pages / 439.37 x 666.142 pts Page_size
- 55 Downloads / 174 Views
DKL: an efficient algorithm for learning deterministic Kripke structures Rabia Mazhar1 · Muddassar Azam Sindhu1 Received: 29 September 2018 / Accepted: 31 August 2020 © Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract There has been a recent growth of interest in software engineering community to use grammatical inference, aka automaton learning, in software engineering applications. This is primarily due to the reason that capacity of underlying hardware resources has improved significantly over the last years; which has enabled the use of this approach beyond the toy examples in a greater frequency. In this paper, we present a new grammatical inference algorithm, DKL, to learn deterministic Kripke structures. The DKL is only the second of its kind for incremental learning of deterministic Kripke structures. Earlier, IKL algorithm was introduced for learning deterministic Kripke structures but it often constructs a hypothesis much larger in state size than the target Kripke structure. This problem is known as state-space explosion and it primarily occurs due to the sub-direct product construction used in the IKL design, which in turn affects time efficiency of IKL; especially when it is used for practical applications of software engineering. The DKL algorithm is designed to resolve the problem of state-space explosion. We give a proof of correctness and termination of the DKL algorithm. We also compared the performance of DKL with IKL by implementing an evaluation framework. Our results show that DKL is more efficient in terms of time in reaching the target automaton than the IKL algorithm and is not prone to the problem of state-space explosion. Keywords Grammatical inference · DKL · Incremental learning · IKL · Kripke structure · State space explosion
1 Introduction The interest of software engineering community has grown considerably in automaton learning (AL) during the past decade or so. This is primarily due to the possibility to use AL for solving practical problems of software engineering. For example, AL has been applied in formal verification (e.g [4,11,18]). The work of [20] and [12] discusses the use of AL in
B
Muddassar Azam Sindhu [email protected] Rabia Mazhar [email protected]
1
Computer Science Department, Quaid i Azam University, Islamabad 45320, Pakistan
123
R. Mazhar, M. A. Sindhu
software testing and [3] describes how AL algorithms can be exploited for model inference. All the above mentioned applications focus on the concept of learning a formal model of a complex software system and then analyzing its behavioral correctness via static analysis techniques like model checking. An AL algorithm can be incremental, sequential or complete in nature. An AL algorithm is said to be incremental when it learns a finite series of hypotheses H0 , H1 , ..., Hm−1 after observing the responses r0 , r1 , ..., rm−1 respectively; generated by an unknown target automaton M corresponding to the inputs i 0 , i 1 , ..., i m−1 . A typical AL algorithm is guaranteed to converge to
Data Loading...
