A temporal logic for input output symbolic transition systems

In this paper we present a temporal logic called F whose interpretation is over Input Output Symbolic Transition Systems (IOSTS). IOSTS extend transition systems to communications and data in order to tackle communications with system environment. F is then defined as an extension of temporal logic CTL* (a temporal logic which mixes together the features of Linear Temporal Logic (LTL) and Computational Temporal Logic (CTL)). Three basic properties are established on F: adequacy and preservation of properties along synchronized product and IOSTS refinement.