A Model Language for Describing Spatio-temporal Changes

摘要

In specifications of Train Control System, the spatio-temporal requirement for trains executing actions is an important part. To model spatio-temporal changes about trains, we present a model language from another perspective in this paper. We adopt a function over a location set to define an action. In such a way, we can describe agent's spatial changes in executing action and can compute agent's location at any time. Firstly, we give syntaxes about a spatio-temporal language and its operational semantics. Then, we do a case study in Train Control System by using the model language. Finally, we present a concept of computation tree. Based on computation tree, we get some properties about the operational semantics of the model.