<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.0 20120330//EN" "JATS-journalpublishing1.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" article-type="research-article">
<front>
<journal-meta>
<journal-id journal-id-type="publisher-id">INFORMATICA</journal-id>
<journal-title-group><journal-title>Informatica</journal-title></journal-title-group>
<issn pub-type="epub">0868-4952</issn><issn pub-type="ppub">0868-4952</issn>
<publisher>
<publisher-name>VU</publisher-name>
</publisher>
</journal-meta>
<article-meta>
<article-id pub-id-type="publisher-id">INFO1074</article-id><article-id pub-id-type="doi">10.15388/Informatica.2015.71</article-id>
<article-categories><subj-group subj-group-type="heading">
<subject>Research Article</subject></subj-group></article-categories>
<title-group>
<article-title>Specifying and Verifying External Behaviour of Fair Input/Output Automata by Using the Temporal Logic of Actions</article-title>
</title-group>
<contrib-group>
<contrib contrib-type="Author">
<name><surname>Kapus</surname><given-names>Tatjana</given-names></name><email xlink:href="mailto:tatjana.kapus@um.si">tatjana.kapus@um.si</email><xref ref-type="aff" rid="j_INFORMATICA_aff_000"/>
</contrib>
<aff id="j_INFORMATICA_aff_000">University of Maribor, Faculty of Electrical Engineering and Computer Science, Smetanova ul. 17, SI-2000 Maribor, Slovenia</aff>
</contrib-group>
<pub-date pub-type="epub"><day>01</day><month>01</month><year>2015</year></pub-date><volume>26</volume><issue>4</issue><fpage>685</fpage><lpage>704</lpage><history><date date-type="received"><day>01</day><month>08</month> <year>2013</year></date><date date-type="accepted"><day>01</day><month>03</month> <year>2015</year></date></history>
<permissions><copyright-statement>Vilnius University</copyright-statement><copyright-year>2015</copyright-year></permissions>
<abstract>
<p>Fair input/output (or I/O) automata are a state-machine model for specifying and verifying reactive and concurrent systems. For the verification purposes, one is usually interested only in the sequences of interactions fair I/O automata offer to their environment. These sequences are called fair traces. The usual approach to the verification consists in proving fair trace inclusion between fair I/O automata. This paper presents a simple approach to the specification of fair traces and shows how to establish a fair trace inclusion relation for a pair of fair I/O automata by using the temporal logic of actions.</p>
</abstract>
<kwd-group>
<label>Keywords</label>
<kwd>formal specification</kwd>
<kwd>fair input/output automaton</kwd>
<kwd>temporal logic of actions</kwd>
<kwd>fair trace</kwd>
<kwd>fair trace inclusion</kwd>
</kwd-group>
</article-meta>
</front>
</article>
