Skip to content

Publications

Jump to bottom
Yi Li edited this page Dec 21, 2016 · 2 revisions

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, LNCS , 2017.

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.
  • 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.
  • 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.
  • Verify LTL with Fairness Assumptions Efficiently, Li, Y.; Song, L.; Feng, Y. and Zhang, L. In TIME, 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.
  • 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.
  • A space-efficient simulation algorithm on probabilistic automata, Zhang, L. and Jansen, D. N. In Inf. Comput., 249: 138-159, 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.
  • 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.

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.
  • 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.
  • 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.
  • Polynomial Time Decision Algorithms for Probabilistic Automata, Turrini, A. and Hermanns, H. In Information and Computation, 244: 134-171, 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.
  • 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 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.
  • 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.
  • 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.
  • 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.

2014

  • Reachability and Reward Checking for Stochastic Timed Automata, Hahn, E. M.; Hartmanns, A. and Hermanns, H. In AVoCS, 2014.
  • Cost Preserving Bisimulations for Probabilistic Automata, Turrini, A. and Hermanns, H. In Logical Methods in Computer Science, 4: 1-58, 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • Model Checking CSL for Markov Population Models, Spieler, D.; Hahn, E. M. and Zhang, L. In QAPL, pages 93-107, 2014.

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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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. On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation, Hashemi, V.; Hermanns, H. and Turrini, A. In ECEASST, 66, 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.

Overview

Clone this wiki locally