Contact Mikkel Larsen Pedersen, postdoc (titles: M.Sc., PhD) Room 1.2.50 Department of Computer Science, Aalborg University Selma Lagerlöfs Vej 300 9220 Aalborg Ø Email: CV

About Me

I am a postdoc at Department of Computer Science at Aalborg University being involved in the project Modular Markovian Logics for Analysis of Stochastic Concurrent Systems working under Radu Mardare.

Until 31/10-2011, I was a ph.d. student in the MT-Lab project.

In June 2008 I graduated from Department of Mathematical Sciences with a Master degree in Mathematics (and a minor in Computer Science). My thesis 'Ramsey Theory for Graphs' focuses on a number of results in Ramsey theory, covering a wide range of graph theoretical tools.

I am interested in specification theories for probabilistic systems, that is, Markov Chains and Probabilistic Automata. I (and others) have developed a specification theory for Markov Chains. A specification in this theory is a model called a Constraint Markov Chain, which is essentially a underspecified Markov Chain. The Constraint Markov Chain allows for a set of Markov Chains as implementations. A goal is to present a notion of generalized model checking for Constraint Markov Chains, that is, given a Constraint Markov Chain and a boolean formula, does there exists an Markov Chain that implements the Constraint Markov Chain and in which the boolean formula is satisfied?

Current and upcoming activities

• I defended my PhD thesis Specification Theories for Probabilistic Systems succesfully on December 15th 2011 (invitation and abstract, slides, thesis)
• Radu Mardare will give the course Introduction to Logic and Model Theory in November-December 2011

Recent activities

• I will be presenting the paper New Results on Abstract Probabilistic Automata at ACSD'11
• The paper APAC: a tool for reasoning about Abstract Probabilistic Automata has been accepted at QEST'11
• The paper Constraint Markov Chains has been accepted in TCS
• The paper New Results on Abstract Probabilistic Automata has been accepted at ACSD'11
• The paper Decision Problems for Interval Markov Chains has been accepted at LATA'11
• The first version of the tool APAC has been released
• I will be visiting Axel Legay at IRISA (Rennes, France), 1st February - 1st May 2011
• I will be presenting the paper Abstract Probabilistic Automata at VMCAI'11
• I will be giving a talk at NWPT 2010 in Turku
• The paper Abstract Probabilistic Automata has been accepted at VMCAI'11
• The paper Compositional Design Methodology with Constraint Markov Chains has been accepted at QEST'10