Mark Timmer received the award for the best PhD dissertation in 2013  in the region Overijssel, the Netherlands for his thesis Efficient Modelling, Generation and Analysis of Markov Automata.  Mark obtained his PhD degree from the University of Twente, and was supervised by Joost-Pieter Katoen, Jaco van de Pol and Marielle Stoelinga. See also http://www.utwente.nl/nieuwsevents/!/2014/11/350971/overijssel-phd-award-voor-mark-timmer.

Our paper “High-level Counterexamples for Probabilistic Automata” by Ralf Wimmer, Nils Jansen, Erika Ábrahám and Joost-Pieter Katoen was accepted for publication in the journal Logical Methods in Computer Science (LMCS). In this paper we investigate the computation of several variations of (minimal) counterexamples that are represented in PRISM’s high-level language which defines a subclass of probabilistic programs. These NP-hard problems are solved […]

The paper “Compositional Analysis Using Component-Oriented Interpolation” by Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, and Thomas Noll has received the Best Paper Award at the 11th International Symposium on  Formal Aspects of Component Software (FACS 2014). It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.

The paper “Exponentially timed SADF: Compositional semantics, reduction, and analysis” by Joost-Pieter Katoen and Hao (Stephen) Wu has been accepted for EMSOFT’14 in New Delhi. The paper presents a compositional semantics of SADF using Markov automata, shows that non-determinism cannot occur, and exploits confluence reduction for scaling quantitative evaluation.

Sergey Sazonov, who completed his master thesis on “Property preservation under bisimulations on Markov Automata” at our chair, received an award of the CS department for completing his master studies with excellent grades. Congratulations!

Our paper “Fast Debugging of PRISM Models” by Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám and Joost-Pieter Katoen was accepted at ATVA 2014. The paper presents a new way to compute critical parts of a PRISM program by utilizing a MAX-SAT solver. This is the first approach rendering the computation of these sort of […]

The paper “Parametric LTL on Markov Chains” by Souymodip Chakraborty and Joost-Pieter Katoen has been accepted at the IFIP TCS conference. The paper shows the undecidability of verifying a Markov chain against a parametric LTL (pLTL) formula, and studies the complexity of model checking several logical fragments of pLTL.

The paper “Tight Game Abstractions of Probabilistic Automata” by Falak Sher and Joost-Pieter Katoen has been accepted at the conference Concurrency Theory. The paper presents game-based abstraction that is based on abstracting distributions (rather than states) and shows that this yields more accurate abstraction than state-based abstractions.

The paper “Minimal Counterexamples for Linear-Time Probabilistic Verification” by Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker was accepted for publication in the journal Theoretical Computer Science. The paper thoroughly examines the possibilities for computing so-called minimal critical subsystems for Markov decision processes by means of mixed integer linear programming.