<?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-006-11-1054</article-id>
      <article-id pub-id-type="publisher-id">27728</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.1 - Requirements/Specifications</subject>
          <subject>D.2.4 - Software/Program Verification</subject>
          <subject>F.3.1 - Specifying and Verifying and Reasoning about Programs</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Nondeterministic Admissible Interference</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Mullins</surname>
            <given-names>John</given-names>
          </name>
          <email xlink:type="simple">john.mullins@polymtl.ca</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Ecole Polytechnique de Montreal, Montreal, Canada</addr-line>
        <institution>Ecole Polytechnique de Montreal</institution>
        <addr-line content-type="city">Montreal</addr-line>
        <country>Canada</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: John Mullins (<email xlink:type="simple">john.mullins@polymtl.ca</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2000</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>11</month>
        <year>2000</year>
      </pub-date>
      <volume>6</volume>
      <issue>11</issue>
      <fpage>1054</fpage>
      <lpage>1070</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/2DE48099-0097-52A8-8755-B3156ED7C95B">2DE48099-0097-52A8-8755-B3156ED7C95B</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6995901">6995901</uri>
      <permissions>
        <copyright-statement>John Mullins</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 article we address the issue of confidentiality of information in the context of downgrading systems i.e. systems admitting information flow between secrecy levels only through a downgrader. Inspired by the intuition underlying the usual definition of admissible information flow, we propose an analogue based on trace equivalence as developed in the context of concurrency theory and on a modification of the usual definition of purge function. We also provide unwinding conditions to guarantee a consistent and complete proof method in terms of communicating transition systems. We take advantage of this framework to investigate its compositionality issues w.r.t. the main operators over communicating transition systems. We conclude the article with a short presentation of this work s most promising aspects in the perspective of future developments.</p>
      </abstract>
    </article-meta>
  </front>
</article>
