李广元

 

中国科学院 软件研究所 计算机科学国家重点实验室

北京市海淀区中关村南四街4号软件园区5号楼3层

电话：010-62661628

研究兴趣：形式化方法，时序逻辑，时间自动机，实时系统的模型检测工具

 

 

LI Guangyuan                                                

image002Research Professor

State Key Laboratory of Computer Science

Institute of Software, Chinese Academy of Sciences  

P.O.Box 8718

Beijing, 100190

P.R. of China

Tel: +86 10 62661628
Fax: +86 10 62661627

Email: ligy (at) ios.ac.cn

Research Interests

Formal Methods; Temporal Logic; Timed Automata; Model Checking Tools for Real-Time Systems.

 

Model Checking Tools

CTAV 2.0:  Model Checking Metric Temporal Logic MTL0,∞ for Timed Büchi Automata

CASAAL:  Translating Metric Temporal logic MTL0,∞ into Timed Büchi Automata

Publications (DBLP)

1.         Hector M. Chavez, Wuwei Shen, Robert B. France, Benjamin A. Mechling, and Guangyuan Li: An Approach to Checking Consistency between UML Class Model and Its Java Implementation, IEEE Transactions on Software Engineering, 42(4), pp322-344,2016.

2.         Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, Lijun Zhang: Lazy Probabilistic Model Checking without Determinisation. 26th International Conference on Concurrency Theory (CONCUR 2015), pp354-367, 2015.

3.         Peter Bulychev, Alexandre David, Kim G. Larsen, Guangyuan Li: Efficient controller synthesis for a fragment of MTL0,∞.  Acta Informatica, Vol. 51, Issue 3, pp.165-192, DOI 10.1007/s00236-013-0189-z, Springer, 2014.

4.         Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny B. Poulsen：Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata. 14th International Conference on Application of Concurrency to System Design (ACSD 2014), pp.32-41, 2014.

5.         Gaogao Yan, Xue-Yang Zhu, Rongjie Yan and Guangyuan Li: Formal Throughput and Response Time Analysis of MARTE Models. 16th International Conference on Formal Engineering Methods (ICFEM 2014), LNCS 8829, pp.430-445, 2014.

6.         Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny B. Poulsen: Rewrite-Based Statistical Model Checking of WMTL. 3rd International Conference on Runtime Verification (RV 2012), LNCS 7687, pp.260-275, 2013.

7.         Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny B. Poulsen, Amelie Stainer: Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), LNCS 7180, pp. 168-182, 2012.

8.         Guangyuan Li: Checking Timed Büchi Automata Emptiness Using LU-Abstractions. Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2009), LNCS 5813, pp. 228-242, Springer, 2009.

9.         Yan Rongjie, Li Guangyuan, Zhang Wenliang and Peng Yunquan: Improvements for the Symbolic Verification of Timed Automata, Proceedings of the 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems ( FORTE 2007), LNCS 4574, pp.196--210, Springer, 2007. 

10.     Yan Rongjie, Li Guangyuan, Xu Yubo, Liu Chunming and Tang Zhisong: Reachability checking of finite precision timed automata(in Chinese), Journal of Software, 17(1):1-10, 2006. 

11.     Li Liang, Ma Huadong and Li Guangyuan: Formal Specification and Model Checking of CSMA/CA Using Finite Precision Timed Automata, The Journal of China Universities of Posts and Telecommunications, 12(3), 33-38,2005.

12.     Yan Rongjie, Li Guangyuan and Tang Zhisong: Symobolic Model Checking of Finite Precision Timed Automata, Proceedings of the Second International Colloquium on Theoretical Aspects of Computing(ICTAC’05), LNCS 3722, pp.272--287, Springer, 2005.

13.     Li Guangyuan and Tang Zhisong: Translating a Continuous-Time Temporal Logic into Timed Automata, Proceedings of the first Asian Symposium on Programming Languages and Systems (APLAS 2003), LNCS 2895, pp.322--338, Springer, 2003.

14.      Li Guangyuan and Tang Zhisong: Representing and Verifying Reactive Systems with Continuous-Time Temporal Logic (in Chinese), Chinese Journal of Computers, Vol.26, No.11, 1424--1434, 2003.

15.      Li Guangyuan and Tang Zhisong: Modeling Real-Time Systems with Continuous-Time Temporal Logic, Proceedings of the 4th International Conference on Formal Engineering Methods (ICFEM 2002), LNCS 2495, pp.231--236, Springer, 2002.

16.      Li Guangyuan and Tang Zhisong: A Linear Temporal Logic with Clocks for Verification of Real-Time Systems (in Chinese). Journal of Software, Vol.13, No.1, 33--41, 2002.

17.      Li Guangyuan and Tang Zhisong: Model Checking of Real-Time Systems in Linear Temporal Logic with Clocks (in Chinese), Journal of Software, Vol.13, No.2, 193--201, 2002.

18.      Li Guangyuan and Tang Zhisong: A Linear Temporal Logic with Continuous Semantics for Hybrid Systems. Proceedings of the International Conference on Software: Theory and Practice (ICS'2000)/ the 16th IFIP World Computer Congress, 395--402, Beijing, August, 2000.

19.      Li Guangyuan and Tang Zhisong: Formalization and Verification of Pointers in the Temporal Logic Language XYZ/E Programs. Journal of Software, Vol.11, No.3, 285--292, 2000.

20.      Li Guangyuan and Tang Zhisong: The Composability Problem of the Semantics of XYZ/BE-Communicating Processes. Systems Science and Mathematical Sciences, Vol.12, Suppl. 61--69, May, 1999.

21.      Li Xiang, Li Guangyuan and Song Ronggong: A Programming Version of Blum-Shub-Smale Machine and R.E. Sets of Real Number. Chinese Journal of Advanced Software Research,  Vol.5, No 2, 133--139, 1998.

22.      Li Guangyuan and Li Xiang: Nonmonotonic Belief Logic NBL and Semantics of Logic Programs. Chinese Journal of Advanced Software Research, Vol.4, No 3, 239--246, 1997.

23.      Li Guangyuan, Fu Jizhong, Li Xiang and Long Sigong: A Local Search Algorithm with Heuristic Information for SAT Problems (in Chinese). Tech Rep. No. ISCAS-LCS-96-3, Laboratory of computer science, Institute of software, Chinese Academy of Sciences, 1996.

24.      Li Xiang, Li Guangyuan and Song Ronggong: The Study on the Computation Theory over Ordered Rings and Fields (Abstract) . Notices, AMS, 11,1995.

25.      Li Guangyuan: Nonmonotonic Belief Logic NBL and Default Logic (in Chinese). In: "Proceedings of CAAI'94, Hangzhou, November, 1994", Zhejiang University Press, 1994.

26.      Li Xiang and Li Guangyuan: On the Relationships between Approximate and Probabilistic Complexity Classes. Science in China, Vol.37, No.2, 247--256, 1994.

27.      Li Xiang and Li Guangyuan: A 3-values Logic with Strong and Weak Negations (in Chinese). Chinese Theoretical Computer Science, Vol 2, 65--82, 1994.

28.      Li Guangyuan：Some Model-theoretic Results for Three-valued Logic TL. In "Chinese Annals of Pure & Applied Logic,1(1989), edited by Zhang Jinwen ", Peking University Press, 1992.

29.      Li Xiang and Li Guangyuan: Medium Logic and Woodruff's Three-Valued Logic. Chinese Science Bulletin, Vol. 35, 8, 622--626, 1990

30.      Li Guangyuan and Li Xiang: Soundness and Completeness for "Medium Logic" ME* (in Chinese). Journal of Guizhou University ( Natural Science), Vol.6, No.4, 193--200, 1989.

31.      Li Xiang and Li Guangyuan: The Characterization Theorems of "Medium Logic" (in Chinese). Kexue Tongbao (Science Bulletin), Vol.33, No.22, 1686--1689, 1988.

PhD Thesis

   LTLC: A Continuous-Time Temporal Logic for Real-Time and Hybrid Systems (in Chinese).  Institute of Software, Chinese Academy of Sciences, 2001.  [ paper.pdf ]