This page on Google Scholar contains publications from other authors with the same name. See this DBLP entry for Lijun Zhang and yet this one for Lijun Zhang (this one contains publications from other authors with the same name).
Most of my papers can be downloaded below: Please respect the corresponding copyright by the publishers. For some papers, additional comments and corrections are marked (in red text) in the pdfs.
- SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM, In ESEC/FSE, pages 1635-1639, ACM, 2020.
- Probabilistic Preference Planning Problem for Markov Decision Processes, In IEEE Trans. Software Eng., 48: 1545-1559, 2020.
- Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling, In ATVA, pages 467-483, Springer, LNCS 12302, 2020.
- On the Power of Unambiguity in Büchi Complementation, In GANDALF, pages 182-198, Electronic Proceedings in Theoretical Computer Science 326, 2020.
- Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification, In SAS, pages 296-319, Springer, LNCS 11822, 2019.
- Synthesizing Nested Ranking Functions for Loop Programs via SVM, In ICFEM, pages 438-454, LNCS 11852, 2019.
- An Axiomatisation of the Probabilistic μ-Calculus, In ICFEM, pages 420-437, LNCS 11852, 2019.
- The Quest for Minimal Quotients for Probabilistic and Markov Automata, In Inf. Comput., 262: 162-186, 2018.
- Probabilistic Bisimulation for Realistic Schedulers, In Acta Informatica, 55: 461-488, 2018.
- Advanced Automata-based Algorithms for Program Termination Checking, In PLDI, pages 135-150, 2018.
- Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems, In IJCAI, pages 4757-4763, ijcai.org, 2018.
- Learning to Complement Büchi Automata, In VMCAI, pages 313-335, Springer, LNCS 10747, 2018.
- Accelerating LTL satisfiability checking by SAT solvers, In J. Log. Comput., 28: 1011-1030, 2018.
- An explicit transition system construction approach to LTL satisfiability checking, In Formal Aspects Comput., 30: 193-217, 2018.
- An Automatic Proving Approach to Parameterized Verification, In ACM Trans. Comput. Log., 19: 27:1-27:25, 2018.
- Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games, In VMCAI, pages 266-287, LNCS 10145, 2017.
- A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees, In TACAS, pages 208-226, LNCS 10205, 2017.
- Distribution-Based Bisimulation for Labelled Markov Processes, In FORMATS, pages 170-186, LNCS 10419, 2017.
- On Equivalence Checking of Nondeterministic Finite Automata, In SETTA, pages 216-231, LNCS 10606, 2017.
- Finding Polynomial Loop Invariants for Probabilistic Programs, In ATVA, pages 400-416, LNCS 10482, 2017.
- Precisely deciding CSL formulas through approximate model checking for CTMCs, In J. Comput. Syst. Sci., 89: 361-371, 2017.
- A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems, In Formal Asp. Comput., 29: 751-775, 2017.
- A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, In CAV, pages 291-311, LNCS 9780, 2016.
- Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes, In ACM Trans. Softw. Eng. Methodol., 25: 21:1-21:39, 2016.
- Verify LTL with Fairness Assumptions Efficiently, In TIME, pages 41-50, IEEE Computer Society, 2016.
- An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties, In SETTA, pages 280-296, LNCS 9984, 2016.
- Efficient approximation of optimal control for continuous-time Markov games, In Inf. Comput., 247: 106-129, 2016.
- A space-efficient simulation algorithm on probabilistic automata, In Inf. Comput., 249: 138-159, 2016.
- Multiphase until formulas over Markov reward models: An algebraic approach, In Theor. Comput. Sci., 611: 116-135, 2016.
- GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs, In ECAI, pages 1726-1727, 2016.
- Lazy Probabilistic Model Checking without Determinisation, In CONCUR, pages 354-367, LIPIcs 42, 2015.
- Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation, In Computer Aided Verification (CAV), pages 658-674, Springer, 2015.
- A Simple Probabilistic Extension of Modal Mu-calculus, In International Joint Conference on Artificial Intelligence (IJCAI), pages 882-888, AAAI Press, 2015.
- Planning for Stochastic Games with Co-safe Objectives, In International Joint Conference on Artificial Intelligence (IJCAI), pages 1682-1688, AAAI Press, 2015.
- Decentralized Bisimulation for Multiagent Systems, In International Conference on Autonomous Agents & Multiagent Systems (AAMAS), pages 209-217, ACM, 2015.
- A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm, In Distributed Computing, 28: 233-244, 2015.
- Preference Planning for Markov Decision Processes, In The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15), pages 3313-3319, AAAI Press, 2015.
- Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems, In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-15), pages 503-514, ACM, 2015.
- Incremental Bisimulation Abstraction Refinement, In Transactions on Embedded Computing Systems (TECS), 13: 142:1-142:23, 2014.
- Probably safe or live, In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pages 55, ACM, 2014.
- A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm, In Concurrency Theory - 25th International Conference (CONCUR 2014), pages 342-356, Springer, LNCS 8704, 2014.
- Aalta: an LTL satisfiability checker over Infinite/Finite traces, In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014), pages 731-734, ACM, 2014.
- LTLf Satisfiability Checking, In 21st European Conference on Artificial Intelligence - Including Prestigious Applications of Intelligent Systems (ECAI 2014), pages 513-518, IOS Press, Frontiers in Artificial Intelligence and Applications 263, 2014.
- IscasMC: A Web-Based Probabilistic Model Checker, In Nineteenth international symposium of the Formal Methods Europe association (FM), pages 312-317, Springer, Lecture Notes in Computer Science 8442, 2014.
- When Equivalence and Bisimulation Join Forces in Probabilistic Automata, In Nineteenth international symposium of the Formal Methods Europe association (FM), Springer, Lecture Notes in Computer Science , 2014.
- Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes, In Verification, Model Checking, and Abstract Interpretation - 15th International Conference (VMCAI), pages 98-117, Springer, Lecture Notes in Computer Science 8318, 2014.
- Model Checking CSL for Markov Population Models, In QAPL, pages 93-107, 2014.
- LTL Satisfiability Checking Revisited, In 20th International Symposium on Temporal Representation and Reasoning (TIME), IEEE Comp. Society Press, 2013.
- Model Repair for Markov Decision Processes, In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 85-92, IEEE, 2013.
- Incremental Bisimulation Abstraction Refinement, In 13th International Conference on Application of Concurrency to System Design (ACSD), pages 11-20, IEEE, 2013.
- A Semantics for Every GSPN, In Application and Theory of Petri Nets and Concurrency - 34th International Conference (PETRI NETS), pages 90-109, Springer, Lecture Notes in Computer Science 7927, 2013.
- CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains, In Automated Technology for Verification and Analysis - 11th International Symposium (ATVA), pages 464-468, Springer, Lecture Notes in Computer Science 8172, 2013.
- On the Relationship between LTL Normal Forms and Büchi Automata, In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pages 256-270, Springer, Lecture Notes in Computer Science 8051, 2013.
- Deciding Bisimilarities on Distributions, In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 72-88, Springer, Lecture Notes in Computer Science 8054, 2013.
- Revisiting Weak Simulation for Substochastic Markov Chains, In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 209-224, Springer, Lecture Notes in Computer Science 8054, 2013.
- Bisimulations Meet PCTL Equivalences for Probabilistic Automata, In Logical Methods in Computer Science, 9, 2013.
- A Tighter Bound for the Self-Stabilization Time in Herman's Algorithm, In Information Processing Letters, 113: 486-488, 2013.
- The Quest for Minimal Quotients for Probabilistic Automata, In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference (TACAS), pages 16-31, Springer, Lecture Notes in Computer Science 7795, 2013.
- Model Checking Conditional CSL for Continuous-Time Markov Chains, In Information Processing Letters, 113: 44-50, 2013.
- Efficient CSL Model Checking Using Stratification, In Logical Methods in Computer Science, 8, 2012.
- Safety Verification for Probabilistic Hybrid Systems, In European Journal of Control, 18: 572-587, 2012.
- A General Framework for Probabilistic Characterizing Formulae, In Verification, Model Checking, and Abstract Interpretation - 13th International Conference (VMCAI), pages 396-411, Springer, Lecture Notes in Computer Science 7148, 2012.
- Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm, In NASA Formal Methods - 4th International Symposium (NFM), pages 326-340, Springer, Lecture Notes in Computer Science 7226, 2012.
- Probabilistic Logical Characterization, In Information and Computation, 209: 154-172, 2011.
- From Concurrency Models to Numbers -- Performance and Dependability, In Software and Systems Safety, pages 182-210, IOS Press, NATO Science for Peace and Security Series - D: Information and Communication Security 30, 2011.
- Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems, In Eighth International Conference on Quantitative Evaluation of Systems (QEST), pages 69-78, IEEE Computer Society, 2011.
- On Stabilization in Herman's Algorithm, In Automata, Languages and Programming - 38th International Colloquium (ICALP), pages 466-477, Springer, Lecture Notes in Computer Science 6756, 2011.
- Automata-Based CSL Model Checking, In Automata, Languages and Programming - 38th International Colloquium (ICALP), pages 271-282, Springer, Lecture Notes in Computer Science 6756, 2011.
- Synthesis for PCTL in Parametric Markov Decision Processes, In NASA Formal Methods - Third International Symposium (NFM), pages 146-161, Springer, Lecture Notes in Computer Science 6617, 2011.
- Model Checking Algorithms for CTMDPs, In Computer Aided Verification - 23rd International Conference (CAV), pages 225-242, Springer, Lecture Notes in Computer Science 6806, 2011.
- Measurability and safety verification for stochastic hybrid systems, In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 43-52, ACM, 2011.
- Bisimulations Meet PCTL Equivalences for Probabilistic Automata, In Concurrency Theory, 22nd International Conference (CONCUR), pages 108-123, Springer, Lecture Notes in Computer Science 6901, 2011.
- Efficient Approximation of Optimal Control for Continuous-Time Markov Games, In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 399-410, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs 13, 2011.
- Probabilistic Reachability for Parametric Markov Models, In STTT, 13: 3-19, 2011.
- On Probabilistic Automata in Continuous Time, In 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 342-351, IEEE CS Press, 2010.
- Concurrency and Composition in a Stochastic World, In Concurrency Theory, 21th International Conference (CONCUR), pages 21-39, Springer, Lecture Notes in Computer Science 6269, 2010.
- PARAM: A Model Checker for Parametric Markov Models, In Computer Aided Verification, 22nd International Conference (CAV), pages 660-664, Springer, Lecture Notes in Computer Science 6174, 2010.
- Safety Verification for Probabilistic Hybrid Systems, In Computer Aided Verification, 22nd International Conference (CAV), pages 196-211, Springer, Lecture Notes in Computer Science 6174, 2010.
- Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains, In Model Checking Software - 17th International SPIN Workshop, pages 193-211, Springer, Lecture Notes in Computer Science 6349, 2010.
- Model Checking Interactive Markov Chains, In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference (TACAS), pages 53-68, Springer, Lecture Notes in Computer Science 6015, 2010.
- PASS: Abstraction Refinement for Infinite Probabilistic Models, In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference (TACAS), pages 353-357, Springer, Lecture Notes in Computer Science 6015, 2010.
- Best Probabilistic Transformers, In Verification, Model Checking, and Abstract Interpretation, 11th International Conference (VMCAI), pages 362-379, Springer, Lecture Notes in Computer Science 5944, 2010.
- INFAMY: An Infinite-State Markov Model Checker, In Computer Aided Verification, 21st International Conference (CAV), pages 641-647, Springer, Lecture Notes in Computer Science 5643, 2009.
- Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains, In Fundamenta Informaticae, 95: 129-155, 2009.
- FlowSim Simulation Benchmarking Platform, In Sixth International Conference on the Quantitative Evaluation of Systems (QEST), pages 211-212, IEEE Computer Society, 2009.
- Probabilistic Reachability for Parametric Markov Models, In Model Checking Software, 16th International SPIN Workshop, pages 88-106, Springer, Lecture Notes in Computer Science 5578, 2009.
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations, In Logical Methods in Computer Science, 4, 2008.
- Time-bounded model checking of infinite-state continuous-time Markov chains, In 8th International Conference on Application of Concurrency to System Design (ACSD), pages 98-107, IEEE, 2008.
- Probabilistic CEGAR, In Computer Aided Verification, 20th International Conference (CAV), pages 162-175, Springer, Lecture Notes in Computer Science 5123, 2008.
- A Space-Efficient Probabilistic Simulation Algorithm, In Concurrency Theory, 19th International Conference (CONCUR), pages 248-263, Springer, Lecture Notes in Computer Science 5201, 2008.
- On the Minimisation of Acyclic Models, In Concurrency Theory, 19th International Conference (CONCUR), pages 295-309, Springer, Lecture Notes in Computer Science 5201, 2008.
- An Experimental Evaluation of Probabilistic Simulation, In Formal Techniques for Networked and Distributed Systems (FORTE), pages 37-52, Springer, Lecture Notes in Computer Science 5048, 2008.
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations, In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference (TACAS), pages 155-169, Springer, Lecture Notes in Computer Science 4424, 2007.
- Deciding Simulations on Probabilistic Automata, In Automated Technology for Verification and Analysis, 5th International Symposium (ATVA), pages 207-222, Springer, Lecture Notes in Computer Science 4762, 2007.
- Probabilistic Model Checking Modulo Theories, In Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST), pages 129-140, IEEE Computer Society, 2007.
- Logic and Model Checking for Hidden Markov Models, In Formal Techniques for Networked and Distributed Systems (FORTE), pages 98-112, Springer, Lecture Notes in Computer Science 3731, 2005.