Current Students

  • Teng Long:
  • Lanlan Zhang:

    Former Students

  • (2007) Jin Yi: State Space Reduction of Buchi Automata
  • (2007) Zhilin Wu: On the theoretical Aspects of Temporal Logics: Expressive Power and Complexity
  • (2008) Syed Asad Raza Kazmi: Intuitionistic Linear-time mu-Calculus
  • (2009) Hongtao Huang: Predicate Detection under Definitely Modality in Distributed Systems
  • (2009) Xiang Zhou: Expressive Power of Logics on Special Classes of Finite Structures
  • (2009) Yanyan Xu: BDD-based Incremental Heuristic Search and Its Applications
  • (2009) Liang Xu: Bounded Model Checking and Its Applications
  • (2010) Wei Chen: Problems in Satisability Solving and Applications in Model Checking
  • (2009) Jinxiu Du: 基于SAT的LTL限界模型检测与验证
  • (2009) Weisong Li: 弱互模拟等价类算法改进
  • (2009) Qingkui Feng: 基于一阶迁移系统的限界模型检测工具实现
  • (2009) Xiaoliang Wang: 基于Yices对时间自动机的有界模型检测
  • (2010) Shaochun Wang: 卫命令模型检测工具的设计与实现
    Papers

    Shaochun Wang. Temporal Filter: A Temporal Extension to Wireshark Display Filter (Short paper). SEKE 2010.

    Yanyan Xu, Weiya Yue, Kaile Su. The BDD-Based Dynamic A* Algorithm for Real-Time Replanning. LNCS 5598 (FAW 2009):271-282.

    Yanyan Xu and Weiya Yue. A generalized framework for BDD-based replanning A* search. SNPD 2009:133-139.

    Xiang Zhou. CFI Construction and Balanced Graphs. LNCS 5598 (FAW 2009): 97-107.

    Weisong Li. Algorithms for Computing Weak Bisimulation Equivalence. TASE 2009:241:248.

    Hongtao Huang. On Detecting of Regular Predicates in Distributed Systems. LNCS 5799 (ATVA 2009):397-411.

    Hongtao Huang. Detection of a Set of States in Distributed Systems. APSEC 2008:281-288. 2008.

    Xiang Zhou. Ehrenfeucht-Fraisse Games in Finite Set Theory. Information Processing Letters 108:3-9. 2008.

    Liang Xu. SMT-Based Bounded Model Checking for Real-Time Systems (Short Paper). QSIC 2008:120-125. 2008.

    Hongtao Huang. Detection of Disjunctive Normal Form Predicate in Distributed Systems. ICDCN 2008:158-169. 2008.

    Zhilin Wu. On the Expressive Power of QLTL. ICTAC 2007:467-481. 2007.

    Zhilin Wu. A note on the characterization of TL[EF]*. Information Processing Letters 102(2-3):48-54, 2007.

    Weiya Yue, Yanyan Xu, Kaile Su. BDDRPA*: An efficient BDD-based incremental heuristic search algorithm for replanning. LNAI 4304 (AI 2006):627-636. 2006.

    Zhilin Wu. Quasi-star-free languagaes on infinite words, Acta Cybernetica 17(1):75-93, 2005.