MASARYK UNIVERSITY FACULTY OF INFORMATICS}w !"#$%&'()+,-./012345<yA| Formal Analysis of Discrete-Event Systems

I declare that this thesis is my own work and has not been submitted in any form for another degree or diploma at any university or other institution of tertiary education. Information derived from the published or unpublished work of others has been acknowledged in the text and a list of references is given. Advisor: prof. RNDr. Antonín Kučera, Ph.D. iii iv v Discrete-event systems (DES) are widely used as a modelling formalism in prob-abilistic verification and performance evaluation. The behaviour of these models is driven by discrete events that occur randomly in continuous time. We study the impact of hard real-time bounds within DES such as time-outs changing the state of the model or deadlines in the specification of the desired behaviour of the model. Previously, there was no rigorous foundational material on such hard real