Semantic Models for a Language with Timed Atomic Actions

摘要

An operational and a denotational semantic model for a language incorporating time related aspects, viz. timed atomic actions and integration, is presented. With timed atomic actions one means atomic actions each provided with a time stamp, which records the time at which the atomic action should be executed. Integration of a statement over some non-empty subset of the time domain gives rise to the execution of the statement with some non-deterministically chosen value of the subset passed to that statement. Both models are built on complete metric spaces. An equivalence result of the operational and the denotational semantic model concludes the paper.