Assume-guarantee reasoning for Interactive Markov Chains
- 11:00 26th November 2013 ( week 7, Michaelmas Term 2013 )441
Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms for assume-guarantee reasoning for IMC with respect to time-bounded properties. Firstly, we give a specification formalism for IMC. Secondly, given a time-bounded property, an IMC component and the assumption that its unknown environment satisfies a given specification, we synthesize a scheduler for the component optimizing the probability that the property is satisfied in any such environment.
Speaker bio
Jan Krčál focuses in his research on fundamental questions from theory of stochastic processes, Markov decision processes, and stochastic games. He applies these questions to the modeling formalisms from the area of probabilistic verification and performance evaluation.Since 2009, Jan has been studying PhD in computer science at Masaryk University, Brno, Czech Republic. During his studies, he was awarded a Dean's prize, co-authored 6 papers at high-quality international conferences, attended numerous summer/winter schools, and gave several seminar talks, e.g., at TU Munich, Saarland University or Uppsala University. In September 2013, Jan moved to the Saarland University for a post-doc position.
Share this:
