Approximate Active Learning of Nondeterministic Input Output Transition Systems Electronic Communications of the EASST Volume 72 (2015) Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015) Approximate Active Learning of Nondeterministic Input Output Transition Systems Michele Volpato and Jan Tretmans 15 pages Guest Editors: Gudmund Grov, Andrew Ireland ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Approximate Active Learning of Nondeterministic Input Output Transition Systems Michele Volpato1∗ and Jan Tretmans2 1 m.volpato@cs.ru.nl, 2 tretmans@cs.ru.nl Radboud Universiteit, Nijmegen, The Netherlands 2 TNO - ESI, Eindhoven, The Netherlands Abstract: Constructing a model of a system for model-based testing, simulation, or model checking can be cumbersome for existing, third party, or legacy components. Active automata learning, a form of black-box reverse engineering, and in particular Angluin’s L⋆ algorithm, support the automatic inference of a model from a Sys- tem Under Learning (SUL), through observations and tests. Most of the algorithms based on L⋆, however, deal with complete learning of deterministic models, thus be- ing unable to cope with nondeterministic SULs, and always learning a complete and correct model as they are based on equivalence between the SUL and the model. We present an adaptation of Angluin’s algorithm for active learning of nondeterministic, input-enabled, input-output transition systems. It enables dealing with nondetermin- istic SULs, and it allows to construct partial, or approximate models, by expressing the relation between the SUL and the learned model as a refinement relation, not necessarily an equivalence. Thus, we can reason about learned models being more, or less precise than others. Approximate learning has benefits in model-based re- gression testing: we need not to wait until a complete model has been learned; with an approximate model ioco-based regression testing can start. Keywords: Approximate Active Learning, Nondeterminism, ioco 1 Introduction Model-based testing, model-driven design, model simulation, model checking: once you have a model of the behaviour of a software component, all kinds of analyses can be performed con- tributing to the construction of better software in less time. A key problem, however, is the initial construction of a model, in particular for existing, third party, or legacy components, for which no or only limited documentation is available. Active automata learning helps with automatically inferring a state-based model from the be- haviour of a System Under Learning (SUL) by observing and testing that behaviour, i.e., through black-box reverse engineering. Automata learning started with the L⋆ algorithm by Angluin [Ang87], after which several variations and improvements were made, among others, for Mealy machines [RS93, Nie03] for learning models of reactive systems such as controllers and network ∗ This research is supported by the Dutch Technology Foundation STW, which is part of the Netherlands Organisation for Scientific Research (NWO), and which is partly funded by the Ministry of Economic Affairs. 1 / 15 Volume 72 (2015) mailto:m.volpato@cs.ru.nl mailto:tretmans@cs.ru.nl Approximate Active Learning of Nondeterministic IOTSs protocols. Most of them, however, concern learning of deterministic systems, which means that (i) they cannot deal with nondeterministically behaving systems, and, (ii) the correctness of a learned model is based on an isomorphism with the SUL. In particular the latter implies that a learned model is either complete and correct, or not correct at all. We present an adaptation of L⋆ for active learning of nondeterministic, input-enabled, input- output transition systems [Tre96]. Nondeterminism allows to reason about partially correct mod- els, using relations that are not equivalences, e.g., pre-orders. This enables reasoning of learned models being better than another learned model, and thus to approximate the model of the SUL. In particular we want to (i) avoid the equivalence checking step used in L⋆, which is impossible to implement in practice, given non-exhaustiveness of testing, and, (ii) define a relation between a partially learned model and the SUL, as an invariant through the learning process. The notion of refinement, for the approximate models, is based on the ioco-theory for model- based testing [Tre96], which defines a framework comprehending a precise notion of confor- mance in terms of implementation relations that can deal with nondeterminism. The learning approach is based on L⋆, with corresponding observation table. At any moment during the learn- ing process an under- and an over-approximation model is constructed for which we prove a refinement-relationship to the SUL. After any step the algorithm can be stopped with a cor- rect, but perhaps not precise enough model. Continuation will lead to gradually better models, until the model is considered precise enough. The learning algorithm uses properties of input- output labelled transition systems for optimization. Moreover, it must be assumed that, due to nondeterminism, there exists an oracle that knows when all nondeterministic outputs have been observed. Without this assumption the over-approximation can only be the most imprecise, yet correct model, i.e., chaos. An implementation of such an oracle depends on the system under learning: does observing an output x exclude the possibility to observe the output y after the same input? Does repeating the same sequence of inputs k times produce all observable outputs after that sequence? Approximate learning can have big advantages in regression testing, for example when testing the complete model is beyond feasibility: because already with a partial model, model-based ioco-regression testing can start. Related Work This paper improves the results presented in our previous work [VT14] by weakening two assumptions on which the learning of nondeterministic systems was based. First, we assumed in [VT14] that we can somehow obtain all nondeterministic outputs in a particular state at once (i.e., the set out(SUL after σ); cf. Section 2). In this paper, more realistically, we observe all outputs individually, but we assume the presence of an oracle that knows when all nondeterministic outputs have been observed (e.g., by repeating observations often enough). The difference with [VT14] is that we are now able to deal with incomplete observations, i.e., we can still construct a model even if not all outputs have been observed. Secondly, we assumed in [VT14] the ability to exhaustively check the equivalence of a learned model w.r.t. the SUL (called equivalence exhaustiveness, or equivalence oracle in [Ang87]). This assumption is completely dropped, implying that we can never be sure anymore to have learned the final, complete model. The assumption is replaced by the property that at any moment during the learning process we can always construct a correct approximation of the complete model, in Proc. AVoCS 2015 2 / 15 ECEASST the sense of having an ioco-like relation between the currently learned model and the (unknown) complete model. Active learning of observable nondeterministic finite state machines (ONFSMs) [Ea10, Pa13], attempts to learn a deterministic model of systems behaving as a nondeterministic Mealy ma- chine. Such a behaviour is comparable to a labelled transition system with alternation between inputs and outputs. The work in [MS11] applies learning-based testing to reactive systems by combining incremental learning algorithms with formal requirements specified in temporal logic. The idea of incremental learning is similar to the approximate learning and it is a good candidate to be considered for future work. 2 Preliminaries Labelled transition systems and ioco relation [Tre96] A labelled transition system is a 5- tuple 〈Q,LI,LU ,→,q0〉, where Q is a set of states, LI and LU are two disjoint sets of inputs and outputs (labels), respectively, → is the transition relation and q0 ∈ Q is the initial state. We may refer at a labelled transition system by using its initial state. We use q λ −→ q′ for (q,λ ,q′) ∈→ and we say that q enables λ . We shorten LI ∪LU by L. A special label τ is used for internal, unobservable transitions. Let q,q′ be states and ε be the empty sequence, we define q ε =⇒ q′ ⇐⇒ q = q′ or q τ −→ ... τ −→ q′. Given a label λ , we define q λ =⇒ q′ as q ε =⇒ p λ −→ p′ ε =⇒ q′ and extend =⇒ for sequences of labels in the usual way. The set traces(q) = {σ ∈ L∗ | ∃q′ : q σ =⇒ q′} indicates the enabled traces from a state q. We denote the set of states reachable from q via a trace σ as (q after σ) ={q′ | q σ =⇒ q′}. We say that such states are reached by running σ from q. A system is deterministic iff |(q after σ)|≤ 1. We write σ1·σ2 or just σ1σ2 to denote the concatenation of sequences σ1 and σ2. We extend this notation to sets of sequences in the usual way. A state q is called quiescent if ∀λ ∈ LU ∪{τ} : q 6 λ −→ q′ for all q′ ∈ Q. Let δ 6∈ LI ∪LU , Lδ is defined as L∪{δ} and 〈Q,LI,LU ∪{δ},→δ ,q0〉 is the labelled transition system 〈Q,LI,LU ,→ ,q0〉 to which transitions we add (q,δ ,q) for all quiescent states q. We identify δ as quiescence and we sometimes include it in the outputs. The set of suspension traces is Straces(q) = {σ ∈ L∗ δ | ∃q′ . q σ =⇒ q′}. The set of outputs, including quiescence, that are enabled in a set of states P is out(P) = {λ ∈ LU ∪{δ} |∃q ∈ P,q ′ ∈ Q : q λ =⇒ q′}. In an input-enabled labelled transition system, also called input-output transition system, all inputs are enabled in every state. Given a set F ⊆ L∗ δ , an input-output transition system i and a labelled transition system s, we define: i iocoF s ⇐⇒ ∀σ ∈ F : out(i after σ) ⊆ out(s after σ) and i ioco s ⇐⇒ i iocoStraces(s) s. The ioco relation is used for testing the conformance of an implementation w.r.t. a given specification. Active Learning of Regular Languages Angluin’s L⋆ [Ang87] is a well known, efficient al- gorithm that, given an alphabet L, infers a Deterministic Finite Automaton (DFA) for a regular language over L. First some membership queries, in the form “Is this word in the target lan- guage?”, are asked in order to construct an hypothesis DFA. Then an oracle replies to an equiv- alence query affirmatively if the hypothesis is equivalent to the system under learning (SUL), otherwise it provides a counterexample that can be used to improve the hypothesis, by asking more membership queries, and the process is repeated. The central structure of the L⋆ algorithm 3 / 15 Volume 72 (2015) Approximate Active Learning of Nondeterministic IOTSs is the observation table. The observation table is a triple (S,E,T ), where S is a prefix-closed set of traces that represent access sequences to states of the learned DFA and E is a suffix-closed set of traces that represent distinguishing sequences of the states in the learned DFA. The func- tion T maps traces in ((S∪S·L)·E) to either TRUE, if that trace is accepted by the language, or FALSE, otherwise. In T both access sequences and their one letter extensions are considered, because this information is needed in order to construct a valid DFA. If two traces in (S∪S·L) are mapped to the same boolean value by T for each suffix in E , then they represent the same state. (S,E,T ) is called observation table because one can depict the elements of (S∪S·L) as rows and the elements of E as columns. Each entry s·e in the table is given by the result of T (s·e). We do not give precise definitions for active learning of DFAs. However, in the next section, we will provide detailed definitions for active learning of input-output transition systems. 3 Manipulating the Observation Table In this paper we aim to learn a nondeterministic input-output transition system by using the L⋆ approach, with some differences: we do not alternate membership and equivalence queries, because we introduce the concept of preciseness that will guide to the termination of the learning process. Furthermore, we assume that the SUL behaves as a (nondeterministic) input-output transition system, and for this reason, in the observation table, we store sets of outputs instead of boolean values. We will present our notions of closedness and consistency, which are similar to the ones used in Angluin’s L⋆. In the rest of the paper we use SUL for both the system under learning and the labelled transition system that represents it. 3.1 Nondeterministic Observation Table We define a nondeterministic observation table, from now on simply observation table, as a triple (S,E,T ) where S and E are non-empty, finite sets of traces over Lδ , prefix-closed and suffix-closed, respectively, and T is a function that maps traces in ((S ∪S·Lδ )·E) to a subset of (LU ∪{δ}). We often use s for elements of (S∪S·Lδ ) and e for elements of E . A matrix view of the table has the prefixes, i. e., elements of (S∪S·Lδ ), as row labels, and suffixes, i. e., elements of E as column labels. Each entry contains the observed outputs after running the related prefix followed by the related suffix on the SUL. An image of T is a set of outputs due to the nondeterministic behaviour of the SUL. Furthermore, at any point in the process of learning, there might be some entries in the observation table whose content is not completely known and others for which we are sure that all the enabled outputs, for that specific trace, have been observed. In the latter case we mark the entry as complete, more precisely, if T (s·e) is marked as complete, then T (s·e) = out(SUL after s·e). If an entry T (s·e) is incomplete, i. e., it is not marked as complete, then T (s·e)⊆ out(SUL after s·e). In the learning process, the table is modified repeatedly, adding rows or columns and changing the content of entries. New entries are not marked as complete and T maps them to the empty set. Given an observation table (S,E,T ) and a trace s ∈ (S∪S·Lδ ), row(s) denotes the function from E to 2(LU∪{δ}) defined by row(s)(e) = T (s·e). Given a trace s ∈ S, if an output λ is not in T (s·ε), because it is either not enabled or not observed yet, then row(s·λ ) is not defined. Proc. AVoCS 2015 4 / 15 ECEASST In classic L⋆, for each entry of the table, it is necessary to ask a membership query in order to fill that entry. While learning an input-output transition system, some entries can be filled automatically, and some others are not needed at all, because of some properties of labelled transition systems. We will present such special cases in the next section. 3.2 Filling the Observation Table In order to be able to infer a valid input-output transition system from an observation table, also called hypothesis, we need to fill the table. Asking an output query, the analogue of a membership query in Section 2, consists of obtaining an output that is enabled after running a trace σ on the SUL: output(σ) gives an output x (including quiescence) such that x ∈ out(SUL after σ). For deterministic systems, replying to this kind of questions is easy. If a trace is enabled from the initial state, then the output obtained from the output query on that trace is the only possible output. An implementation of the output query for deterministic systems just needs to run the sequence, waiting for all the outputs during the process. For nondeterministic systems, on the contrary, given a trace σ , processing output(σ) is not so trivial. We are not sure that we will observe precisely the outputs that are contained in σ while running it. If we assume that there exists a maximum number k such that, after running a trace k times, we are sure of having observed all the possible outputs after that trace, then the output query can be implemented. It’s out of scope of this paper to give an implementation of the output query. We assume that such an implementation exists. We assume also the existence of another type of queries: the completeness queries. Given a sequence of labels and a set of outputs (the observed outputs so far, after that sequence), if the completeness query replies affirmatively then the set of outputs defines exactly the outputs that are enabled after running that sequence on the SUL. As for the output query, we do not provide an implementation of the completeness query. An approach for implementing it, similarly to [Pa13], assuming that after a given number of output queries on the same sequence, we are sure to have observed all the possible outputs, is testing if that many output queries have already been asked. We couple output and completeness queries in order to fill the observation table. When an output query is answered, there are more entries in the table that can be updated with the result of that query. The result of output(σ1·δ·σ2) must also be a possible outcome of output(σ1·σ2), given that, in a labelled transition system, quiescence is always modelled as a self loop. For this reason we define δ∗(σ) as the smallest set s.t. σ ∈ δ∗(σ) and σ1·δ·σ2 ∈ δ∗(σ) ⇒ σ1·σ2 ∈ δ ∗(σ). We use update(S,E,T) for populating the observation table. In Algorithm 1, for each incomplete entry T (s·e) of the observation table, if s·e ends with δ only quiescence, or some inputs, can be enabled, thus we set T (s·e) to {δ} and mark it as complete. If s ends with δ and the state reachable by the longest proper prefix of s enables only δ , then there will be a δ self loop in that state, thus row(s·δ ) = row(s), Lines 8 to 11. If none of the previous special cases is met, then we ask an output query for the trace s·e and update each entry identified by s·e. Afterwards, a completeness query is asked, and the entries are updated accordingly. Example 1 Figure 1b gives an observation table for the system under learning of Figure 1a. This is not the only possible observation table; to a different nondeterministic reply to an output or a completeness query corresponds a different table. We will show later that the learning 5 / 15 Volume 72 (2015) Approximate Active Learning of Nondeterministic IOTSs Algorithm 1 update(S,E,T) 1: for each s ∈ (S∪S·Lδ ),e ∈ E s.t. row(s) is defined do 2: if T (s·e) is marked as complete then 3: continue; 4: if s·e ends with δ then 5: T (s·e) ←{δ} 6: mark T (s·e) as complete 7: else 8: if s = s′·δ ∧T (s′·ε) ={δ}∧T (s′·ε) is complete then 9: T (s·e) ← T (s′·e) 10: if T (s′·e) is complete then 11: mark T (s·e) as complete 12: else 13: out ← output(s·e) 14: for each s′ ∈ (S ∪ S·Lδ ),e ′ ∈ E s.t. s′·e′ ∈ δ∗(s·e) do 15: T (s′·e′)← T (s′·e′) ∪{out} 16: if isComplete(s·e) then 17: for each s′ ∈ (S∪S·Lδ ),e ′ ∈ E s.t. s′·e′ = s·e do 18: mark T (s′·e′) as complete process starts with S = E ={ε}, thus S·Lδ ={a,x,y,δ}. Accordingly to Subsection 3.1, row(x) and row(y) are not defined, thus we do not add them to the table. While executing Algorithm 1, none of the entries is complete. The output queries will reply with the only possible output for each entry: output(ε) = δ and output(a) = δ . Let’s say that the completeness queries for ε and a result in FALSE, then we do not mark those entries as complete. Because of Line 5 we know that δ will be added in the third entry and the entry will be marked as complete. a a x a,y (a) An iots q, LI = {a} and LU ={x,y} ε S ε 〈{δ},⊥〉 S·Lδ a 〈{δ},⊥〉 δ 〈{δ},⊤〉 (b) A possible first obser- vation table for q. ε S ε 〈{δ},⊥〉 δ 〈{δ},⊤〉 S·Lδ a 〈{δ},⊥〉 δ a 〈{δ},⊥〉 δ δ 〈{δ},⊤〉 (c) The observation table after it has been stabilized. Figure 1: Running example used in this paper. FALSE is replaced by ⊥ and TRUE by ⊤. If isComplete(s·e) does not reply affirmatively, then we do not know if we have observed all the outputs enabled after s·e. This uncertainty can be expressed in the current hypothesis induced by the learning algorithm in either a restrictive way, considering the set as complete, or in a permissive way, considering all outputs, including quiescence, as a possible outcome for s·e. These two different approaches lead us to construct two different hypotheses: the re- strictive H − and the permissive H +. The hypothesis H − is constructed in a way similar to the hypothesis in [VT14], where this uncertainty was not considered. In order to build the other hypothesis, H +, we need to give a formal notion of what its states are, and how to han- dle the uncertain transitions. For this reason, we define a function row+, similar to row: given a trace s ∈ (S ∪S·Lδ ), row + denotes the function from E to (2(LU∪{δ}),{TRUE,FALSE}) de- fined by row+(s)(e) = (T (s·e),isComplete(s·e)). Given two prefixes s1,s2 ∈ (S∪S·Lδ ) and two suffixes e1,e2 ∈ E we define the equivalence over marked entries of the table as T (s1·e1) = + T (s2·e2) if and only if T (s1·e1) = T (s2·e2) and isComplete(s1·e1) = isComplete(s2·e2). As for the function row, given s ∈ S, if an output λ 6∈ T (s·ε), row+(s·λ ) is not defined. If row(s) is not defined, also row+(s) is not, and vice versa. The two hypotheses H − and H + are suspension automata [Tre96], label-deterministic ver- Proc. AVoCS 2015 6 / 15 ECEASST sions of some labelled transition systems, where quiescence has been made explicit. Ideally, we want to stop the learning process when either the set of traces of H − or the set of traces of H + is equivalent to the set of suspension traces of SUL. Given the nondeterministic nature of labelled transition systems, we are satisfied when we find a good approximation of SUL. We will elaborate more on this concept in Section 5. 3.3 Global closedness and consistency In the classic L⋆ algorithm, two properties of the observation table are necessary in order to construct an hypothesis: closedness and consistency. In this paper we derive two different hy- potheses H − and H +, and for this reason, we need to define similar properties for constructing both of them. Global closedness, Definition 1, extends the notion of closedness introduced in [VT14] to rows with cells that are not marked as complete. A globally closed observation table must be closed on both row and row+ functions. Closedness on row+ implies closedness on row, given the definition of row+, thus it is enough to check only the most specific one. Definition 1 An observation table (S,E,T ) is globally closed if ∀s′ ∈ (S·Lδ ) s.t. row +(s′) is defined: ∃s ∈ S such that row+(s′) = row+(s) Note that prefixes whose function row is not defined are not taken into consideration for global closedness. The same is true for global consistency. Two elements in S that are mapped in the same way by row (resp. row+), represent the same state in H − (resp. H +). Thus their one label extensions, in S·Lδ , must also represent the same state. Definition 2 An observation table (S,E,T ) is globally consistent if ∀s1,s2 ∈ S: row(s1) = row(s2) ⇒∀λ ∈ Lδ . row(s1λ ) = row(s2λ ) AND row+(s1) = row +(s2)⇒∀λ ∈ Lδ . row +(s1λ ) = row +(s2λ ) A globally closed and consistent observation table is called stable. Algorithm 2 stabilizes a given observation table. It checks for global closedness and global consistency. If any of Algorithm 2 Stabilize observation table 1: while not globally closed or consistent do 2: if not globally closed then 3: pick an s′ ∈ (S·Lδ ) such that ∀s ∈ S, row+(s′) 6= row+(s)∧row+(s′)is defined 4: S ← S∪{s′} 5: u pdate(S,E,T ) 6: if not globally consistent then 7: pick λ ∈ Lδ and e ∈ E such that the suffix λ·e is inconsistent with row or row+ 8: E ← E ∪{λ·e} 9: u pdate(S,E,T ) 10: return the stable observation table (S,E,T ) the two properties is not valid, the algorithm takes the same actions that are taken for classic closedness and consistency, i. e., either adding some elements to S from S·Lδ , or adding one or more elements to E . After each step the table is updated again, because new entries are created. Note that only prefixes whose row function is defined are added to S. 7 / 15 Volume 72 (2015) Approximate Active Learning of Nondeterministic IOTSs Example 2 Let us consider the observation table of Example 1. It is not globally closed, be- cause row+(δ ) does not have a representative in S. Thus we add δ to S. Once quiescence has been observed, no other output can be observed again, unless an input is provided. Thus row(δ x) can never be defined. After having updated the table, a possible result, due to nondeterminism, is the table of Figure 1c. Now the observation table is both globally closed and globally consistent. Quiescence Reducibility The explicit representation of quiescence in suspension automata introduces some properties that must be satisfied by any valid suspension automaton to be suspension-trace equivalent to a labelled transition system. In [Wil07] four properties are iden- tified and in [VT14] it is proven that three of them are always satisfied by the transition systems constructed from any observation table. Even though H − and H + are new constructions, the main points for the proofs in [VT14] are still valid. The fourth one, quiescence reducibility, needs to be checked on the table before the construction of the two hypotheses, after it has been stabilized. It results in adding some suffixes to E preserving the observations made so far. We refer the reader to [VT14] for an algorithm that ensures quiescence reducibility. 4 Construction of Hypotheses If T maps a trace s·e to an empty set, then we never observed any output after running s·e. This can happen because s·e contains rare outputs. Rows with an empty set in the first column rep- resent states from which the output behaviour is not known. Empty entries in the table are, by definition, incomplete. During the construction of hypothesis H +, they are handled as full en- tries, where the entire set of outputs, including quiescence, is enabled. For constructing H −, on the contrary, such entries remain empty and if we would use the same hypothesis construction al- gorithm of [VT14] we would obtain some states with no output transitions. A labelled transition system, and in particular a suspension automaton, must be non-blocking, i. e., it must be possible to observe an output, or quiescence, in every state. Thus a naive construction of H − would produce a non valid suspension automaton. For this reason we consider this kind of unknown behaviour as quiescence, and we add a δ -transition to any state which would have no output transitions. If our guess is proven wrong in a future query, then that query will also provide a valid output to add to the empty entry, allowing us to proceed with a “more” correct model. Otherwise, either our guess was correct, or that part of the system was not easily reachable and it is not possible to derive a better model of it. The construction of H − is given by Algorithm 3. It is similar to the one used in [VT14], the only difference is a quiescent state that collects δ -transitions from states with unknown output behaviour. In order to construct H −, Algorithm 3 first creates a state for each row in the top part of the table and the quiescent state ∆. Then it adds, for each state and for each input label, a transition from that state to the state identified by the row function. Finally, for each output, a transition is added only if that output is enabled in that state. If the state enables no outputs, it adds a δ -transition from that state to ∆. Chaotic behaviour In H +, an incomplete entry T (s·e) is treated as a sort of full entry, in which all the outputs that are not yet observed might be observed in future queries. However, the Proc. AVoCS 2015 8 / 15 ECEASST Algorithm 3 Construct H − from a stable and quiescent reducible (S,E,T ) 1: Q ←{row(s) | s ∈ S} 2: Q ← Q∪{∆} 3: add ∆ δ −→ ∆ {∆ is a quiescent state} 4: q0 ← row(ε) 5: for each row(s) ∈ Q do 6: for each λ ∈ LI do 7: add row(s) λ −→ row(s·λ ) 8: if T (s·ε) 6= /0 then 9: for each λ ∈ T (s·ε) do 10: add row(s) λ −→ row(s·λ ) 11: else 12: add row(s) δ −→ row(∆) {Non-blocking} observation table is not able to specify any behaviour for such outputs from a state row+(s) if T (s·ε) is not complete, because row+(s·λ ), where λ is an unobserved output, is not defined. For this reason, during the construction of H +, we keep a non-conservative approach and we allow any behaviour, i. e., we add (row+(s),λ , p) to →, where λ is an output never observed after the query s ∈ S, and p is a chaotic state [BRT04]. Such a chaotic state can be defined in many ways. Figure 2a shows a representation of a chaotic state. The construction of H + starts with χ and χδ as states. Then more states are added according to row +. Output transitions whose behaviour is unknown, i. e., whose target state is unknown, will target χ . Transitions labelled with δ whose behaviour is unknown will target χδ . Algorithm 4 Construct H + from a stable and quiescent reducible (S,E,T ) 1: Q ←{row+(s) | s ∈ S} 2: Q ← Q∪{χ, χδ} 3: q0 ← row +(ε) 4: add χ LU −→ χ ,χ δ −→ χδ and χδ δ −→ χδ 5: for each row+(s) ∈ Q do 6: for each λ ∈ LI do 7: add row+(s) λ −→ row+(s·λ ) 8: for each λ ∈ (LU ∪{δ}) do 9: if λ ∈ T (s,ε) then 10: add row+(s) λ −→ row+(s·λ ) 11: else if T (s,ε) is not complete then 12: if λ = δ then 13: add row+(s) δ −→ χδ 14: else 15: add row+(s) λ −→ χ Example 3 The table of Figure 1c is stable and quiescence reducible. We can construct H − and H +. The construction of H − is easy. There is only one state, with output δ (∆ is not χ χδ δ LI ∪LULI δ (a) Graphical representation of chaotic behaviour. a,δ (b) The hypothesis H − from Figure 1c. χ δ x,y a a δ (c) The hypothesis H + from Figure 1c. Figure 2: Chaotic behaviour and the two hypotheses constructed from Figure 1c. shown in the figure because it is not reachable). All transitions are self loops: Figure 2b. The construction of H + is slightly more complex. First we add the chaotic state (χδ is not drawn in Figure 2c). Then we create two more states, one for row+(ε) and the other for row+(δ ), and finally, we add the transitions to the relevant states. From the state identified by row+(ε), we 9 / 15 Volume 72 (2015) Approximate Active Learning of Nondeterministic IOTSs need to reach the chaotic state for each output that is not in the entry T (ε·ε). This action is not necessary for the state represented by row+(δ ) because T (δ·ε) is complete. Theorem 1 Let (S,E,T ) be a globally closed, globally consistent and quiescent reducible observation table, and let H − and H + be the hypotheses obtained with Algorithm 3 and Algorithm 4, respectively, then: H − ioco H +. 4.1 Conformance Relation on Observed Behaviour We provided the construction of two models, based on the observation table, that represent the current information we have been able to infer from observing the behaviour of the SUL. How can we formally describe how they are related to the SUL? We need to introduce a new confor- mance relation based on that behaviour. The fact that H − and H + are constructed from a limited amount of information, i. e., the replies to some output queries, offers the idea of reasoning in terms of relations restricted to that information only. For this reason we define ioco(S,E,T ) in Definition 3. Informally, a labelled transition system i is ioco(S,E,T ) conforming to another labelled transition system i ′ if and only if, for all the traces that can be constructed from the table (S,E,T ) by concatenating any prefix with any suffix, the set of outputs observable after executing those traces on i can also be observed after executing the same trace on i′. Definition 3 Let (S,E,T ) be an observation table, i and i′ two labelled transition systems, then: i ioco(S,E,T )i ′ ⇐⇒ ∀σ = s·e such that s ∈ (S∪S·Lδ ),e ∈ E ∧row(s) is defined ∧T (s·e) 6= /0 : out(i after σ)⊆ out(i ′ after σ) The system under learning and the two hypotheses are related accordingly to ioco(S,E,T ). Theorem 2 Let (S,E,T ) be a globally closed and consistent observation table obtained from SUL, and H − and H + be the suspension automata constructed using Algorithm 3 and Algorithm 4 respectively. Then H − ioco(S,E,T ) SUL and SUL ioco(S,E,T ) H +. Proof idea. First note that T (s·e) ⊆ out(SUL after s·e). Then the theorem can be proven by showing that H − and H + are consistent with the observation table. Note that, fixing (S,E,T ), the relation ioco(S,E,T ) is transitive, thus H − ioco(S,E,T ) H +. Fur- thermore, SUL ioco(S,E,T ) H − implies that each entry of the observation table must be complete and, thus, Straces(H −) = Straces(H +). Theorem 3 Let (S,E,T ) be a globally closed and consistent observation table obtained from SUL, and i be an input-output transition system, then i ioco SUL ⇒ i ioco(S,E,T ) SUL. Proof idea. It is easy to prove the contrapositive by showing that the concatenation of a prefix s and a suffix e for which out(i after s·e) 6⊆ out(SUL after s·e) is in Straces(SUL). We gave the basis for maintaining an observation table for learning a nondeterministic system and we provided the definitions of the hypotheses that can be constructed from the observation Proc. AVoCS 2015 10 / 15 ECEASST table. In the next section we will discuss the learning process and we will show how to use the concepts introduced so far. 5 Learning Process When learning deterministic systems, under the assumption that a correct and sound equivalence oracle exists, it is proven that the learning process ends when the correct model has been learned. Due to nondeterminism, one can never be sure of having observed all the possible outputs after a given trace, thus we do not know when to stop the learning process. initialize (S,E,T ) update (S,E,T ) stabilize (S,E,T ) quiescence reducibility check is (S,E,T ) precise enough? stop with H − and H + increase preciseness no yes Figure 3: Flow diagram of the learning process. In Figure 3 we give a flow diagram that includes the nondeterministic decision to either stop learning and keep the current hypotheses as final, even tough they do not represent exactly the system under learning, or continue learning, trying to obtain a more precise hypothesis and post- pone the decision of stopping to a later time. The learning process starts with the initialization of the observation table. Then the table is updated, stabilized and checked for quiescence re- ducibility. After these steps, it might be necessary to update and stabilize the table again, and, subsequently, checking again for quiescence reducibility. Only when the table is stable and qui- escence reducible, its preciseness is addressed. If the table is precise enough, then the learning can stop. Otherwise we can try to improve its preciseness. Given the nondeterministic behaviour, it is not always possible to increase the preciseness. A table that is the result of updating another table, after having used a proper technique, should always be more precise than the initial one. In this section we define a qualitative preciseness relation on tables and show that the update does not decrease the preciseness. We introduce some techniques that attempt to increase it, either directly or by triggering an update of a stable table. 5.1 Preciseness of the Table The preciseness of the observation table depends on three factors: 1) the size of the observation table, in term of rows and columns, i. e., the cardinality of (S∪S·Lδ ) and E ; 2) the cardinality of the set of outputs in each entry; and 3) the number of completed entries. If two observation tables are comparable, i. e., they are constructed from the same SUL, and the first has a bigger observation table, bigger sets of output for some entries, and more completed entries than the second, then the first is more precise than the second. Definition 4 Let (S,E,T ) and (S′,E′,T ′) be two observation tables. We say that (S′,E′,T ′) is 11 / 15 Volume 72 (2015) Approximate Active Learning of Nondeterministic IOTSs more precise than (S,E,T ), written as (S,E,T )⊑ (S′,E′,T ′), if and only if: S ⊆ S′ and E ⊆ E′ and ∀s ∈ (S∪S·Lδ ),e ∈ E : { T ′(s·e) =+ T (s·e) if T (s·e) is complete T ′(s·e) ⊇ T (s·e) otherwise If an observation table is more precise than another one, then the relation it describes is stronger than the relation implied by the other observation table (Theorem 4). By increasing the preciseness of the table, we increase the strength of the relation. Theorem 4 (S,E,T ) ⊑ (S′,E′,T ′)⇒ ioco(S,E,T ) ⊇ ioco(S′,E′,T ′) It is easy to verify that Algorithm 1 and Algorithm 2 do not decrease the preciseness of the table, neither does the quiescence reducibility check. Proposition 1 During learning, each table is more (or equally) precise than the previous one. 5.2 Techniques for Increasing the Preciseness Classic L⋆ stops with the exact model of the system under learning: if the current model is not the correct one, there must be a counterexample that will improve the model. In our approach, instead, we are more interested in learning an approximation of the SUL. If the approximation is not good enough we want to make it better. We can achieve this goal by acting on the observation table directly, adding elements to S, E and T (s·e) or by testing our current hypotheses. Extending S and E The first method for increasing the preciseness of the table relies on di- rectly enlarging the table, i. e., increment the number of rows and columns. The cardinality of S and E will therefore grow. Even though this is an easy modification to perform on the observa- tion table, the choice of new elements for those sets is not trivial. It is important to keep S and E prefix and suffix closed, respectively. Thus good candidates for S are elements of S·Lδ , and good candidates for E are elements of Lδ·E . After having added elements to S and E the observation table must be updated and stabilized again. Updating the Table Another method that acts on the table is to run Algorithm 1 with the goal of finding new outputs for existing entries, or making the table not globally closed or consistent. The former case increases the preciseness directly, while the latter will result in an increase of the preciseness due to the stabilizing step. This method is less direct than the previous one, because it might result in not increasing the preciseness at all. Consider a table where all entries are completed: updating the table will have no consequences. Testing the Current Hypotheses The last method we mention is analogue to the classic learn- ing process: once an hypothesis has been constructed, an equivalence oracle confirms that it is equivalent to the system under learning. If not, it provides a counterexample. In practice, this is done by testing. The hypothesis is tested for equivalence against the system under learning. In learning nondeterministic systems, we can use an ioco-based model-based testing tool to test if the SUL is conforming to one of the hypotheses. We can search for a counterexample by Proc. AVoCS 2015 12 / 15 ECEASST testing against H − or H +, using either ioco(S,E,T ) or classic ioco. Testing against H + will find less counterexamples than testing against H −, because SUL ioco(S,E,T ) H +, see Theorem 2. The conformance relation also plays an important role in the conformance query. If ioco(S,E,T ) is used, then the test is concentrated in finding new outputs for the entries in the table, while classic ioco can explore the SUL more widely. A reason for using ioco(S,E,T ) is that it is defined on a finite set of traces, making the testing process exhaustive. By handling a counterexample, either we add an output in one or more already existing entries of the table, or we add some suffixes to E and prefixes to S, increasing the preciseness. 5.3 The Learning Algorithm Combining all the algorithms presented in previous sections results in Algorithm 5. We start by Algorithm 5 LearnLTS 1: S ←{ε} {Initialize (S,E,T )} 2: E ←{ε} 3: loop 4: repeat 5: update(S,E,T ) 6: Stabilize (S,E,T ) using Algorithm 2 7: Check quiescence reduc. on row and row+ ob- taining suffix-closed sets E− and E+ 8: E ← E ∪E−∪E+ 9: until E−∪E+ = /0 10: Construct H − using Algorithm 3 11: Construct H + using Algorithm 4 12: if (S,E,T ) is not precise enough then 13: Try to increase preciseness 14: else 15: return H −,H + initializing the observation table with a set containing only the empty trace ε for both prefixes and suffixes. At this point the table has one column, for the empty trace, and a row for each element of Lδ , plus a column for the empty trace. Then we fill it using Algorithm 1 and Algorithm 2. Quiescence reducibility is checked for both row and row+ and, if that results in adding suffixes to the table, we update and stabilize it again and check again for quiescence reducibility. Once we obtain a stable and quiescence reducible table we consider whether the table is precise. If it is, then we are done: we construct the two hypotheses H − and H + and return them. If the table is not precise, we need to use some techniques to increase its preciseness. Example 4 The first three examples cover Algorithm 5 until the decision point at Line 12. Let’s assume the preciseness is not high enough. We try to improve the preciseness by updating the table, and as a result we discover that T (ε·ε) is complete. The table is not globally closed any more, accordingly to row+: we add a to S and update the table. The table is still not globally closed because of row(aa), thus we add a to S obtaining Figure 4a. The table is globally closed, but not globally consistent. For row we have that row(ε) = row(a) but row(ε a) = row(a) 6= row(aa). We solve the inconsistency by adding a to E . This makes the table not globally closed, because of aδ and aax which are added to S obtaining the table in Figure 4b. This table is globally closed and consistent. It also is quiescence reducible, thus we can construct H − and H +. Figure 4c shows H −, while H + is shown in Figure 5a. Compared with the previous hypotheses, these new ones contain more information. We want to increase the preciseness of the observation table by testing. We test the SUL against H − for ioco(S,E,T ) and we find that, out(SUL after aa) 6= out(H − after aa) because we observed a y during our tests. Assume also 13 / 15 Volume 72 (2015) Approximate Active Learning of Nondeterministic IOTSs ε ε 〈{δ},⊤〉 δ 〈{δ},⊤〉 a 〈{δ},⊥〉 aa 〈{x},⊥〉 δ a 〈{δ},⊥〉 δ δ 〈{δ},⊤〉 aδ 〈{δ},⊤〉 aaa 〈{x},⊥〉 aax 〈{δ},⊥〉 (a) An inconsistent observation table. ε a ε 〈{δ},⊤〉 〈{δ},⊥〉 δ 〈{δ},⊤〉 〈{δ},⊥〉 a 〈{δ},⊥〉 〈{x},⊥〉 aa 〈{x},⊥〉 〈{x},⊥〉 aδ 〈{δ},⊤〉 〈{x},⊥〉 aax 〈{δ},⊥〉 〈{δ},⊥〉 δ a 〈{δ},⊥〉 〈{x},⊥〉 δ δ 〈{δ},⊤〉 〈{δ},⊥〉 aaa 〈{x},⊥〉 〈{x},⊥〉 aδ a 〈{x},⊥〉 〈{x},⊥〉 aδ δ 〈{δ},⊤〉 〈{x},⊥〉 aaxa 〈{δ},⊥〉 〈{x},⊥〉 aaxδ 〈{δ},⊤〉 〈{δ},⊥〉 (b) A stable, more precise, observation table. a δ a δ a x (c) The hypothesis H − for Figure 4b. Figure 4: The top part of the tables represents S and the bottom part represents S·Lδ . a δ a δ δa a x a δ x,y y,δ x,y (a) H + for Figure 4b. ε a ε 〈{δ},⊤〉 〈{δ},⊤〉 δ 〈{δ},⊤〉 〈{δ},⊤〉 a 〈{δ},⊤〉 〈{x,y},⊥〉 aa 〈{x,y},⊥〉 〈{x,y},⊥〉 aδ 〈{δ},⊤〉 〈{x,y},⊥〉 aax 〈{δ},⊥〉 〈{δ},⊤〉 (b) A more precise observation table. a a x δ a,x (c) H + for Figure 5b. Figure 5: The grey state represents chaotic behaviour. that we tested the system enough to obtain TRUE in some entries. A possible observation table could be the one in Figure 5b (S·Lδ is not shown). If we construct H − from Figure 5b, we obtain the SUL, H + is shown in Figure 5c. We consider the table precise enough and we stop. 6 Conclusions We presented an algorithm for learning nondeterministic input-output transition systems by us- ing an active learning L⋆-style approach. The observation table has been modified to handle nondeterminism and unknown behaviour. We defined two different hypotheses, that can be de- rived from the modified observation table, which are able to describe the unknown behaviour in two different ways. We also adapted the properties that the table must satisfy for successfully inferring such hypotheses. The hypotheses are an under and an over-approximation of the SUL according to a newly defined relation ioco(S,E,T ). We uncoupled the membership and equivalence queries, used in classic L⋆, by following a learning process based on preciseness of the obser- vation table: the learning stops, always with an ioco(S,E,T ) conforming model, when the table is considered precise enough, otherwise some actions can be taken to increase its preciseness. Thus, a conformance test, analogue of the equivalence query, is not used directly in the learning process, but only as a mechanism to increase the preciseness. Stopping without reaching an iso- morphism of the system under learning, contrary to L⋆, allows to obtain a valid, conforming, but approximate model which can be used to start (regression) testing. Proc. AVoCS 2015 14 / 15 ECEASST Future Work In this paper we focus on qualitative approximation for the learned model. As future work we want to quantitatively define the preciseness using some measures. A possible measure is given by a combination of the size of S and E , the number of outputs in the table and the number of complete entries, avoiding redundancy (see Algorithm 1). Another measure we are considering is the discounted reachability of χ when H + is considered as a Markov chain. After each modification of the table such measures are calculated and the learning process might end, because a certain value for the preciseness has been reached, or because the preciseness is not changing rapidly any more. Moreover, we wish to investigate which hypothesis, H − or H + is better for regression test- ing, and for other testing and verification techniques where the use of a model is of help. Another topic concerns the techniques used in incremental learning-based testing [MS11] and their adap- tation to active learning of nondeterministic systems. Finally, an experimental evaluation of our approach is necessary to assess its practical feasibility. Bibliography [Ang87] D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation 75(2):87–106, 1987. [BRT04] M. van der Bijl, A. Rensink, J. Tretmans. Compositional Testing with ioco. In Petrenko and Ulrich (eds.), FATES. LNCS 2931, pp. 86–100. Springer, 2004. [Ea10] K. El-Fakih, et al. Learning Finite State Models of Observable Nondeterministic Sys- tems in a Testing Context. In ICTSS. Pp. 97–102. 2010. [MS11] K. Meinke, M. Sindhu. Incremental Learning-Based Testing for Reactive Systems. In Gogolla and Wolff (eds.), TAP. LNCS 6706, pp. 134–151. Springer, 2011. [Nie03] O. Niese. An integrated approach to testing complex systems. PhD thesis, University of Dortmund, 2003. [Pa13] W. Pacharoen, et al. Active Learning of Non-deterministic Finite State Machines. Mathematical Problems in Engineering 2013:11, 2013. [RS93] R. Rivest, R. Schapire. Inference of finite automata using homing sequences. In Han- son et al. (eds.), Machine Learning: From Theory to Applications. LNCS 661, pp. 51– 73. Springer, 1993. [Tre96] J. Tretmans. Test Generation with Inputs, Outputs and Repetitive Quiescence. Software-Concepts and Tools 3:103–120, 1996. [VT14] M. Volpato, J. Tretmans. Active Learning of Nondeterministic Systems from an ioco Perspective. In Margaria and Steffen (eds.), Leveraging Applications of Formal Meth- ods, Verification and Validation. LNCS 8802, pp. 220–235. Springer, 2014. [Wil07] T. Willemse. Heuristics for ioco-Based Test-Based Modelling. In Brim et al. (eds.), Formal Methods: Applications and Technology. LNCS 4346, pp. 132–147. Springer, 2007. 15 / 15 Volume 72 (2015) Introduction Preliminaries Manipulating the Observation Table Nondeterministic Observation Table Filling the Observation Table Global closedness and consistency Construction of Hypotheses Conformance Relation on Observed Behaviour Learning Process Preciseness of the Table Techniques for Increasing the Preciseness The Learning Algorithm Conclusions