Publications | Trustworthy Intelligent Systems

2021

Verifying Pufferfish Privacy in Hidden Markov Models. Depeng Liu, Bow-Yaw Wang and Lijun Zhang, to appear in VMCAI 2022
A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. Yong Li, Yu-Fang Chen, Lijun Zhang, Depeng Liu. Information and Computation, 104678. (2021)
Probabilistic Verification of Neural Networks Against Group Fairness. Bing Sun, Jun Sun, Ting Dai, Lijun Zhang. FM 2021: 83-102
Enhancing robustness verification for deep neural networks via symbolic propagation.Yang, P., Li, J., Liu, J., Huang, C. C., Li, R., Chen, L., … & Zhang, L. (2021). Formal Aspects of Computing, 1-29.
Solving Not-Substring Constraint withFlat Abstraction. Abdulla, P. A., Atig, M. F., Chen, Y. F., Diep, B. P., Holík, L., Hu, D., … & Yen, D. D. (2021, October). In Asian Symposium on Programming Languages and Systems (pp. 305-320). Springer, Cham.
Frontmatter: mining Android user interfaces at scale. Kuznetsov, K., Fu, C., Gao, S., Jansen, D. N., Zhang, L., & Zeller, A. (2021, August). In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (pp. 1580-1584).
Formal Verification of Consensus in the Taurus Distributed Database. Gao, S., Zhan, B., Liu, D., Sun, X., Zhi, Y., Jansen, D. N., & Zhang, L. (2021, November). In International Symposium on Formal Methods (pp. 741-751). Springer, Cham.
An axiom system of probabilistic Mu-calculus. Liu, W., Xu, J., Jansen, D. N., Turrini, A., & Zhang, L. (2021). Tsinghua Science and Technology, 27(2), 372-385.
Synthesizing Good-Enough Strategies for LTLf Specifications. Li, Y., Turrini, A., Vardi, M. Y., & Zhang, L. IJCAI 2021: 4144-4151
Congruence Relations for Büchi Automata. Li, Y., Tsay, Y. K., Turrini, A., Vardi, M. Y., & Zhang, L. (2021). FM 2021: 465-482
Improving Neural Network Verification through Spurious Region Guided Refinement, Yang, P.; Li, R.; Li, J.; Huang, C.-C.; Wang, J.; Sun, J.; Xue, B. and Zhang, L. In TACAS, LNCS , 2021.

2020

Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications, Bansal, S.; Li, Y.; Tabajara, L. M. and Vardi, M. Y. In AAAI, pages 9766-9774, 2020.
On Correctness, Precision, and Performance in Quantitative Verification, Budde, C. E.; Hartmanns, A.; Klauck, M.; Křetínský, J.; Parker, D.; Quatmann, T. and Turrini, A. In ISoLA, 2020.
A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving, Chen, Y.-F.; Havlena, V.; Lengál, O. and Turrini, A. In APLAS, 2020.
Modelling and Implementation of Unmanned Aircraft Collision Avoidance, Feng, W.; Huang, C.-C.; Turrini, A. and Li, Y. In SETTA, 2020.
LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, Hermanns, H.; Zhang, L.; Kobayashi, N. and Miller, D., ed. ACM, 2020.
An O(m log n) algorithm for branching bisimilarity on labelled transition systems, Jansen, D. N.; Groote, J. F.; Keiren, J. J. A. and Wijs, A. In TACAS (2), pages 3-20, Springer, Lecture Notes in Computer Science 12079, 2020.
A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains, Jansen, D. N.; Groote, J. F.; Timmers, F. and Yang, P. In CONCUR, pages 8:1-8:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs 171, 2020.
How does Weight Correlation Affect Generalisation Ability of Deep Neural Networks?, Jin, G.; Yi, X.; Zhang, L.; Zhang, L.; Schewe, S. and Huang, X. In NeurIPS, 2020.
Accelerated Verification of Parametric Protocols with Decision Trees, Li, Y.; Cao, T.; Jansen, D. N.; Pang, J. and Wei, X. In ICCD, pages 397-404, IEEE, 2020.
Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings, Pang, J. and Zhang, L., ed. Springer, Lecture Notes in Computer Science 12153, 2020.
SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM, Li, X.; Li, Y.; Li, Y.; Sun, X.; Turrini, A. and Zhang, L. In ESEC/FSE, 2020.
PRODeep: a platform for robustness verification of deep neural networks, Li, R.; Li, J.; Huang, C.-C.; Yang, P.; Huang, X.; Zhang, L.; Xue, B. and Hermanns, H. In ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020, pages 1630-1634, ACM, 2020.
Probabilistic Preference Planning Problem for Markov Decision Processes, Li, M.; Turrini, A.; Hahn, E. M.; She, Z. and Zhang, L. In TSE, 2020.
Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling, Li, Y.; Turrini, A.; Sun, X. and Zhang, L. In ATVA, 2020.
On the Power of Unambiguity in Büchi Complementation, Li, Y.; Vardi, M. Y. and Zhang, L. In GANDALF, pages 182-198, Electronic Proceedings in Theoretical Computer Science 326, 2020.

2019

An Initial Study on the Relationship Between Meta Features of Dataset and the Initialization of NNRW, Cao, W.; Patwary, M. J. A.; Yang, P.; Wang, X. and Ming, Z. In IJCNN, pages 1-8, 2019.
The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report), Hahn, E. M.; Hartmanns, A.; Hensel, C.; Klauck, M.; Klein, J.; Kret'inský, J.; Parker, D.; Quatmann, T.; Ruijters, E. and Steinmetz, M. In TACAS (3), pages 69-92, LNCS 11429, 2019.
Interval Markov Decision Processes with Multiple Objectives: from Robust Strategies to Pareto Curves, Hahn, E. M.; Hashemi, V.; Hermanns, H.; Lahijanian, M. and Turrini, A. In TOMACS, 29, 2019.
Omega-Regular Objectives in Model-Free Reinforcement Learning, Hahn, E. M.; Perez, M.; Schewe, S.; Somenzi, F.; Trivedi, A. and Wojtczak, D. In TACAS (1), pages 395-412, LNCS 11427, 2019.
Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification, Li, J.; Liu, J.; Yang, P.; Chen, L.; Huang, X. and Zhang, L. In SAS, pages 296-319, LNCS 11822, 2019.
Synthesizing Nested Ranking Functions for Loop Programs via SVM, Li, Y.; Sun, X.; Li, Y.; Turrini, A. and Zhang, L. In ICFEM, pages 438-454, LNCS 11852, 2019.
ROLL 1.0: ω-Regular Language Learning Library, Li, Y.; Sun, X.; Turrini, A.; Chen, Y.-F. and Xu, J. In TACAS, pages 365-371, LNCS 11427, 2019.
SAT-based explicit LTL reasoning and its application to satisfiability checking, Li, J.; Zhu, S.; Pu, G.; Zhang, L. and Vardi, M. Y. In Formal Methods in System Design, 54: 164-190, 2019.
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, Vojnar, T. and Zhang, L., ed. Springer, Lecture Notes in Computer Science 11427, 2019.
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, Vojnar, T. and Zhang, L., ed. Springer, Lecture Notes in Computer Science 11428, 2019.
An Axiomatisation of the Probabilistic μ-Calculus, Xu, J.; Liu, W.; Jansen, D. N. and Zhang, L. In ICFEM, pages 420-437, LNCS 11852, 2019.

2018

Advanced Automata-based Algorithms for Program Termination Checking, Chen, Y.-F.; Heizmann, M.; Lengál, O.; Li, Y.; Tsai, M.-H.; Turrini, A. and Zhang, L. In PLDI, pages 135-150, 2018.
The Quest for Minimal Quotients for Probabilistic and Markov Automata, Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. In Information and Computation, 262, Part 1: 162-186, 2018.
Preface for the special issue for ATVA 2015, Finkbeiner, B.; Pu, G. and Zhang, L. In Acta Informatica, 55: 625-626, 2018.
Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems, Fu, C.; Turrini, A.; Huang, X.; Song, L.; Feng, Y. and Zhang, L. In IJCAI, pages 4757-4763, 2018.
Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution), Heizmann, M.; Chen, Y.-F.; Dietsch, D.; Greitschus, M.; Hoenicke, J.; Li, Y.; Nutz, A.; Musa, B.; Schilling, C.; Schindler, T. and Podelski, A. In TACAS, LNCS , 2018.
An Automatic Proving Approach to Parameterized Verification, Li, Y.; Duan, K.; Jansen, D. N.; Pang, J.; Zhang, L.; Lv, Y. and Cai, S. In ACM Trans. Comput. Log., 19: 27:1-27:25, 2018.
Accelerating LTL satisfiability checking by SAT solvers, Li, J.; Pu, G.; Zhang, L.; Vardi, M. Y. and He, J. In J. Log. Com.: exy013, 2018.
Learning to Complement Büchi Automata, Li, Y.; Turrini, A.; Zhang, L. and Schewe, S. In VMCAI, pages 313-335, LNCS 10747, 2018.
An explicit transition system construction approach to LTL satisfiability checking, Li, J.; Zhang, L.; Zhu, S.; Pu, G.; Vardi, M. Y. and He, J. In Formal Asp. Comput., 30: 193-217, 2018.
29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, Schewe, S. and Zhang, L., ed. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs 118, 2018.
Probabilistic Bisimulation for Realistic Schedulers, Zhang, L.; Yang, P.; Song, L.; Hermanns, H.; Eisentraut, C.; Jansen, D. N. and Godskesen, J. C. In Acta Inf., 2018.

2017

JANI: Quantitative Model and Tool Interaction, Budde, C. E.; Dehnert, C.; Hahn, E. M.; Hartmanns, A.; Junges, S. and Turrini, A. In TACAS, pages 151-168, LNCS 10206, 2017.
Model Checking ω-regular Properties for Quantum Markov Chains, Feng, Y.; Hahn, E. M.; Turrini, A. and Ying, S. In CONCUR, pages 35:1-35:16, LIPIcs 85, 2017.
Precisely deciding CSL formulas through approximate model checking for CTMCs, Feng, Y. and Zhang, L. In J. Comput. Syst. Sci., 89: 361-371, 2017.
Finding Polynomial Loop Invariants for Probabilistic Programs, Feng, Y.; Zhang, L.; Jansen, D. N.; Zhan, N. and Xia, B. In ATVA, pages 400-416, LNCS 10482, 2017.
On Equivalence Checking of Nondeterministic Finite Automata, Fu, C.; Deng, Y.; Jansen, D. N. and Zhang, L. In SETTA, pages 216-231, LNCS 10606, 2017.
Multi-objective Robust Strategy Synthesis for Interval MDPs, Hahn, E. M.; Hashemi, V.; Hermanns, H.; Lahijanian, M. and Turrini, A. In QEST, pages 207-223, LNCS 10503, 2017.
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In VMCAI, pages 266-287, LNCS 10145, 2017.
Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs, Hashemi, V.; Turrini, A.; Hahn, E. M.; Hermanns, H. and Elbassioni, K. In SETTA, pages 25-41, LNCS 10606, 2017. (Best paper award)
A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees, Li, Y.; Chen, Y.-F.; Zhang, L. and Liu, D. In TACAS, pages 208-226, LNCS 10205, 2017.
A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems, Wang, S.; Zhan, N. and Zhang, L. In Formal Asp. Comput., 29: 751-775, 2017.
Distribution-Based Bisimulation for Labelled Markov Processes, Yang, P.; Jansen, D. N. and Zhang, L. In FORMATS, pages 170-186, LNCS 10419, 2017.

2016

Efficient approximation of optimal control for continuous-time Markov games, Fearnley, J.; Rabe, M. N.; Schewe, S. and Zhang, L. In Inf. Comput., 247: 106-129, 2016.
Deciding Probabilistic Automata Weak Bisimulation: Theory and Practice, Ferrer Fioriti, L. M.; Hashemi, V.; Hermanns, H. and Turrini, A. In Formal Aspects of Computing, 28: 109-143, 2016.
Exploiting Robust Optimization for Interval Probabilistic Bisimulation, Hahn, E. M.; Hashemi, V.; Hermanns, H. and Turrini, A. In QEST, pages 55-71, LNCS 9826, 2016.
A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In CAV, pages 291-311, LNCS 9780, 2016.
Compositional Bisimulation Minimization for Interval Markov Decision Processes, Hashemi, V.; Hermanns, H.; Song, L.; Subramani, K.; Turrini, A. and Wojciechowski, P. In LATA'16, pages 114-126, LNCS 9618, 2016.
Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes, He, F.; Gao, X.; Wang, M.; Wang, B.-Y. and Zhang, L. In ACM Trans. Softw. Eng. Methodol., 25: 21:1-21:39, 2016.
An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties, Li, Y.; Liu, W.; Turrini, A.; Hahn, E. M. and Zhang, L. In SETTA, pages 280-296, LNCS 9984, 2016.
Verify LTL with Fairness Assumptions Efficiently, Li, Y.; Song, L.; Feng, Y. and Zhang, L. In TIME, 2016.
GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs, Wu, Z.; Hahn, E. M.; Günay, A.; Zhang, L. and Liu, Y. In ECAI, pages 1726-1727, 2016.
Multiphase until formulas over Markov reward models: An algebraic approach, Xu, M.; Zhang, L.; Jansen, D. N.; Zhu, H. and Yang, Z. In Theor. Comput. Sci., 611: 116-135, 2016.
A space-efficient simulation algorithm on probabilistic automata, Zhang, L. and Jansen, D. N. In Inf. Comput., 249: 138-159, 2016.

2015

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation, Chen, Y.-F.; Hong, C.-D.; Wang, B.-Y. and Zhang, L. In Computer Aided Verification (CAV), pages 658-674, Springer, 2015.
A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking, van Dijk, T.; Hahn, E. M.; Jansen, D. N.; Li, Y.; Neele, T.; Stoelinga, M.; Turrini, A. and Zhang, L. In Dependable Software Engineering, Theories, Tools, and Applications. First International Symposium (SETTA 2015), pages 35-54, Springer, Lecture Notes in Computer Science 9409, 2015.
QPMC: A Model Checker for Quantum Programs and Protocols, Feng, Y.; Hahn, E. M.; Turrini, A. and Zhang, L. In Twentieth international symposium of the Formal Methods Europe association (FM), pages 265-272, Springer, Lecture Notes in Computer Science 9109, 2015.
A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm, Feng, Y. and Zhang, L. In Distributed Computing, 28: 233-244, 2015.
Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, Finkbeiner, B.; Pu, G. and Zhang, L., ed. Springer, Lecture Notes in Computer Science 9364, 2015.
Transient Reward Approximation for Continuous-Time Markov Chains, Hahn, E. M.; Hermanns, H.; Wimmer, R. and Becker, B. In IEEE Transactions on Reliability, 64: 1254-1275, 2015.
Lazy Probabilistic Model Checking without Determinisation, Hahn, E. M.; Li, G.; Schewe, S.; Turrini, A. and Zhang, L. In CONCUR, pages 354-367, LIPIcs 42, 2015.
Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems, He, F.; Gao, X.; Wang, B.-Y. and Zhang, L. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-15), pages 503-514, ACM, 2015.
Preference Planning for Markov Decision Processes, Li, M.; She, Z.; Turrini, A. and Zhang, L. In The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15), pages 3313-3319, AAAI Press, 2015.
A Simple Probabilistic Extension of Modal Mu-calculus, Liu, W.; Song, L.; Wang, J. and Zhang, L. In International Joint Conference on Artificial Intelligence (IJCAI), pages 882-888, AAAI Press, 2015.
Planning for Stochastic Games with Co-safe Objectives, Song, L.; Feng, Y. and Zhang, L. In International Joint Conference on Artificial Intelligence (IJCAI), pages 1682-1688, AAAI Press, 2015.
Decentralized Bisimulation for Multiagent Systems, Song, L.; Feng, Y. and Zhang, L. In International Conference on Autonomous Agents & Multiagent Systems (AAMAS), pages 209-217, ACM, 2015.
Polynomial Time Decision Algorithms for Probabilistic Automata, Turrini, A. and Hermanns, H. In Information and Computation, 244: 134-171, 2015.

2014

When Equivalence and Bisimulation Join Forces in Probabilistic Automata, Feng, Y. and Zhang, L. In Nineteenth international symposium of the Formal Methods Europe association (FM), Springer, Lecture Notes in Computer Science , 2014.
A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm, Feng, Y. and Zhang, L. In Concurrency Theory - 25th International Conference (CONCUR 2014), pages 342-356, Springer, LNCS 8704, 2014.
Reachability and Reward Checking for Stochastic Timed Automata, Hahn, E. M.; Hartmanns, A. and Hermanns, H. In AVoCS, 2014.
IscasMC: A Web-Based Probabilistic Model Checker, Hahn, E. M.; Li, Y.; Schewe, S.; Turrini, A. and Zhang, L. In Nineteenth international symposium of the Formal Methods Europe association (FM), pages 312-317, Springer, Lecture Notes in Computer Science 8442, 2014.
Probably safe or live, Katoen, J.-P.; Song, L. and Zhang, L. 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.
Aalta: an LTL satisfiability checker over Infinite/Finite traces, Li, J.; Yao, Y.; Pu, G.; Zhang, L. and He, J. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014), pages 731-734, ACM, 2014.
LTLf Satisfiability Checking, Li, J.; Zhang, L.; Pu, G.; Vardi, M. Y. and He, J. 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.
Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes, Song, L.; Zhang, L. and Godskesen, J. C. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference (VMCAI), pages 98-117, Springer, Lecture Notes in Computer Science 8318, 2014.
Incremental Bisimulation Abstraction Refinement, Song, L.; Zhang, L.; Hermanns, H. and Godskesen, J. C. In Transactions on Embedded Computing Systems (TECS), 13: 142:1-142:23, 2014.
Model Checking CSL for Markov Population Models, Spieler, D.; Hahn, E. M. and Zhang, L. In QAPL, pages 93-107, 2014.
Cost Preserving Bisimulations for Probabilistic Automata, Turrini, A. and Hermanns, H. In Logical Methods in Computer Science, 4: 1-58, 2014.

2013

Model Repair for Markov Decision Processes, Chen, T.; Hahn, E. M.; Han, T.; Kwiatkowska, M.; Qu, H. and Zhang, L. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 85-92, IEEE, 2013.
Computing Cumulative Rewards Using Fast Adaptive Uniformisation, Dannenberg, F.; Hahn, E. M. and Kwiatkowska, M. Z. In Computational Methods in Systems Biology - 11th International Conference (CMSB), pages 33-49, Springer, Lecture Notes in Computer Science 8130, 2013.
Deciding Bisimilarities on Distributions, Eisentraut, C.; Hermanns, H.; Krämer, J.; Turrini, A. and Zhang, L. In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 72-88, Springer, Lecture Notes in Computer Science 8054, 2013.
A Semantics for Every GSPN, Eisentraut, C.; Hermanns, H.; Katoen, J.-P. and Zhang, L. 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.
The Quest for Minimal Quotients for Probabilistic Automata, Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. 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.
A Tighter Bound for the Self-Stabilization Time in Herman's Algorithm, Feng, Y. and Zhang, L. In Information Processing Letters, 113: 486-488, 2013.
CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains, Gao, Y.; Hahn, E. M.; Zhan, N. and Zhang, L. In Automated Technology for Verification and Analysis - 11th International Symposium (ATVA), pages 464-468, Springer, Lecture Notes in Computer Science 8172, 2013.
Model Checking Conditional CSL for Continuous-Time Markov Chains, Gao, Y.; Xu, M.; Zhan, N. and Zhang, L. In Information Processing Letters, 113: 44-50, 2013.
On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation, Hashemi, V.; Hermanns, H. and Turrini, A. In ECEASST, 66, 2013.
Cost Preserving Bisimulations for Probabilistic Automata, Hermanns, H. and Turrini, A. In Concurrency Theory - 24th International Conference (CONCUR), pages 349-363, Springer, Lecture Notes in Computer Science 8052, 2013.
Revisiting Weak Simulation for Substochastic Markov Chains, Jansen, D. N.; Song, L. and Zhang, L. In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 209-224, Springer, Lecture Notes in Computer Science 8054, 2013.
On the Relationship between LTL Normal Forms and Büchi Automata, Li, J.; Pu, G.; Zhang, L.; Wang, Z.; He, J. and Larsen, K. G. 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.
LTL Satisfiability Checking Revisited, Li, J.; Zhang, L.; Pu, G.; Vardi, M. and He, J. In 20th International Symposium on Temporal Representation and Reasoning (TIME), IEEE Comp. Society Press, 2013.
Bisimulations Meet PCTL Equivalences for Probabilistic Automata, Song, L.; Zhang, L.; Godskesen, J. C. and Nielson, F. In Logical Methods in Computer Science, 9, 2013.
Incremental Bisimulation Abstraction Refinement, Song, L.; Zhang, L.; Hermanns, H. and Godskesen, J. C. In 13th International Conference on Application of Concurrency to System Design (ACSD), pages 11-20, IEEE, 2013.