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 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 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 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 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 Verifying Pufferfish Privacy in Hidden Markov Models Liu, D.; Wang, B.-Y. and Zhang, L.
In VMCAI , pages 174-196, Springer 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 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 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 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 Synthesizing Good-Enough Strategies for LTLf Specifications Li, Y.; Turrini, A.; Vardi, M. Y. and Zhang, L.
In IJCAI , pages 4144-4151, ijcai.org 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 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
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 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 Modelling and Implementation of Unmanned Aircraft Collision Avoidance Feng, W.; Huang, C.-C.; Turrini, A. and Li, Y.
In SETTA , pages 52-69, Springer 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Learning to Complement Büchi Automata Li, Y.; Turrini, A.; Zhang, L. and Schewe, S.
In VMCAI , pages 313-335, Springer 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 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 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.