The Community for Technology Leaders
12th Asia-Pacific Software Engineering Conference (APSEC'05) (2005)
Taipei, Taiwan
Dec. 15, 2005 to Dec. 17, 2005
ISSN: 1530-1362
ISBN: 0-7695-2465-6
pp: 43-50
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
ABSTRACT
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.
INDEX TERMS
input output symbolic transition systems, temporal logic, strong bisimulation, refinement, adequacy
CITATION

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.
doi:10.1109/APSEC.2005.19
97 ms
(Ver 3.3 (11022016))