Real-Time Predicate Detection in Timed Asynchronous Systems

摘要

This research is the first effort providing real-time predicate detection in a timed asynchronous environment. Based on the technique of a lease, we define a new "leased before" relation on local states, which permits a set of Currently Consistent Global States (CCGSs) that are consistent with a computation and are detectable while they continue to hold. Predicate detection on CCGSs brings about a new modality, Cur ("Currently"), that characterizes the semantics that real-time evaluation of a predicate on CCGSs is possible in a timed asynchronous system. We also describe the conditions under which predicates are detectable under the timed asynchronous model.