Trustworthy Intelligent Systems

TIS's Publications

These are all the publications published by members of the TIS group.

2024

  • Yi Dong, Ronghui Mu, Gaojie Jin (), Yi Qi, Jinwei Hu, Xingyu Zhao, Jie Meng, Wenjie Ruan, Xiaowei Huang (): Position: Building Guardrails for Large Language Models Requires Systematic Design. In Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024, 2024. URL BIB
  • Suguman Bansal, Yash Kankariya, Yong Li: DAG-Based Compositional Approaches for LTLf to DFA Conversions. In Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design - FMCAD 2024, pages 227-235, 2024. DOI
  • Daniele Dell'Erba, Yong Li, Sven Schewe (): DFAMiner: Mining Minimal Separating DFAs from Labelled Samples. In Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, volume 14934 of Lecture Notes in Computer Science, pages 48-66, 2024. DOI BIB
  • Weizhi Feng, Yicheng Liu, Jiaxiang Liu, David N. Jansen (), Lijun Zhang, Zhilin Wu (): Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. In 61st ACM/IEEE Design Automation Conference, DAC 2024, San Francisco, CA, USA, June 23-27, 2024, 2024.
  • Song Gao, Bohua Zhan (), Zhilin Wu (), Lijun Zhang: Verifying Randomized Consensus Protocols with Common Coins. In 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2024, Brisbane, Australia, June 24-27, 2024, pages 403-415, 2024. DOI BIB
  • Ji Guan, Yuan Feng (), Andrea Turrini, Mingsheng Ying: Measurement-based Verification of Quantum Markov Chains. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, volume 14683 of Lecture Notes in Computer Science, pages 533-554, 2024. DOI BIB
  • Renjue Li, Tianhang Qin, Cas Widdershoven: ISS-Scenario: Scenario-based Testing in CARLA. In Theoretical Aspects of Software Engineering - 18th International Symposium, TASE 2024, Guiyang, China, July 29 - August 1, 2024, Proceedings, volume 14777 of Lecture Notes in Computer Science, pages 279-286, 2024. DOI BIB
  • Yong Li, Sven Schewe (), Qiyi Tang: Angluin-Style Learning of Deterministic Büchi and Co-Büchi Automata. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, August 03-09, 2024, Jeju, Republic of Korea, 2024.
  • Yong Li, Sven Schewe (), Moshe Y. Vardi (): Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata. In Theor. Comput. Sci. 1006:114650, 2024. DOI BIB
  • Tao Lin, Lijia Yu, Gaojie Jin (), Renjue Li, Peng Wu, Lijun Zhang: Out-of-Bounding-Box Triggers: A Stealthy Approach to Cheat Object Detectors. In Computer Vision - ECCV 2024 - 18th European Conference, Milan, Italy, September 29-October 4, 2024, Proceedings, Part LXVI, volume 15124 of Lecture Notes in Computer Science, pages 269-287, 2024. DOI BIB
  • Zongxin Liu, Pengfei Yang, Lijun Zhang, Xiaowei Huang (): DeepCDCL: A CDCL-based Neural Network Verification Framework. In Theoretical Aspects of Software Engineering - 18th International Symposium, TASE 2024, Guiyang, China, July 29 - August 1, 2024, Proceedings, volume 14777 of Lecture Notes in Computer Science, pages 343-355, 2024. DOI BIB
  • Yibo Miao, Yinpeng Dong, Jinlai Zhang, Lijia Yu, Xiao Yang, Xiao-Shan Gao: Improving Robustness of 3D Point Cloud Recognition from a Fourier Perspective. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, NeurIPS 2024, Vancouver, Canada, December 10-15, 2024, 2024.
  • Shidong Shen, Yicheng Liu, Lijun Zhang, Fu Song (), Zhilin Wu (): Formal Verification of RISC-V Processor Chisel Designs. In Dependable Software Engineering. Theories, Tools, and Applications - 10th International Symposium, SETTA 2024, Hong Kong, China, November 26-28, 2024, Proceedings, volume 15469 of Lecture Notes in Computer Science, pages 142-160, 2024. DOI
  • Deqian Yang, Hui Meng, Haochen Zhao, Gaojie Jin (), Lijun Zhang: Class-aware Cross Pseudo Supervision Framework for Semi-Supervised Multi-Organ Segmentation in Abdominal CT Scans. In Patter Recognition and Computer Vision - 7th Chinese Conference, PRCV 2024, 2024. BIB
  • Lijia Yu, Xiao-Shan Gao, Lijun Zhang: Optimal Robust Memorization with ReLU Neural Networks. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024, 2024. URL BIB
  • Lijia Yu, Shuang Liu, Yibo Miao, Lijun Zhang, Xiaoshan Gao: Generalization Bound and New Algorithm for Clean-Label Backdoor Attack. In Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024, 2024. URL BIB
  • Lijia Yu, Yibo Miao, Lijun Zhang, Xiaoshan Gao: Generalizability of Memorization Neural Networks. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, NeurIPS 2024, Vancouver, Canada, December 10-15, 2024, 2024. BIB
  • Hanwei Zhang, Luo Cheng, Qisong He, Wei Huang, Renjue Li, Ronan Sicre, Xiaowei Huang (), Holger Hermanns (), Lijun Zhang: Eidos: Efficient, Imperceptible Adversarial 3D Point Clouds. In SETTA 2024 - Symposium on Dependable Software Engineering Theories, Tools and Applications, Lecture notes in Computer Science, 2024. BIB
  • Yifan Zhu, Lijia Yu, Xiao-Shan Gao: Detection and Defense of Unlearnable Examples. In Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pages 17211-17219, 2024. DOI BIB

2023

  • 刘颖, 杨鹏飞, 张立军, 吴志林 (), 冯元 (): 前馈神经网络和循环神经网络的鲁棒性验证综述. In 软件学报 34(7):3134, 2023. DOI BIB
  • Yu-Fang Chen (), Vojtech Havlena, Ondrej Lengál, Andrea Turrini: A symbolic algorithm for the case-split rule in solving word constraints with extensions. In J. Syst. Softw. 201:111673, 2023. DOI BIB
  • Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: On the power of finite ambiguity in Büchi complementation. In Inf. Comput. 292:105032, 2023. DOI BIB
  • Jianling Fu, Cheng-Chao Huang, Yong Li, Jingyi Mei, Ming Xu, Lijun Zhang: Quantitative controller synthesis for consumption Markov decision processes. In Inf. Process. Lett. 180:106342, 2023. DOI BIB
  • Chen Fu, Andrea Turrini, Xiaowei Huang (), Lei Song, Yuan Feng (), Lijun Zhang: Model Checking for Probabilistic Multiagent Systems. In Journal of Computer Science and Technology 38(4):1-25, 2023. DOI BIB
  • Vojtech Havlena, Ondrej Lengál, Yong Li, Barbora Smahlíková, Andrea Turrini: Modular Mix-and-Match Complementation of Büchi Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 249-270, 2023. DOI BIB
  • Gaojie Jin (), Xinping Yi, Dengyu Wu, Ronghui Mu, Xiaowei Huang (): Randomized Adversarial Training via Taylor Expansion. In IEEE/CVF Conference on Computer Vision and Pattern Recognition, CVPR 2023, Vancouver, BC, Canada, June 17-24, 2023, pages 16447-16457, 2023. DOI BIB
  • Ying Liu, Andrea Turrini, Ernst Moritz Hahn (), Bai Xue (), Lijun Zhang: Scenario Approach for Parametric Markov Models. In Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, volume 14215 of Lecture Notes in Computer Science, pages 158-180, 2023. DOI BIB
  • Depeng Liu, Bow-Yaw Wang, Chen Fu, Lijun Zhang: Model checking differentially private properties. In Theor. Comput. Sci. 943:153-170, 2023. DOI BIB
  • Dejin Ren, Wanli Lu, Jidong Lv, Lijun Zhang, Bai Xue (): Model Predictive Control with Reach-avoid Analysis. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 5437-5445, 2023. DOI BIB
  • Liang Zhang, Nathaniel Xu, Pengfei Yang, Gaojie Jin (), Cheng-Chao Huang, Lijun Zhang: TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models. In IEEE/CVF International Conference on Computer Vision, ICCV 2023, Paris, France, October 1-6, 2023, pages 8293-8305, 2023. DOI BIB

2022

  • Suguman Bansal, Giuseppe De Giacomo, Antonio Di Stasio, Yong Li, Moshe Y. Vardi (), Shufang Zhu: Compositional Safety LTL Synthesis. In Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers, volume 13800 of Lecture Notes in Computer Science, pages 1-19, 2022. DOI BIB
  • Chen Fu, Ernst Moritz Hahn (), Yong Li, Sven Schewe (), Meng Sun (), Andrea Turrini, Lijun Zhang: EPMC Gets Knowledge in Multi-agent Systems. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, volume 13182 of Lecture Notes in Computer Science, pages 93-107, 2022. DOI BIB
  • Cheng-Chao Huang: Explicit Bounds for Linear Forms in the Exponentials of Algebraic Numbers. In ISSAC '22: International Symposium on Symbolic and Algebraic Computation, Villeneuve-d'Ascq, France, July 4 - 7, 2022, pages 371-379, 2022. DOI BIB
  • Gaojie Jin (), Xinping Yi, Pengfei Yang, Lijun Zhang, Sven Schewe (), Xiaowei Huang (): Weight Expansion: A New Perspective on Dropout and Generalization. In Trans. Mach. Learn. Res. 2022, 2022. URL BIB
  • Yi Li, Xie Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang: Synthesizing ranking functions for loop programs via SVM. In Theor. Comput. Sci. 935:1-20, 2022. DOI BIB
  • Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi (), Lijun Zhang: Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 152-173, 2022. DOI BIB
  • Meilun Li, Andrea Turrini, Ernst Moritz Hahn (), Zhikun She, Lijun Zhang: Probabilistic Preference Planning Problem for Markov Decision Processes. In IEEE Trans. Software Eng. 48(5):1545-1559, 2022. DOI BIB
  • Renjue Li, Pengfei Yang, Cheng-Chao Huang, Youcheng Sun, Bai Xue (), Lijun Zhang: Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022, pages 2189-2201, 2022. DOI BIB
  • Depeng Liu, Bow-Yaw Wang, Lijun Zhang: Verifying Pufferfish Privacy in Hidden Markov Models. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, volume 13182 of Lecture Notes in Computer Science, pages 174-196, 2022. DOI BIB
  • Wanwei Liu, Junnan Xu, David N. Jansen (), Andrea Turrini, Lijun Zhang: An Axiom System of Probabilistic Mu-Calculus. In Tsinghua Science and Technology 27(2):372-385, 2022. DOI BIB
  • Moshe Y. Vardi (), Seth Fogarty, Yong Li, Yih-Kuen Tsay (): Towards a Grand Unification of Büchi Complementation Constructions. In Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of Lecture Notes in Computer Science, pages 185-207, 2022. DOI BIB
  • Tomás Vojnar, Lijun Zhang: Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019. In Int. J. Softw. Tools Technol. Transf. 24(1):29-31, 2022. DOI BIB
  • Shizhen Yu, Yifan Dong, Jiuyang Liu, Yong Li, Zhilin Wu (), David N. Jansen (), Lijun Zhang: CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). In Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings, volume 13550 of Lecture Notes in Computer Science, pages 324-331, 2022. DOI BIB

2021

  • Konstantin Kuznetsov, Chen Fu, Song Gao, David N. Jansen (), Lijun Zhang, Andreas Zeller (): Frontmatter: mining Android user interfaces at scale. In ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021, pages 1580-1584, 2021. DOI BIB
  • Song Gao, Bohua Zhan (), Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen (), Lijun Zhang: Formal Verification of Consensus in the Taurus Distributed Database. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 741-751, 2021. DOI BIB
  • Yong Li, Yu-Fang Chen (), Lijun Zhang, Depeng Liu: A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. In Inf. Comput. 281:104678, 2021. DOI BIB
  • Yong Li, Yih-Kuen Tsay (), Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: Congruence Relations for Büchi Automata. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 465-482, 2021. DOI BIB
  • Yong Li, Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: Synthesizing Good-Enough Strategies for LTLf Specifications. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 4144-4151, 2021. DOI BIB
  • Sven Schewe (), Lijun Zhang: Editorial - Special issue on Concurrency Theory (CONCUR 2018). In J. Comput. Syst. Sci. 119:19-20, 2021. DOI BIB
  • Bing Sun, Jun Sun (), Ting Dai, Lijun Zhang: Probabilistic Verification of Neural Networks Against Group Fairness. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 83-102, 2021. DOI BIB
  • Pengfei Yang, Jianlin Li (), Jiangchao Liu, Cheng-Chao Huang, Renjue Li, Liqian Chen, Xiaowei Huang (), Lijun Zhang: Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation. In Formal Aspects Comput. 33(3):407-435, 2021. DOI BIB
  • Pengfei Yang, Renjue Li, Jianlin Li (), Cheng-Chao Huang, Jingyi Wang, Jun Sun (), Bai Xue (), Lijun Zhang: Improving Neural Network Verification through Spurious Region Guided Refinement. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 389-408, 2021. DOI BIB

2020

  • Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang: Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 467-483, 2020. DOI BIB
  • Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi (): Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 9766-9774, 2020. DOI BIB
  • Carlos E. Budde, Arnd Hartmanns (), Michaela Klauck, Jan Kretínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang: On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. In Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV, volume 12479 of Lecture Notes in Computer Science, pages 216-241, 2020. DOI BIB
  • Yu-Fang Chen (), Vojtech Havlena, Ondrej Lengál, Andrea Turrini: A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, volume 12470 of Lecture Notes in Computer Science, pages 343-363, 2020. DOI BIB
  • Weizhi Feng, Cheng-Chao Huang, Andrea Turrini, Yong Li: Modelling and Implementation of Unmanned Aircraft Collision Avoidance. In Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings, volume 12153 of Lecture Notes in Computer Science, pages 52-69, 2020. DOI BIB
  • Gaojie Jin (), Xinping Yi, Liang Zhang, Lijun Zhang, Sven Schewe (), Xiaowei Huang (): How does Weight Correlation Affect Generalisation Ability of Deep Neural Networks?. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020. URL BIB
  • Renjue Li, Jianlin Li (), Cheng-Chao Huang, Pengfei Yang, Xiaowei Huang (), Lijun Zhang, Bai Xue (), Holger Hermanns (): PRODeep: a platform for robustness verification of deep neural networks. 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, 2020. DOI BIB
  • Xie Li, Yi Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang: SVMRanker: a general termination analysis framework of loop programs via SVM. 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 1635-1639, 2020. DOI BIB
  • Yong Li, Moshe Y. Vardi (), Lijun Zhang: On the Power of Unambiguity in Büchi Complementation. In Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, volume 326 of EPTCS, pages 182-198, 2020. DOI BIB

2019

  • Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Morteza Lahijanian, Andrea Turrini: Interval Markov Decision Processes with Multiple Objectives: From Robust Strategies to Pareto Curves. In ACM Trans. Model. Comput. Simul. 29(4):27:1-27:31, 2019. DOI BIB
  • Jianlin Li (), Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang (), Lijun Zhang: Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification. In Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science, pages 296-319, 2019. DOI BIB
  • Yi Li, Xuechao Sun, Yong Li, Andrea Turrini, Lijun Zhang: Synthesizing Nested Ranking Functions for Loop Programs via SVM. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, volume 11852 of Lecture Notes in Computer Science, pages 438-454, 2019. DOI BIB
  • Yong Li, Xuechao Sun, Andrea Turrini, Yu-Fang Chen (), Junnan Xu: ROLL 1.0: ω-Regular Language Learning Library. In 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, volume 11427 of Lecture Notes in Computer Science, pages 365-371, 2019. DOI BIB
  • Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang, Moshe Y. Vardi (): SAT-based explicit LTL reasoning and its application to satisfiability checking. In Formal Methods Syst. Des. 54(2):164-190, 2019. DOI BIB
  • Junnan Xu, Wanwei Liu, David N. Jansen (), Lijun Zhang: An Axiomatisation of the Probabilistic μ-Calculus. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, volume 11852 of Lecture Notes in Computer Science, pages 420-437, 2019. DOI BIB

2018

  • Yu-Fang Chen (), Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang: Advanced automata-based algorithms for program termination checking. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 135-150, 2018. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Johann Schuster, Andrea Turrini, Lijun Zhang: The quest for minimal quotients for probabilistic and Markov automata. In Inf. Comput. 262:162-186, 2018. DOI BIB
  • Bernd Finkbeiner, Geguang Pu, Lijun Zhang: Preface for the special issue for ATVA 2015. In Acta Informatica 55(8):625-626, 2018. DOI BIB
  • Chen Fu, Andrea Turrini, Xiaowei Huang (), Lei Song, Yuan Feng (), Lijun Zhang: Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 4757-4763, 2018. DOI BIB
  • Matthias Heizmann, Yu-Fang Chen (), Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pages 447-451, 2018. DOI BIB
  • Yongjian Li, Kaiqiang Duan, David N. Jansen (), Jun Pang, Lijun Zhang, Yi Lv, Shaowei Cai: An Automatic Proving Approach to Parameterized Verification. In ACM Trans. Comput. Log. 19(4):27:1-27:25, 2018. DOI BIB
  • Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi (), Jifeng He: Accelerating LTL satisfiability checking by SAT solvers. In J. Log. Comput. 28(6):1011-1030, 2018. DOI BIB
  • Yong Li, Andrea Turrini, Yu-Fang Chen (), Lijun Zhang: Learning Büchi Automata and Its Applications. In Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, volume 11430 of Lecture Notes in Computer Science, pages 38-98, 2018. DOI BIB
  • Yong Li, Andrea Turrini, Lijun Zhang, Sven Schewe (): Learning to Complement Büchi Automata. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 of Lecture Notes in Computer Science, pages 313-335, 2018. DOI BIB
  • Jianwen Li, Lijun Zhang, Shufang Zhu, Geguang Pu, Moshe Y. Vardi (), Jifeng He: An explicit transition system construction approach to LTL satisfiability checking. In Formal Aspects Comput. 30(2):193-217, 2018. DOI BIB
  • Depeng Liu, Bow-Yaw Wang, Lijun Zhang: Model Checking Differentially Private Properties. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 394-414, 2018. DOI BIB
  • Lijun Zhang, Pengfei Yang, Lei Song, Holger Hermanns (), Christian Eisentraut, David N. Jansen (), Jens Chr. Godskesen: Probabilistic bisimulation for realistic schedulers. In Acta Informatica 55(6):461-488, 2018. DOI BIB

2017

  • Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn (), Arnd Hartmanns (), Sebastian Junges (), Andrea Turrini: JANI: Quantitative Model and Tool Interaction. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, volume 10206 of Lecture Notes in Computer Science, pages 151-168, 2017. DOI BIB
  • Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Shenggang Ying: Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 35:1-35:16, 2017. DOI BIB
  • Yuan Feng (), Lijun Zhang: Precisely deciding CSL formulas through approximate model checking for CTMCs. In J. Comput. Syst. Sci. 89:361-371, 2017. DOI BIB
  • Yijun Feng, Lijun Zhang, David N. Jansen (), Naijun Zhan (), Bican Xia: Finding Polynomial Loop Invariants for Probabilistic Programs. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 400-416, 2017. DOI BIB
  • Chen Fu, Yuxin Deng (), David N. Jansen (), Lijun Zhang: On Equivalence Checking of Nondeterministic Finite Automata. In Dependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings, volume 10606 of Lecture Notes in Computer Science, pages 216-231, 2017. DOI BIB
  • Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Morteza Lahijanian, Andrea Turrini: Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes. In Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings, volume 10503 of Lecture Notes in Computer Science, pages 207-223, 2017. DOI BIB
  • Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 266-287, 2017. DOI BIB
  • Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn (), Holger Hermanns (), Khaled M. Elbassioni: Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. In Dependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings, volume 10606 of Lecture Notes in Computer Science, pages 25-41, 2017. Best paper. DOI BIB
  • Yong Li, Yu-Fang Chen (), Lijun Zhang, Depeng Liu: A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, volume 10205 of Lecture Notes in Computer Science, pages 208-226, 2017. DOI BIB
  • Shuling Wang, Naijun Zhan (), Lijun Zhang: A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. In Formal Aspects Comput. 29(4):751-775, 2017. DOI BIB
  • Pengfei Yang, David N. Jansen (), Lijun Zhang: Distribution-Based Bisimulation for Labelled Markov Processes. In Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings, volume 10419 of Lecture Notes in Computer Science, pages 170-186, 2017. DOI BIB

2016

  • John Fearnley, Markus N. Rabe, Sven Schewe (), Lijun Zhang: Efficient approximation of optimal control for continuous-time Markov games. In Inf. Comput. 247:106-129, 2016. DOI BIB
  • Luis María Ferrer Fioriti, Vahid Hashemi, Holger Hermanns (), Andrea Turrini: Deciding probabilistic automata weak bisimulation: theory and practice. In Formal Aspects Comput. 28(1):109-143, 2016. DOI BIB
  • Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Andrea Turrini: Exploiting Robust Optimization for Interval Probabilistic Bisimulation. In Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings, volume 9826 of Lecture Notes in Computer Science, pages 55-71, 2016. DOI BIB
  • Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 291-311, 2016. DOI BIB
  • Vahid Hashemi, Holger Hermanns (), Lei Song, K. Subramani, Andrea Turrini, Piotr Wojciechowski: Compositional Bisimulation Minimization for Interval Markov Decision Processes. In Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 114-126, 2016. DOI BIB
  • Fei He (), Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, Lijun Zhang: Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. In ACM Trans. Softw. Eng. Methodol. 25(3):21:1-21:39, 2016. DOI BIB
  • Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn (), Lijun Zhang: An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. In Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings, volume 9984 of Lecture Notes in Computer Science, pages 280-296, 2016. DOI BIB
  • Yong Li, Lei Song, Yuan Feng (), Lijun Zhang: Verify LTL with Fairness Assumptions Efficiently. In 23rd International Symposium on Temporal Representation and Reasoning, TIME 2016, Kongens Lyngby, Denmark, October 17-19, 2016, pages 41-50, 2016. DOI BIB
  • Zhimin Wu, Ernst Moritz Hahn (), Akin Günay, Lijun Zhang, Yang Liu: GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs. In ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016),, volume 285 of Frontiers in Artificial Intelligence and Applications, pages 1726-1727, 2016. DOI BIB
  • Ming Xu, Lijun Zhang, David N. Jansen (), Huibiao Zhu, Zongyuan Yang: Multiphase until formulas over Markov reward models: An algebraic approach. In Theor. Comput. Sci. 611:116-135, 2016. DOI BIB
  • Lijun Zhang, David N. Jansen (): A space-efficient simulation algorithm on probabilistic automata. In Inf. Comput. 249:138-159, 2016. DOI BIB

2015

  • Yu-Fang Chen (), Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang: Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 658-674, 2015. DOI BIB
  • Tom van Dijk (), Ernst Moritz Hahn (), David N. Jansen (), Yong Li, Thomas Neele (), Mariëlle Stoelinga (), Andrea Turrini, Lijun Zhang: A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 35-51, 2015. DOI BIB
  • Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns (), Lei Song, Lijun Zhang: Probabilistic Bisimulation for Realistic Schedulers. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 248-264, 2015. DOI BIB
  • Yuan Feng (), Lijun Zhang: A nearly optimal upper bound for the self-stabilization time in Herman's algorithm. In Distributed Comput. 28(4):233-244, 2015. DOI BIB
  • Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Lijun Zhang: QPMC: A Model Checker for Quantum Programs and Protocols. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 265-272, 2015. DOI BIB
  • Ernst Moritz Hahn (), Guangyuan Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 354-367, 2015. DOI BIB
  • Fei He (), Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang: Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 503-514, 2015. DOI BIB
  • Meilun Li, Zhikun She, Andrea Turrini, Lijun Zhang: Preference Planning for Markov Decision Processes. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA, pages 3313-3319, 2015. DOI BIB
  • Wanwei Liu, Lei Song, Ji Wang, Lijun Zhang: A Simple Probabilistic Extension of Modal Mu-calculus. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 882-888, 2015. URL BIB
  • Yu Peng, Shuling Wang, Naijun Zhan (), Lijun Zhang: Extending Hybrid CSP with Probability and Stochasticity. In Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 87-102, 2015. DOI BIB
  • Lei Song, Yuan Feng (), Lijun Zhang: Decentralized Bisimulation for Multiagent Systems. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015, pages 209-217, 2015. URL BIB
  • Lei Song, Yuan Feng (), Lijun Zhang: Planning for Stochastic Games with Co-Safe Objectives. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 1682-1688, 2015. URL BIB
  • Andrea Turrini, Holger Hermanns (): Polynomial time decision algorithms for probabilistic automata. In Inf. Comput. 244:134-171, 2015. DOI BIB

2014

  • Yuan Feng (), Lijun Zhang: A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 342-356, 2014. DOI BIB
  • Yuan Feng (), Lijun Zhang: When Equivalence and Bisimulation Join Forces in Probabilistic Automata. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 247-262, 2014. DOI BIB
  • Ernst Moritz Hahn (), Yi Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: IscasMc: A Web-Based Probabilistic Model Checker. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 312-317, 2014. DOI BIB
  • Joost-Pieter Katoen (), Lei Song, Lijun Zhang: 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 '14, Vienna, Austria, July 14 - 18, 2014, pages 55:1-55:10, 2014. DOI BIB
  • Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi (), Jifeng He: LTLf Satisfiability Checking. In ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), volume 263 of Frontiers in Artificial Intelligence and Applications, pages 513-518, 2014. DOI BIB
  • Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, Jifeng He: Aalta: an LTL satisfiability checker over Infinite/Finite traces. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014, pages 731-734, 2014. DOI BIB
  • Lei Song, Lijun Zhang, Jens Chr. Godskesen: Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, volume 8318 of Lecture Notes in Computer Science, pages 98-117, 2014. DOI BIB
  • Lei Song, Lijun Zhang, Holger Hermanns (), Jens Chr. Godskesen: Incremental Bisimulation Abstraction Refinement. In ACM Trans. Embed. Comput. Syst. 13(4s):142:1-142:23, 2014. DOI BIB
  • Andrea Turrini, Holger Hermanns (): Cost Preserving Bisimulations for Probabilistic Automata. In Log. Methods Comput. Sci. 10(4), 2014. DOI BIB
  • David Spieler, Ernst Moritz Hahn (), Lijun Zhang: Model Checking CSL for Markov Population Models. In Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014, volume 154 of EPTCS, pages 93-107, 2014. DOI BIB

2013

  • Taolue Chen (), Ernst Moritz Hahn (), Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu, Lijun Zhang: Model Repair for Markov Decision Processes. In Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK, pages 85-92, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Joost-Pieter Katoen (), Lijun Zhang: A Semantics for Every GSPN. In Application and Theory of Petri Nets and Concurrency - 34th International Conference, PETRI NETS 2013, Milan, Italy, June 24-28, 2013. Proceedings, volume 7927 of Lecture Notes in Computer Science, pages 90-109, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Julia Krämer, Andrea Turrini, Lijun Zhang: Deciding Bisimilarities on Distributions. In Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8054 of Lecture Notes in Computer Science, pages 72-88, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Johann Schuster, Andrea Turrini, Lijun Zhang: The Quest for Minimal Quotients for Probabilistic Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 16-31, 2013. DOI BIB
  • Yuan Feng (), Lijun Zhang: A tighter bound for the self-stabilization time in Herman's algorithm. In Inf. Process. Lett. 113(13):486-488, 2013. DOI BIB
  • Yang Gao, Ernst Moritz Hahn (), Naijun Zhan (), Lijun Zhang: CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 464-468, 2013. DOI BIB
  • Yang Gao, Ming Xu, Naijun Zhan (), Lijun Zhang: Model checking conditional CSL for continuous-time Markov chains. In Inf. Process. Lett. 113(1-2):44-50, 2013. DOI BIB
  • Vahid Hashemi, Holger Hermanns (), Andrea Turrini: On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation. In Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66, 2013. DOI BIB
  • Holger Hermanns (), Andrea Turrini: Cost Preserving Bisimulations for Probabilistic Automata. In CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 349-363, 2013. DOI BIB
  • David N. Jansen (), Lei Song, Lijun Zhang: Revisiting Weak Simulation for Substochastic Markov Chains. In Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8054 of Lecture Notes in Computer Science, pages 209-224, 2013. DOI BIB
  • Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He, Kim Guldstrand Larsen: 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, volume 8051 of Lecture Notes in Computer Science, pages 256-270, 2013. DOI BIB
  • Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi (), Jifeng He: LTL Satisfiability Checking Revisited. In 2013 20th International Symposium on Temporal Representation and Reasoning, Pensacola, FL, USA, September 26-28, 2013, pages 91-98, 2013. DOI BIB
  • Lei Song, Lijun Zhang, Holger Hermanns (), Jens Chr. Godskesen: Incremental Bisimulation Abstraction Refinement. In 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013, pages 11-20, 2013. DOI BIB
  • Lei Song, Lijun Zhang, Jens Chr. Godskesen: Bisimulations Meet PCTL Equivalences for Probabilistic Automata. In Log. Methods Comput. Sci. 9(2), 2013. DOI BIB