[Seminar 18.10.2016] Ody
Prof. Dr. Ernst-Rüdiger Olderog,
Department of Computing Science, FK II, University of Oldenburg,
D-26111 Oldenburg, Germany
To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.