Abstract. We apply Uppaal Tiga to automatically compute adaptive scheduling strategies for an industrial case study dealing with a state-of-the-art image processing pipeline of a printer. As far as we know, this is the first application of timed automata technology to an industrial scheduling problem with uncertainty in job arrivals. Marco Bernardo. Markovian Testing Equivalence and Exponentially Timed Internal Actions In the theory of testing for Markovian processes developed so far, exponentially timed internal actions are not admitted within processes. sent, these actions cannot be abstracted away as their execution takes a nonzero amount of time. On the other hand, they must be carefully taken into account in order not to equate processes that are distinguishable from a timing viewpoint. In this paper we recast the definition of Markovian testing equivalence in the framework of a Markovian process calculus including exponentially timed internal actions. Then we show that the result...