... Systems¹¹

To appear in Journal of Systems and Software, Vol. 18, Number 1, April 1992. Jonathan Ostroff is with the Department of Computer Science, York University 4700 Keele Street, North York, Ontario, Canada, M3J 1P3. This work is supported by the Natural Sciences and Engineering Research Council of Canada.

... example²²

The robot example was used in a discussion on real-time issues on Usenet in 1990 with contributors Duncan Thomson and David Stewart

... divided³³

Ron Koymans has pointed out [61] that interval semantics may also be coupled with linear/branching/partial orders — in practice interval semantics have tended to use linear time orders. However, in theory these are orthogonal issues.

... Models⁴⁴

Originally called Extended State Machines.

...activity⁵⁵

An activity variable is also sometimes called a control or location variable. An activity is any particular value that the activity variable may assume. The word ``activity'' is used rather than ``state'' as the word ``state'' is reserved for the global vector of all values of activity and data variables. An activity has persistence as opposed to a transition which occurs instantaneously.

...model-checking⁶⁶

The notion of model-checking was first explored by Clarke and others [20] in the context of (untimed) branching time temporal logics.