A temporal logic for input output symbolic transition systems

In this paper, we present a temporal logic called ℱ 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. ℱ 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 ℱ: adequacy and preservation of properties along synchronized product and IOSTS refinement.