论文部分内容阅读
Mean Value Calculus (MVC)[1] is a real-time logicwhich can be used to specify and verify real-time systems[2]. As aconservative extension of Duration Calculus (DC)[3], MVC increasesthe expressive power but keeps the properties of DC. In this paper wepresent decidability results of MVC. An interesting result is that propositional MVC with chop star operator is still decidable, which develops the results of[4]and[5].