Combining The Temporal And Epistemic Dimensions For Mtl Monitoring
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2017)(2017)
摘要
We define a new notion of satisfaction of a temporal logic formula phi by a behavior w. This notion, denoted by (w, t, t') |= phi, is characterized by two time parameters: the position t from which satisfaction is considered, and the end of the (finite) behavior t' which indicates how much do we know about the behavior. We define this notion in dense time where phi is a formula in the future fragment of metric temporal logic (MTL) and w is a Boolean signal of bounded variability. We show that the set of all pairs (t, t') such that (w, t, t') |= phi can be expressed as a finite union of two-dimensional zones and give an effective procedure to compute it.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络