Lijun Zhang
| Oxford University, |
| Computing Laboratory, |
| Office:
Room 415, Wolfson Building |
| Address:Parks Road, Oxford OX1 3QD, UK |
| eMail:first.last@comlab.ox.ac.uk |
About me:
I am a postdoctoral researcher
working with Andrzej Murawski,
Joel Ouaknine, and
James Worrel at
Oxford University Computing Laboratory.
Before this I was a Ph.D. student and later a postdoc at the chair of Prof. Dr.-Ing.
Holger Hermanns, the head of the Dependable Systems and Software Group of the Universität des
Saarlandes. I defended my the thesis in December 2008. More Information about me
please find in my curriculum vitae.
Research Interests:
Probabilistic models, simulation
reduction, decision algorithms for probabilistic simulation preorders,
abstraction and model checking.
I am involved in the following tools:
I am currently involved in the
following projects:
Involved projects in the past (at Saarland University):
Publications:
Recent Papers:
Refereed Papers:
- Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains (Fundamentae Informaticae'09 with E. Moritz Hahn, Holger Hermanns, Björn Wachter. A preliminary version appeared in ACSD'08)
- FlowSim Simulation Benchmarking Platform (QEST'09 with Jonathan Bogdoll, Holger Hermanns)
- Probabilistic Reachability for Parametric Markov Models (SPIN'09 with E. Moritz Hahn, Holger Hermanns)
- INFAMY: An Infinite-State Markov Model Checker (CAV'09 with E. Moritz Hahn, Holger Hermanns, Björn Wachter)
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations (LMCS'08 with Holger Hermanns, Friedrich Eisenbrand, David N. Jansen. A preliminary version appeared in TACAS'07)
- A Space-Efficient Probabilistic Simulation Algorithm (CONCUR'08)
- On the minimisation of acyclic models(CONCUR'08 with Pepijn Crouzen, Holger Hermanns)
- Probabilistic CEGAR (CAV'08 with Holger Hermanns, Björn Wachter)
- An Experimental Evaluation of Probabilistic Simulation (FORTE'08 with Jonathan Bogdoll, Holger Hermanns)
- Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains (ACSD'08 with Holger Hermanns, E. Moritz Hahn, Björn Wachter)
- Deciding Simulations on Probabilistic Automata (ATVA'07 with Holger Hermanns)
- Probabilistic Model Checking Modular Theories (QEST'07 with Björn Wachter, Holger Hermanns)
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations (TACAS'07 with Holger Hermanns, Friedrich Eisenbrand, David N. Jansen.)
- Logic and model checking for hidden Markov models (FORTE'05 with Holger Hermanns, David N. Jansen.)
Technical Reports and Non-Refereed Papers:
- Best probabilistic transformers and beyond. (AVACS Report with Björn Wachter)
- Time-bounded model checking of infinite-state continuous-time Markov chains. (AVACS Report with E. Moritz Hahn, Holger Hermanns, Björn Wachter)
- No cycling? Go faster! On the minimization of acyclic models. (AVACS Report with Pepijn Crouzen, Holger Hermanns)
- On probabilistic CEGAR. (AVACS Report with Holger Hermanns, Björn Wachter)
- Hardware Reliability (Dependability Metrics 2005 with Irene Eusgeld, Bernhard Fechner, Felix Salfner, Max Walter, Philipp Limbourg)
- Logic and model checking for hidden Markov models. (AVACS Report with Holger Hermanns, and David N. Jansen. )
Thesis:
- Master thesis: Logic and Model Checking for Hidden Markov Models, Saarland University, Apr., 2004.
- PhD thesis: Decision Algorithms for Probabilistic Simulations, Saarland University, Dec., 2008.
Student Projects:
- E. Moritz Hahn: Parametric Markov Model Analysis, Master Thesis, Saarland University, 2008
- Jonathan Bogdoll: An Experimental Evaluation of Probabilistic Simulation, Bachelor Thesis, Saarland University, 2008
Teaching activities (at Saarland University)
As an Instructor:
As an Assistant:
Last modified: Fri Jan 29 12:40:41 GMT 2010
