RWTH Aachen hosts the Young Researchers’ Conference “Frontiers in Formal Methods”, February 25-27 2015.  Young researchers (up to two years after completing their PhD thesis) are encouraged to submit a 2-5 page abstract by January 12, 2015 (extended firm deadline). More information can be found here.

Hongfei Fu has successfully defended his PhD dissertation entitled “Verifying Probabilistic Systems: New Algorithms and Complexity Results”.  Hongfei started his PhD research in autumn 2010.  His examiners were Antonin Kucera (Masaryk University, Brno), Wolfgang Thomas and Stefan Kowalewski (see picture).   

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.

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!

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 papers “Probably Safe or Live” by Katoen, Song and Zhang, and “Zero-Reachability in Probabilistic Multi-Counter Automata” by Brazdil, Kiefer, Kucera, Novotny and Katoen have been accepted at CSL-LICS 2014 in Vienna.  The former paper classifies safety and liveness properties in the probabilistic setting while the second paper sets the ground for showing some flaws […]

The paper entitled “Layered Reduction for Abstract Probabilistic Automata” by Arpit Sharma and Joost-Pieter Katoen has been accepted for  the 14th Int. Conf. on Application of Concurrency on System Design (ACSD) 2014.