Specifying and Verifying External Behaviour of Fair Input/Output Automata by Using the Temporal Logic of Actions
Volume 26, Issue 4 (2015), pp. 685–704
Pub. online: 1 January 2015
Type: Research Article
Received
1 August 2013
1 August 2013
Accepted
1 March 2015
1 March 2015
Published
1 January 2015
1 January 2015
Abstract
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.