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.