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.

• Type: Conference
• Year: 2005
• Where: APSEC
• Authors: Marc Aiguier, Pascale Le Gall, Delphine Longuet, Assia Touil
• Keywords: APSEC 2005, Computational Temporal Logic, Software Engineering, Temporal Logic, Temporal Logic Ctl∗