Specifying and Verifying External Behaviour of Fair Input/Output Automata by Using the Temporal Logic of Actions

Article type: Research Article

Authors: Kapus, Tatjana

Affiliations: University of Maribor, Faculty of Electrical Engineering and Computer Science, Smetanova ul. 17, SI-2000 Maribor, Slovenia, e-mail: [email protected]

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.

Keywords: formal specification, fair input/output automaton, temporal logic of actions, fair trace, fair trace inclusion

Journal: Informatica, vol. 26, no. 4, pp. 685-704, 2015