<?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-007-11-0980</article-id>
      <article-id pub-id-type="publisher-id">27833</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.3.1 - Specifying and Verifying and Reasoning about Programs</subject>
          <subject>F.4.1 - Mathematical Logic</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>A Logic for Abstract State Machines</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Stärk</surname>
            <given-names>Robert F.</given-names>
          </name>
          <email xlink:type="simple">staerk@inf.ethz.ch</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Nanchen</surname>
            <given-names>Stanislas</given-names>
          </name>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Computer Science Department, ETH Zürich, Zuerich, Switzerland</addr-line>
        <institution>Computer Science Department, ETH Zürich</institution>
        <addr-line content-type="city">Zuerich</addr-line>
        <country>Switzerland</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Robert F. Stärk (<email xlink:type="simple">staerk@inf.ethz.ch</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2001</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>11</month>
        <year>2001</year>
      </pub-date>
      <volume>7</volume>
      <issue>11</issue>
      <fpage>980</fpage>
      <lpage>1005</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/6EE0A33F-1D28-560E-9178-5765CF3F28D7">6EE0A33F-1D28-560E-9178-5765CF3F28D7</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6996073">6996073</uri>
      <permissions>
        <copyright-statement>Robert F. Stärk, Stanislas Nanchen</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>We introduce a logic for non distributed, deterministic Abstract State Machines with parallel function updates. Unlike other logics for ASMs which are based on dynamic logic, our logic is based on an atomic predicate for function updates and on a definedness predicate for the termination of the evaluation of transition rules. We do not assume that the transition rules of ASMs are in normal form, for example, that they concern distinct cases. Instead we allow structuring concepts of ASM rules including sequential composition and possibly recursive submachine calls. We show that several axioms that have been proposed for reasoning about ASMs are derivable in our system. We provide also an extension of the logic with explicit step information which allows to eliminate modal operators in certain cases. The main technical result is that the logic is complete for hierarchical (non-recursive) ASMs. We show that, for hierarchical ASMs, the logic is a definitional extension of first-order predicate logic.</p>
      </abstract>
    </article-meta>
  </front>
</article>
