12th Asia-Pacific Software Engineering Conference (APSEC'05) (2005)
Dec. 15, 2005 to Dec. 17, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.2005.19
Marc Aiguier , LaMI-Universite d?E?vry, France
Pascale Le Gall , LaMI-Universite d?E?vry, France
Delphine Longuet , LaMI-Universite d?E?vry, France
Assia Touil , CEA/LIST Saclay, Yvette France
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.
input output symbolic transition systems, temporal logic, strong bisimulation, refinement, adequacy
D. Longuet, P. Le Gall, A. Touil and M. Aiguier, "A Temporal Logic for Input Output Symbolic Transition Systems," 12th Asia-Pacific Software Engineering Conference (APSEC'05)(APSEC), Taipei, Taiwan, 2005, pp. 43-50.