<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Using model checking to identify customers' purchasing behaviour in an e-commerce</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Sergio Hern´andez</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Pedro A´lvarez</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Javier Fabra</string-name>
          <email>jfabra@unizar.es</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Joaqu´ın Ezpeleta</string-name>
          <email>ezpeleta@unizar.es</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Department of Computer Science and Systems Engineering, Arago ́n Institute of Engineering Research (I3A), University of Zaragoza</institution>
          ,
          <country country="ES">Spain</country>
        </aff>
      </contrib-group>
      <fpage>158</fpage>
      <lpage>164</lpage>
      <abstract>
        <p>Understanding customers' behaviour is essential to adapt ecommerce websites to their preferences and requirements. Process mining techniques can be used to analyse e-commerce web logs with such purpose. However, procedural techniques are not suitable to analyse logs from open systems and current declarative ones focus on extracting the most frequent behavioural constraints. In this paper the use of a declarative approach based on Linear Temporal Logic and model checking is explored for the analysis of a real e-commerce website. This approach explores complex queries adapted to the problem domain. Results show that analysing both common and uncommon behavioural patterns provides valuable insights that can be used to adapt the website and to improve marketing and advertising campaigns.</p>
      </abstract>
      <kwd-group>
        <kwd>Linear temporal logic</kwd>
        <kwd>model checking</kwd>
        <kwd>declarative process mining</kwd>
        <kwd>complex behavioural patterns</kwd>
        <kwd>purchasing process</kwd>
      </kwd-group>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>
        The appearance of e-commerce websites has revolutionized the shopping context
allowing people to purchase products from anywhere at any time. Understanding
users’ requirements, necessities and preferences is key to survive the competition
and succeed [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ]. Nevertheless, it is a complex task [
        <xref ref-type="bibr" rid="ref2">2</xref>
        ].
      </p>
      <p>
        Users’ behaviour when using an e-commerce website is recorded in the web
server logs which store the sequence of requests performed by users. Analysing
this type of logs to extract and identify behaviour has been the goal of both data
and process mining communities. On the one hand, data mining approaches are
focused on extracting behaviour by applying clustering, sequence pattern
mining and rule association techniques [
        <xref ref-type="bibr" rid="ref3 ref4 ref5 ref6">3,4,5,6</xref>
        ]. However, these techniques do not
consider the order of activities recorded in the log and, as a consequence, they
lose information about which events influence the occurrence of other events,
for instance. On the other hand, the process mining community mainly focus
on discovering a procedural model from the log [
        <xref ref-type="bibr" rid="ref7">7</xref>
        ]. However, in the e-commerce
domain this approach is not very suitable [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ]. An e-commerce website is an open
system where any behaviour is possible and a meaningful process model cannot
be identified since the application of procedural techniques usually provides a
flower model or a spaghetti one from where no useful information can be
extracted [
        <xref ref-type="bibr" rid="ref7">7</xref>
        ]. In this context, declarative approaches are more suitable since they
allow to look for specific behavioural constraints [
        <xref ref-type="bibr" rid="ref8 ref9">8,9</xref>
        ].
      </p>
      <p>
        In this paper we propose the use of Linear Temporal Logic (LTL) [
        <xref ref-type="bibr" rid="ref10">10</xref>
        ] and
model checking [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ] techniques to explore complex behavioural patterns in open
systems as the case of the e-commerce domain. The approach is then illustrated
by its application to the analysis of the Up&amp;Scrap e-commerce website1. The
goal is to analyse multi-perspective behavioural patterns related with the buying
process defining and checking LTL formulas that describe such behaviour against
the log model. By applying this kind of analysis, we are interested in finding
causal dependencies among events and the fact of purchasing goods, that is,
behavioural patterns whose occurrence increase the probability of purchase. The
obtained information can be used to improve the website design and contents,
to adapt and personalize contents or to recommend products with the ultimate
goal of increasing sales.
      </p>
      <p>
        The use of temporal logics to analyse event logs using a declarative
approach has been previously explored [
        <xref ref-type="bibr" rid="ref12 ref13 ref14 ref15 ref16 ref17 ref8 ref9">12,8,13,14,15,16,9,17</xref>
        ]. Nevertheless, these
approaches struggle with multi-perspective analysis that is and/or the use of
ad-hoc complex queries. Most approaches do not consider the possibility or
including data attributes to enable multi-perspective analysis [
        <xref ref-type="bibr" rid="ref13 ref14 ref15 ref16 ref8">8,13,14,15,16</xref>
        ], or
they only allow specific perspectives [
        <xref ref-type="bibr" rid="ref12">12</xref>
        ]. This limits the effectiveness in the
approach when the log contains many data attributes and their importance is key
for the analysis as in the e-commerce domain where identifying and
differentiating web sections is fundamental. Furthermore, many techniques are based on
the use of the Declare language [
        <xref ref-type="bibr" rid="ref8">8</xref>
        ] and, as a consequence, they can only explore
a reduced set of predefined patterns [
        <xref ref-type="bibr" rid="ref13 ref14 ref15 ref17 ref8 ref9">8,13,14,15,9,17</xref>
        ] which can be hardly
extended [
        <xref ref-type="bibr" rid="ref17 ref9">9,17</xref>
        ]. This issue reduces the type of behavioural patterns and constraints
that can be discovered or analysed causing that interesting behaviours remain
unexplored although they could provide valuable information.
      </p>
      <p>Compared with the above mentioned approaches, our proposal is more
general since it enables multi-perspective analysis without limitations on the
perspectives that can be used, it allows the use of any kind of LTL formula and it is
able to handle large event logs as the one explored in this paper. Finally, it must
be mentioned that the approach proposed in this paper focuses on supervised
and semi-supervised mining while previous approaches have mainly focused in
unsupervised one. Although supervised techniques require a business expert to
define the behavioural patterns that must be explored, they have the advantage
that uncommon but valuable patterns, as the ones related with the
purchasing process, can be identified. In this regard, unsupervised techniques are less
suitable since they focus on extracting the most frequent patterns.
1 http://www.upandscrap.com</p>
      <p>Model checking-based analysis of the Up&amp;Scrap logs
In this work we have applied the LTL-based model checking approach to the web
logs of the Up&amp;Scrap website. Up&amp;Scrap is the leader company in Spain for the
sale of equipment for scrapbooking. The company website is structured in a set of
main sections which organize the products in eight categories (paper, decorate,
stamp, tools, project life-smash, albums, home decor-diy and gifts) according
to the product categorization that includes two levels of depth. There are also
secondary sections which provide an alternative way of accessing products by
brands, collections, thematics, designers, offers and new products. Additionally,
a search engine is provided to look for products within the website.</p>
      <p>We have analysed the web logs of two months which include 8, 607, 625 HTTP
requests. Initially, this information must be preprocessed to remove automatic,
erroneous and irrelevant requests and to group requests belonging to the same
session (sessionization). Next, each request must be analysed to identify
interesting events for the analysis that is going to be carried out. Since our aim
is to analyse the customers’ purchasing behaviour, we have identified the
following 12 types of events: Visit homepage, Visit product, Visit main section L1,
Visit main section L2, Visit secondary section L1, Visit secondary section L2,
Buy products, Delete product from the cart, Add wishlist products to the cart,
Add product to the wishlist, Add product to the cart, Update product from cart.
Also, the category and subcategory being accessed are obtained and included in
the final log along with the URL accessed, the operation code (GET or POST),
the status code and the timestamp. After the preprocessing, the final log used for
the analysis contains 1, 331, 697 events corresponding to 144, 330 user sessions.</p>
      <p>
        To enable the LTL-based model checking analysis, the set of traces (user
sessions) in the log is considered as the model representing the process and each
event is represented as the conjunction of atomic propositions corresponding
to the event activity and its attributes. Figure 1 shows a simplified example of
trace in the previous format showing the event activity and part of the attributes
defining the different perspectives that can be used in the analysis. Therefore,
LTL formulas can be used to analyse the trace behaviour using the model checker
tool presented in [
        <xref ref-type="bibr" rid="ref18">18</xref>
        ] that is based on the use of the Spot libraries [
        <xref ref-type="bibr" rid="ref19">19</xref>
        ]. To
exemplify the kind of behavioural patterns that can be discovered by using this
technique, we are going to focus on the buying process.
3
      </p>
      <p>
        Analysis of Up&amp;Scrap customers’ purchasing behaviour
To enable the analysis, we have defined a set of variables and macros in the
model checker tool described in [
        <xref ref-type="bibr" rid="ref18">18</xref>
        ]. Their use improves the queries readability
and allows the execution of a query on multiple values such as all the sections
of the web page, for instance. The defined variables and macros are:
– Variable ?visit main includes the events referred to visit a main section.
      </p>
      <p>Values: Visit main section L1 and Visit main section L2.</p>
      <p>– Variable ?visit secondary includes the events referred to visit a secondary
section. Values: Visit secondary section L1 and Visit secondary section L2.
– Variable ?visit includes events in ?visit main and ?visit secondary.
– Variable ?main cat includes all the possible values of main categories. Values:
papers, decorate, stamp, tools, project life-smash, home decor-diy and gifts.
– Variable ?sec cat includes all the possible values of secondary categories.</p>
      <p>Values: offers, new products, collections, thematics, designers, brands and
search results.
– Macros ?OR VISIT MAIN, ?OR VISIT SEC, ?OR VISIT correspond to a
logical OR of “?visit main”, “?visit secondary” and “?visit”, respectively.</p>
      <p>In the buying process there are two essential actions: adding products to the
cart and buying the products in the cart. Our goal is to analyse specific sections
that lead to the appearance of these two actions. In the Up&amp;Scrap website,
products can be reached both from main and secondary sections. Furthermore,
products can be added to the cart from the own product page, which has no
information about the section from where the product has been accessed, and
from the product listings in the sections. Therefore, identifying web sections
that lead to purchases is not immediate since the query must consider both
possibilities. With such purpose we have executed two types of queries2:
1. Which are the main sections from where products are added to the cart?
♦(?OR VISIT MAIN ∧ ?main cat) ∧ l((¬ ?OR VISIT) ∪
(Add product to the cart)))
2. Which are the main sections from where products are added to the cart in
sessions that buy some product?
♦(?OR VISIT MAIN ∧ ?main cat) ∧ l((¬ ?OR VISIT) ∪
(Add product to the cart)) ∧ l♦ Buy products)
3. Which are the secondary sections from where products are added to the cart?
♦(?OR VISIT SEC ∧ ?sec cat) ∧ l((¬ ?OR VISIT) ∪
(Add product to the cart)))
2 In the literature, X, G, F are used as alternative symbols for l, , ♦, respectively.
4. Which are the secondary sections from where products are added to the cart
in sessions that buy some product?
♦(?OR VISIT SEC ∧ ?sec cat) ∧ l((¬ ?OR VISIT) ∪
(Add product to the cart)) ∧ l♦ Buy products)</p>
      <p>Note the use of variables and macros allows to write more compact
formulas. Nevertheless, macros must be substituted with their appropriate values
and variables must be evaluated for each possible value. For example, one of
the specific formulas evaluated in the last case for the offers secondary
sections is: ♦((Visit secondary section L1 ∨ Visit secondary section L2) ∧ offers) ∧
l((¬(Visit main section L1 ∨ Visit main section L2 ∨ Visit secondary section L1 ∨
Visit secondary section L2)) ∪ (Add product to the cart)) ∧ l♦ Buy products)</p>
      <p>
        Table 1 summarizes the results. For the first query type (queries 1 and 3) we
define the so-called interest-rate as the ratio between the number of accesses to the
section that leads to adding a product to the cart and the total number of accesses
to the section. For the second query type (queries 2 and 4) we introduce the so-called
purchase-interest rate as the percentage of sessions that add products to the cart and
purchase them compared to the total number of sessions that add products to the cart.
These metrics are inspired in known concepts, as support or confidence, commonly
used in other declarative approaches [
        <xref ref-type="bibr" rid="ref8 ref9">8,9</xref>
        ].
      </p>
      <p>There are four main sections that are leading to the addition of products to the cart
according to their interest rate: stamp, papers, decorate and tools. Regarding secondary
sections, a remarkable finding is that the designers section has one of the highest
interest rate. This is explained by users that show fidelity to specific designers and look
for their products. Another relevant discovery is that offers and new products sections
are not showing high interest rates. Regarding the purchase-interest rate, surprisingly,
the gifts section has the lowest interest rate but the highest purchase-interest one.
The remaining main sections show a similar percentage and there are not a
significant differences between sections. On the contrary, the search engine has the highest
purchase-interest rate among secondary ones. This indicates that when people finds
an interesting product through the search engine it is more likely to buy it. It is also
remarkable that new products and offers sections present a rate much lower than other
web sections. This issue points towards the lack of effectiveness of these sections and
the need of improving its importance within the website.
4</p>
    </sec>
    <sec id="sec-2">
      <title>Conclusions and future work</title>
      <p>The analysis of event logs of open systems, as the ones recorded in the web server
logs of e-commerce websites, requires the use of flexible declarative approaches able
to identify valuable behavioural patterns. Current approaches present limitations in
the use of data attributes and complex user-defined patterns. In this paper we have
proposed a LTL-based model checking approach that is able of effectively analyse this
type of logs by exploring complex domain-related behavioural patterns that include
data attributes and allow multi-perspective analysis. Analysis results provide insights
on most and less effective sections regarding the buying process that have been used
to improve the Up&amp;Scrap website design.</p>
      <p>As future work, we intend to develop a methodology for the analysis of any
ecommerce website using this approach and to apply the technique in other application
domains.</p>
    </sec>
    <sec id="sec-3">
      <title>Acknowledgements</title>
      <p>This work has been supported by the TIN2014-56633-C3-2-R research project, granted
by the Spanish Ministerio de Econom´ıa y Competitividad and teh
UZCUD-2016-TEC06 research project granted by the University of Zaragoza. The authors of this paper
want to specially thank the Up&amp;Scrap team for their collaboration, for providing the
data used in this study and for giving feedback on the results.</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <given-names>N.</given-names>
            <surname>Poggi</surname>
          </string-name>
          ,
          <string-name>
            <given-names>V.</given-names>
            <surname>Muthusamy</surname>
          </string-name>
          ,
          <string-name>
            <given-names>D.</given-names>
            <surname>Carrera</surname>
          </string-name>
          ,
          <string-name>
            <given-names>R.</given-names>
            <surname>Khalaf</surname>
          </string-name>
          ,
          <article-title>Business process mining from e-commerce web logs</article-title>
          ,
          <source>in: Proceedings of the 11th International Conference on Business Process Management, BPM'13</source>
          , Springer-Verlag, Berlin, Heidelberg,
          <year>2013</year>
          , pp.
          <fpage>65</fpage>
          -
          <lpage>80</lpage>
          . doi:
          <volume>10</volume>
          .1007/978-3-
          <fpage>642</fpage>
          -40176-
          <issue>3</issue>
          _
          <fpage>7</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <given-names>R.</given-names>
            <surname>Kohavi</surname>
          </string-name>
          ,
          <article-title>Mining e-commerce data: the good, the bad, and the ugly, in: Proceedings of the seventh ACM SIGKDD international conference on Knowledge discovery and data mining</article-title>
          ,
          <source>ACM</source>
          ,
          <year>2001</year>
          , pp.
          <fpage>8</fpage>
          -
          <lpage>13</lpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <given-names>Q.</given-names>
            <surname>Zhang</surname>
          </string-name>
          , R. S. Segall,
          <article-title>Web mining: a survey of current research, techniques, and software</article-title>
          ,
          <source>International Journal of Information Technology &amp; Decision Making</source>
          <volume>7</volume>
          (
          <issue>04</issue>
          ) (
          <year>2008</year>
          )
          <fpage>683</fpage>
          -
          <lpage>720</lpage>
          . doi:
          <volume>10</volume>
          .1142/S0219622008003150.
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <given-names>Q.</given-names>
            <surname>Su</surname>
          </string-name>
          ,
          <string-name>
            <given-names>L.</given-names>
            <surname>Chen</surname>
          </string-name>
          ,
          <article-title>A method for discovering clusters of e-commerce interest patterns using click-stream data</article-title>
          ,
          <source>Electronic Commerce Research and Applications</source>
          <volume>14</volume>
          (
          <issue>1</issue>
          ) (
          <year>2015</year>
          )
          <fpage>1</fpage>
          -
          <lpage>13</lpage>
          . doi:
          <volume>10</volume>
          .1016/j.elerap.
          <year>2014</year>
          .
          <volume>10</volume>
          .002.
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <given-names>S.</given-names>
            <surname>Kim</surname>
          </string-name>
          ,
          <string-name>
            <given-names>J.</given-names>
            <surname>Yeo</surname>
          </string-name>
          , E. Koh,
          <string-name>
            <given-names>N.</given-names>
            <surname>Lipka</surname>
          </string-name>
          ,
          <article-title>Purchase influence mining: Identifying top-k items attracting purchase of target item</article-title>
          ,
          <source>in: Proceedings of the 25th International Conference Companion on World Wide Web, International World Wide Web Conferences Steering Committee</source>
          ,
          <year>2016</year>
          , pp.
          <fpage>57</fpage>
          -
          <lpage>58</lpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <given-names>J. D.</given-names>
            <surname>Xu</surname>
          </string-name>
          ,
          <article-title>Retaining customers by utilizing technology-facilitated chat: Mitigating website anxiety and task complexity</article-title>
          ,
          <source>Information &amp; Management</source>
          <volume>53</volume>
          (
          <issue>5</issue>
          ) (
          <year>2016</year>
          )
          <fpage>554</fpage>
          -
          <lpage>569</lpage>
          . doi:
          <volume>10</volume>
          .1016/j.im.
          <year>2015</year>
          .
          <volume>12</volume>
          .007.
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <surname>W. M. P. van der Aalst</surname>
          </string-name>
          ,
          <source>Process Mining: Discovery, Conformance and Enhancement of Business Processes, 1st Edition</source>
          , Springer Publishing Company, Incorporated,
          <year>2011</year>
          . doi:
          <volume>10</volume>
          .1007/978-3-
          <fpage>642</fpage>
          -19345-3.
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <surname>W. M. van Der Aalst</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          <string-name>
            <surname>Pesic</surname>
            ,
            <given-names>H.</given-names>
          </string-name>
          <string-name>
            <surname>Schonenberg</surname>
          </string-name>
          ,
          <article-title>Declarative workflows: Balancing between flexibility and support</article-title>
          ,
          <source>Computer Science-Research and Development</source>
          <volume>23</volume>
          (
          <issue>2</issue>
          ) (
          <year>2009</year>
          )
          <fpage>99</fpage>
          -
          <lpage>113</lpage>
          . doi:
          <volume>10</volume>
          .1007/s00450-009-0057-9.
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9.
          <string-name>
            <given-names>A.</given-names>
            <surname>Burattin</surname>
          </string-name>
          ,
          <string-name>
            <given-names>F. M.</given-names>
            <surname>Maggi</surname>
          </string-name>
          ,
          <string-name>
            <given-names>A.</given-names>
            <surname>Sperduti</surname>
          </string-name>
          ,
          <article-title>Conformance checking based on multiperspective declarative process models</article-title>
          ,
          <source>Expert Systems with Applications</source>
          <volume>65</volume>
          (
          <year>2016</year>
          )
          <fpage>194</fpage>
          -
          <lpage>211</lpage>
          . doi:
          <volume>10</volume>
          .1016/j.eswa.
          <year>2016</year>
          .
          <volume>08</volume>
          .040.
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <given-names>A.</given-names>
            <surname>Pnueli</surname>
          </string-name>
          ,
          <string-name>
            <given-names>Z.</given-names>
            <surname>Manna</surname>
          </string-name>
          ,
          <article-title>The temporal logic of reactive and concurrent systems (</article-title>
          <year>1992</year>
          ). doi:
          <volume>10</volume>
          .1007/978-1-
          <fpage>4612</fpage>
          -0931-7.
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11. E.
          <string-name>
            <surname>Clarke</surname>
            ,
            <given-names>O.</given-names>
          </string-name>
          <string-name>
            <surname>Grumberg</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          <string-name>
            <surname>Long</surname>
          </string-name>
          ,
          <article-title>Verification tools for finite-state concurrent systems</article-title>
          , in: Workshop/School/Symposium of the REX
          <source>Project (Research and Education in Concurrent Systems)</source>
          , Springer,
          <year>1993</year>
          , pp.
          <fpage>124</fpage>
          -
          <lpage>175</lpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <surname>W. M. van der Aalst</surname>
            , H. De Beer,
            <given-names>B. F. van Dongen</given-names>
          </string-name>
          ,
          <article-title>Process mining and verification of properties: An approach based on temporal logic, in: OTM Confederated International Conferences” On the Move to Meaningful Internet Systems”</article-title>
          , Springer,
          <year>2005</year>
          , pp.
          <fpage>130</fpage>
          -
          <lpage>147</lpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.
          <string-name>
            <surname>F. M. Maggi</surname>
            ,
            <given-names>R. P. J. C.</given-names>
          </string-name>
          <string-name>
            <surname>Bose</surname>
            ,
            <given-names>W. M. P. van der Aalst</given-names>
          </string-name>
          ,
          <source>Efficient Discovery of Understandable Declarative Process Models from Event Logs</source>
          , Springer Berlin Heidelberg, Berlin, Heidelberg,
          <year>2012</year>
          , pp.
          <fpage>270</fpage>
          -
          <lpage>285</lpage>
          . doi:
          <volume>10</volume>
          .1007/978-3-
          <fpage>642</fpage>
          -31095-9_
          <fpage>18</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          14.
          <string-name>
            <surname>C. D. Ciccio</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          <string-name>
            <surname>Mecella</surname>
          </string-name>
          ,
          <article-title>A two-step fast algorithm for the automated discovery of declarative workflows</article-title>
          ,
          <source>in: 2013 IEEE Symposium on Computational Intelligence and Data Mining (CIDM)</source>
          ,
          <year>2013</year>
          , pp.
          <fpage>135</fpage>
          -
          <lpage>142</lpage>
          . doi:
          <volume>10</volume>
          .1109/CIDM.
          <year>2013</year>
          .
          <volume>6597228</volume>
          .
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          15.
          <string-name>
            <surname>M. Westergaard</surname>
            ,
            <given-names>C.</given-names>
          </string-name>
          <string-name>
            <surname>Stahl</surname>
            ,
            <given-names>H. A.</given-names>
          </string-name>
          <string-name>
            <surname>Reijers</surname>
          </string-name>
          ,
          <article-title>UnconstrainedMiner: efficient discovery of generalized declarative process models</article-title>
          ,
          <source>BPM Center Report BPM-13-28</source>
          , BPMcenter. org (
          <year>2013</year>
          )
          <fpage>28</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          16. M. Ra¨im, C. Di
          <string-name>
            <surname>Ciccio</surname>
            ,
            <given-names>F. M.</given-names>
          </string-name>
          <string-name>
            <surname>Maggi</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          <string-name>
            <surname>Mecella</surname>
            ,
            <given-names>J.</given-names>
          </string-name>
          <string-name>
            <surname>Mendling</surname>
          </string-name>
          ,
          <article-title>Log-based understanding of business processes through temporal logic query checking</article-title>
          ,
          <source>in: On the Move to Meaningful Internet Systems: OTM 2014 Conferences: Confederated International Conferences: CoopIS, and ODBASE</source>
          <year>2014</year>
          , Proceedings, Springer Berlin Heidelberg,
          <year>2014</year>
          , pp.
          <fpage>75</fpage>
          -
          <lpage>92</lpage>
          . doi:
          <volume>10</volume>
          .1007/978-3-
          <fpage>662</fpage>
          -45563-
          <issue>0</issue>
          _
          <fpage>5</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          17. S. Scho¨nig, C. Di
          <string-name>
            <surname>Ciccio</surname>
            ,
            <given-names>F. M.</given-names>
          </string-name>
          <string-name>
            <surname>Maggi</surname>
            ,
            <given-names>J.</given-names>
          </string-name>
          <string-name>
            <surname>Mendling</surname>
          </string-name>
          ,
          <source>Discovery of Multi-perspective Declarative Process Models</source>
          , Springer International Publishing, Cham,
          <year>2016</year>
          , pp.
          <fpage>87</fpage>
          -
          <lpage>103</lpage>
          . doi:
          <volume>10</volume>
          .1007/978-3-
          <fpage>319</fpage>
          -46295-
          <issue>0</issue>
          _
          <fpage>6</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          18. P. A´lvarez, J. Fabra, S. Herna´ndez, J. Ezpeleta,
          <article-title>Alignment of teacher's plan and students' use of lms resources. analysis of moodle logs</article-title>
          ,
          <source>in: 2016 15th International Conference on Information Technology Based Higher Education and Training (ITHET)</source>
          ,
          <year>2016</year>
          , pp.
          <fpage>1</fpage>
          -
          <lpage>8</lpage>
          . doi:
          <volume>10</volume>
          .1109/ITHET.
          <year>2016</year>
          .
          <volume>7760720</volume>
          .
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          19. A.
          <string-name>
            <surname>Duret-Lutz</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          <string-name>
            <surname>Poitrenaud</surname>
          </string-name>
          ,
          <article-title>Spot: an extensible model checking library using transition-based generalized b uuml;chi automata</article-title>
          ,
          <source>in: Modeling, Analysis, and Simulation of Computer and Telecommunications Systems</source>
          ,
          <year>2004</year>
          . (
          <article-title>MASCOTS 2004)</article-title>
          .
          <source>Proceedings. The IEEE Computer Society's 12th Annual International Symposium on, 2004</source>
          , pp.
          <fpage>76</fpage>
          -
          <lpage>83</lpage>
          . doi:
          <volume>10</volume>
          .1109/MASCOT.
          <year>2004</year>
          .
          <volume>1348184</volume>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>