2023
On Strategies in Synthesis Over Finite Traces , Bansal, S.; Li, Y.; Martinelli Tabajara, L.; Vardi, M. Y. and Wells, A.
In ATVA , LNCS , 2023.
A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions , Chen, Y.-F.; Havlena, V.; Lengál, O. and Turrini, A.
In J. Syst. Softw. , 2023.
On the Power of Finite Ambiguity in Büchi Complementation , Feng, W.; Li, Y.; Turrini, A.; Vardi, M. Y. and Zhang, L.
In Inf. Comput. , 2023.
Modular Mix-and-Match Complementation of Büchi Automata , Havlena, V.; Lengál, O.; Li, Y.; Šmahl'iková, B. and Turrini, A.
In TACAS , LNCS , 2023.
A novel family of finite automata for recognizing and learning ω-regular languages , Li, Y.; Schewe, S. and Tang, Q.
In ATVA , LNCS , 2023.
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata , Li, Y.; Schewe, S. and Vardi, M. Y.
In CONCUR , 2023.
Scenario Approach for Parametric Markov Models , Liu, Y.; Turrini, A.; Hahn, E. M.; Xue, B. and Zhang, L.
In ATVA , LNCS , 2023.
TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models , Zhang, L.; Xu, N.; Yang, P.; Jin, G.; Huang, C. and Zhang, L.
In ICCV , 2023.
2022
Compositional Safety LTL Synthesis , Bansal, S.; De Giacomo, G.; Di Stasio, A.; Li, Y.; Vardi, M. V. and Zhu, S.
In VSTTE'22 , 2022.
Deciding All Behavioral Equivalences at Once: A Game for Linear-Time-Branching-Time
Spectroscopy , Bisping, B.; Jansen, D. N. and Nestmann, U.
In Log. Methods Comput. Sci. , 18, 2022.
Solving string constraints with Regex-dependent functions through
transducers with priorities and variables , Chen, T.; Flores-Lamas, A.; Hague, M.; Han, Z.; Hu, D.; Kan, S.; Lin, A. W.; Rümmer, P. and Wu, Z.
In Proc. ACM Program. Lang. , 6: 1-31, 2022.
Quantitative Controller Synthesis for Consumption Markov Decision Processes , Fu, J.; Huang, C.-C.; Li, Y.; Mei, J.; Xu, M. and Zhang, L.
In Information Processing Letters , 2022.
EPMC Gets Knowledge in Multi-agent Systems , Fu, C.; Hahn, E. M.; Li, Y.; Schewe, S.; Sun, M.; Turrini, A. and Zhang, L.
In VMCAI , pages 93-107, Springer , Lecture Notes in Computer Science 13182, 2022.
Model Checking for Probabilistic Multiagent Systems , Fu, C.; Turrini, A.; Huang, X.; Song, L.; Feng, Y. and Zhang, L.
In Journal of Computer Science and Technology , 2022.
Explicit Bounds for Linear Forms in the Exponentials of Algebraic Numbers , Huang, C.-C.
In ISSAC , pages 371-379, ACM , 2022.
Rooted Divergence-Preserving Branching Bisimilarity is a Congruence:
A Simpler Proof , Jansen, D. N. and Liu, X.
In A Journey from Process Algebra via Timed Automata to Model Learning
- Essays Dedicated to Frits Vaandrager on the Occasion of His 60th
Birthday , pages 358-370, Springer , Lecture Notes in Computer Science 13560, 2022.
Synthesizing Ranking Functions for Loop Programs via SVM , Li, Y.; Li, X.; Li, Y.; Sun, X.; Turrini, A. and Zhang, L.
In TCS , 2022.
Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition , Li, Y.; Turrini, A.; Feng, W.; Vardi, M. Y. and Zhang, L.
In CAV , pages 152-173, Springer , Lecture Notes in Computer Science 13372, 2022.
Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning , Li, R.; Yang, P.; Huang, C.-C.; Sun, Y.; Xue, B. and Zhang, L.
In ICSE , IEEE , 2022.
Verifying Pufferfish Privacy in Hidden Markov Models , Liu, D.; Wang, B.-Y. and Zhang, L.
In VMCAI , pages 174-196, Springer , Lecture Notes in Computer Science 13182, 2022.
An Introduction to Quantum Model Checking , Turrini, A.
In Applied Sciences , 12, 2022.
CHA: Supporting SVA-like Assertions in Formal Verification of Chisel Programs , Yu, S.; Dong, Y.; Liu, J.; Li, Y.; Wu, Z.; Jansen, D. N. and Zhang, L.
In FMSE , 2022.
2021
Solving Not-Substring Constraint withFlat Abstraction , Abdulla, P. A.; Atig, M. F.; Chen, Y.-F.; Diep, B. P.; Hol'ik, L.; Hu, D.; Tsai, W.-L.; Wu, Z. and Yen, D.-D.
In APLAS , pages 305-320, Springer , Lecture Notes in Computer Science 13008, 2021.
Formal Verification of Consensus in the Taurus Distributed Database , Gao, S.; Zhan, B.; Liu, D.; Sun, X.; Zhi, Y.; Jansen, D. N. and Zhang, L.
In FM , pages 741-751, Springer , Lecture Notes in Computer Science 13047, 2021.
Frontmatter: mining Android user interfaces at scale , Kuznetsov, K.; Fu, C.; Gao, S.; Jansen, D. N.; Zhang, L. and Zeller, A.
In ESEC/SIGSOFT FSE , pages 1580-1584, ACM , 2021.
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 Inf. Comput. , 281: 104678, 2021.
Congruence Relations for Büchi Automata , Li, Y.; Tsay, Y.-K.; Turrini, A.; Vardi, M. Y. and Zhang, L.
In FM , pages 465-482, Springer , Lecture Notes in Computer Science 13047, 2021.
Synthesizing Good-Enough Strategies for LTLf Specifications , Li, Y.; Turrini, A.; Vardi, M. Y. and Zhang, L.
In IJCAI , pages 4144-4151, ijcai.org , 2021.
An Axiom System of Probabilistic Mu-Calculus , Liu, W.; Xu, J.; Jansen, D. N.; Turrini, A. and Zhang, L.
In Tsinghua Science and Technology , 27: 372-385, 2021.
Probabilistic Verification of Neural Networks Against Group Fairness , Sun, B.; Sun, J.; Dai, T. and Zhang, L.
In FM , pages 83-102, Springer , Lecture Notes in Computer Science 13047, 2021.
Enhancing Robustness Verification for Deep Neural Networks via Symbolic
Propagation , Yang, P.; Li, J.; Liu, J.; Huang, C.-C.; Li, R.; Chen, L.; Huang, X. and Zhang, L.
In Formal Aspects Comput. , 33: 407-435, 2021.
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 (1) , pages 389-408, Springer , Lecture Notes in Computer Science 12651, 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
- QComp 2020 Competition Report , Budde, C. E.; Hartmanns, A.; Klauck, M.; Kret'inský, J.; Parker, D.; Quatmann, T.; Turrini, A. and Zhang, Z.
In ISoLA (4) , pages 216-241, Springer , Lecture Notes in Computer Science 12479, 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 , pages 343-363, Springer , 2020.
Modelling and Implementation of Unmanned Aircraft Collision Avoidance , Feng, W.; Huang, C.-C.; Turrini, A. and Li, Y.
In SETTA , pages 52-69, Springer , Lecture Notes in Computer Science 12153, 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 , pages 1635-1639, ACM , 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 IEEE Trans. Software Eng. , 48: 1545-1559, 2020.
Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling , Li, Y.; Turrini, A.; Sun, X. and Zhang, L.
In ATVA , pages 467-483, Springer , LNCS 12302, 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, Springer , 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 Inf. Comput. , 262: 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, ijcai.org , 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 , pages 447-451, Springer , LNCS 10806, 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. Comput. , 28: 1011-1030, 2018.
Learning Büchi Automata and Its Applications , Li, Y.; Turrini, A.; Chen, Y.-F. and Zhang, L.
In Engineering Trustworthy Software Systems - 4th International School,
SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures , pages 38-98, Springer , Lecture Notes in Computer Science 11430, 2018.
Learning to Complement Büchi Automata , Li, Y.; Turrini, A.; Zhang, L. and Schewe, S.
In VMCAI , pages 313-335, Springer , 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 Aspects 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 Informatica , 55: 461-488, 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, Schloss Dagstuhl - Leibniz-Zentrum für Informatik , 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 Markov Decision Processes , 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 , pages 41-50, IEEE Computer Society , 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.