A Modal µ-Calculus for Durational Transition Systems

Durational transition systems are finite transition systems where every transition is additionally equipped with a duration. We consider the problem of interpreting {formulas over durational transition systems. In case the formula contains only operations minimum, maximum, addition, and sequencing, we show that the interpretation ist not only computable but (up to a linear factor) as eciently computable as the interpretation of {formulas over ordinary finite transition systems