Research Training Group SCARE

Heinrich Ody


In economics discounting represents that money earned soon can be
reinvested earlier and hence yields more revenue than money earned
later. Discounting has been introduced into temporal logics to formally
express that something should happen soon. This can be described also as
quantifying the temporal quality of a system.


A typical example is a rail road crossing. Consider the property: "after
a train passes, the gates are open eventually". While a controller
leaving the gates closed an hour after the train has passed might be
safe and alive, it is not useful. We can use discounting to express that
the controller should not wait unnecessarily long before opening the gates.


So far discounting in logics only has been studied for discrete-time
temporal logics (LTL, CTL*, mu-calculus). In this talk I first explain
discounting in temporal logics. Then I introduce discounted Duration
Calculus along with some example formulas. Consider a robot that uses
energy in working mode and conserves energy in idle mode. Then one
example formula is: "the energy of the robot will last long".