Publications

See also the DBLP entry for Lijun Zhang. At the moment this page contains publications of two different people with the name "Lijun Zhang", and contains also links to 12 other "Lijun Zhang"s. My Chinese name is:

. There are many different Chinese names, mapping to the same English name "Lijun Zhang". According to this page there arecurrently 1967

registered, 89% of which are male.

Please respect the corresponding copyright by the publishers. For some papers, additional comments and corrections are given in red text in the pdfs.

2012

Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm. (NFM'12 with David N. Jansen and Flemming Nielson)
A general framework for probabilistic characterizing formulae. (VMCAI'12 with Joshua Sack)
Safety Verification for Probabilistic Hybrid Systems (to appear in European Journal of Control with Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn. A preliminary version appeared in CAV'10)

2011

Efficient Approximation of Optimal Control for Markov Games. (FSTTCS'11 with John Fearnley, Markus Rabe and Sven Schewe)
Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems(QEST'11 with Moritz Hahn, Gethin Norman, David Parker and Björn Wachter)
Bisimulations Meet PCTL Equivalences for Probabilistic Automata(CONCUR'11 with Lei Song and Jens Chr. Godskesen)
Automata-based CSL model checking (ICALP'11 with David N. Jansen, Flemming Nielson and Holger Hermanns)
On Stabilization in Herman's Algorithm (ICALP'11 with Stefan Kiefer, Andrzej Murawski, Joel Ouaknine and James Worrell)
Model Checking Algorithms for CTMDPs (CAV'11 with Peter Buchholz, Ernst Moritz Hahn and Holger Hermanns)
Synthesis for PCTL in Parametric Markov Decision Processes (NFM'11 with Ernst Moritz Hahn and Tingting Han)
Measurability and Safety Verification for Stochastic Hybrid Systems (HSCC'11 with Martin Fränzle, Ernst Moritz Hahn, Holger Hermannsand Nicolás Wolovick)
Probabilistic Logical Characterization (Information and Computation with Holger Hermanns, Augusto Parma, Roberto Segala and Björn Wachter)
Probabilistic Reachability for Parametric Markov Models (STTT with Ernst Moritz Hahn, Holger Hermanns. A preliminary version appeared in SPIN'09)
From Concurrency Models to Numbers: Performance and Dependability (Software and Systems Safety: Specification and Verification, with Holger Hermanns)

2010

Concurrency and Composition in a Stochastic World (CONCUR'10 with Christian Eisentraut, Holger Hermanns, invited paper)
Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains (SPIN'10 with Georgel Calin, Pepijn Crouzen, Pedro R. D'Argenio and E. Moritz Hahn)
Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes (QEST'10 with Martin R. Neuhäußer)
On Probabilistic Automata In Continuous Time (LICS'10 with Christian Eisentraut, Holger Hermanns)
Safety Verification for Probabilistic Hybrid Systems (CAV'10 with Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn)
PARAM: A Model Checker for Parametric Markov Models (CAV'10 with Ernst Moritz Hahn, Holger Hermanns, Björn Wachter)
Model Checking Interactive Markov Chains (TACAS'10 with Martin R. Neuhäußer.)
PASS: Abstraction Refinement for Infinite Probabilistic Models (TACAS'10 with Ernst Moritz Hahn, Holger Hermanns, Björn Wachter)
Best probabilistic transformers and beyond. (VMCAI'10 with Björn Wachter)

2009

FlowSim Simulation Benchmarking Platform (QEST'09 with Jonathan Bogdoll, Holger Hermanns)
Probabilistic Reachability for Parametric Markov Models (SPIN'09 with Ernst Moritz Hahn, Holger Hermanns)
INFAMY: An Infinite-State Markov Model Checker (CAV'09 with Ernst Moritz Hahn, Holger Hermanns, Björn Wachter)
Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains (Fundamenta Informaticae with Ernst Moritz Hahn, Holger Hermanns, Björn Wachter. A preliminary version appeared in ACSD'08)

2008

A Space-Efficient Probabilistic Simulation Algorithm (revised full version of 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, Ernst Moritz Hahn, 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)

2007

Deciding Simulations on Probabilistic Automata (ATVA'07 with Holger Hermanns)
Probabilistic Model Checking Modulo 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.)

2005

Hardware Reliability (Dependability Metrics 2005 with Irene Eusgeld, Bernhard Fechner, Felix Salfner, Max Walter, Philipp Limbourg)
Logic and model checking for hidden Markov models (FORTE'05 with Holger Hermanns, David N. Jansen.)

Technical Reports:

On probabilistic automata in continuous time. (AVACS Report with Christian Eisentraut, Holger Hermanns)
Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. (AVACS Report with Georgel Calin, Pepijn Crouzen, Ernst Moritz Hahn, Pedro D'Argenio)
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 Ernst 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)
Logic and model checking for hidden Markov models. (AVACS Report with Holger Hermanns, and David N. Jansen. )

Lijun Zhang

Last modified: Tue Jan 24 18:16:35 CET 2012