<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-012-05-0482</article-id>
      <article-id pub-id-type="publisher-id">28613</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>D.2.4 - Software/Program Verification</subject>
          <subject>F.1.1 - Models of Computation</subject>
          <subject>F.4.1 - Mathematical Logic</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>On-line Monitoring of Metric Temporal Logic with Time-Series Constraints Using Alternating Finite Automata</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Drusinsky</surname>
            <given-names>Doron</given-names>
          </name>
          <email xlink:type="simple">ddrusins@nps.edu</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Naval Postgraduate School, Monterey, United States of America</addr-line>
        <institution>Naval Postgraduate School</institution>
        <addr-line content-type="city">Monterey</addr-line>
        <country>United States of America</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Doron Drusinsky (<email xlink:type="simple">ddrusins@nps.edu</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2006</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>05</month>
        <year>2006</year>
      </pub-date>
      <volume>12</volume>
      <issue>5</issue>
      <fpage>482</fpage>
      <lpage>498</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/E66FD3F0-E9C7-5A8C-89AF-97E8B3141CAF">E66FD3F0-E9C7-5A8C-89AF-97E8B3141CAF</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6997018">6997018</uri>
      <permissions>
        <copyright-statement>Doron Drusinsky</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>In this paper we describe a technique for monitoring and checking temporal logic assertions augmented with real-time and time-series constraints, or Metric Temporal Logic Series (MTLS). The method is based on Remote Execution and Monitoring (REM) of temporal logic assertions. We describe the syntax and semantics of MTLS and a monitoring technique based on alternating finite automata that is efficient for a large set of frequently used formulae and is also an on-line technique. We investigate the run-time data-structure size for several interesting assertions taken from the Kansas State specification patterns.</p>
      </abstract>
    </article-meta>
  </front>
</article>
