[1]王晓燕,韩啸,彭君,等.实时并发系统的PTSL模型检测[J].智能系统学报,2017,12(5):694-701.[doi:10.11992/tis.201706008]
 WANG Xiaoyan,HAN Xiao,PENG Jun,et al.PTSL model checking of timed concurrent system[J].CAAI Transactions on Intelligent Systems,2017,12(5):694-701.[doi:10.11992/tis.201706008]
点击复制

实时并发系统的PTSL模型检测

参考文献/References:
[1] CLARKE E, GRUMBERG O, PELED D. Model Checking[M]. Cambridge:MIT press, 1999:5-60.
[2] BEAUQUIER D. On probabilistic timed automata[J]. Theoretical computer science, 2003, 292(1):65-84.
[3] KWIATKOWSKA M, NORMAN G, SEGALA R, et al. Automatic verification of real-time systems with discrete probability distributions[J]. Theoretical computer science,2002, 282:101-150.
[4] CLARKE E, EMERSON A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Proceedinns of the Workshop Logic of Programs.Newyork, US, 1981:52-71.
[5] HANSSON H, JONSSON B. A logic for reasoning about time and reliability[J]. Formal aspects of computing, 1994, 6(5):512-535.
[6] ALFARO de L. Temporal Logics for the Specification of Performance and Reliability[C]//Proc STACS’97.New York, US, 1997:165-176.
[7] ALUR R, HENZINGER T A, KUPFERMAN O. Alternating-time temporal logic[J]. Journal of the ACM, 2002, 49:672-713.
[8] CHATTERJEE K, HENZINGER T A. Strategy improvement for stochastic Rabin and Strett Games[C]//Proc DBLP 2006. Bonn, Germany, 2006:375-389.
[9] CHATTERJEE K, HENZINGER T A, PITERMAN N. Strategy logic[J]. Information and computation, 2007, 208(6):677-693.
[10] Basset N, Kwiatkowska M, Topcu U, et al. Strategy synthesis for stochastic games with multiple long-run objectives[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany, 2015:256-271.
[11] KRISHNENDU Chatterjee, LUCA de Alfaro, THOMAS A,et al. Strategy improvement for concurrent reachability and turn-based stochastic safety games[J]. Journal of computer and system sciences, 2013, 79:640-657.
[12] ALFARO L de, FAELLA M, HENZINGER T, et al. The element of surprise in timed games[C]//14th International Conference on Concurrency Theory. Marceille, France,2003:144-158.
[13] THOMAS Brihaye, FRAN Cois, LAROUSSINIE, et al. Timed Concurrent Game Structures[C]//Proceedings of the 18th international conference on Concurrency Theory. Lisbon, Portugal, 2007:445-459.
[14] RAJEEV A, THOMAS A, HENZINGER, et al. Alternating-time temporal logic[J]. Journal of the ACM, 2002,49(5):672-713.
[15] CHEN Taolue, LU Jian. Probabilistic alternating-time temporal logic and model checking algorithm[C]//Fourth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD), 2007. Haikou, China, 2007:35-39.
[16] CHRISTEL Baier, TOMÁ? Brázdil, MARCUS Größer, et al. Stochastic game logic[C]//Conference:Quantitative Evaluation of Systems. Edinburgh, UK,2007:227-236.
[17] MARTA Kwiatkowska A, GETHIN Norman A, JEREMY Sproston B, et al. Symbolic model checking for probabilistic timed automata[J]. Information and computation, 2007, 205(2):1027-1077.
[18] MARTA Kwiatkowska, GETHIN Norman, DAVID Parker, et al. Performance analysis of probabilistic timed automata using digital clocks[J]. Formal methods in system design, 2006, 29(1):33-78.
相似文献/References:
[1]朱创营,常亮,徐周波,等.含有合取查询的时态描述逻辑ALC-LTL模型检测[J].智能系统学报,2014,9(6):714.[doi:10.3969/j.issn.1673-4785.201303034]
 ZHU Chuangying,CHANG Liang,XU Zhoubo,et al.Research on the model checking of temporal description logic ALC-LTL containing conjunctive query[J].CAAI Transactions on Intelligent Systems,2014,9():714.[doi:10.3969/j.issn.1673-4785.201303034]

备注/Memo

收稿日期:2017-06-05。
基金项目:国家自然科学基金项目(61502196).
作者简介:王晓燕,女,1977年生,讲师,博士,主要研究方向为软件建模与验证技术、软件开发新方法。申请发明专利2项,并获得2010年中国国家专利优秀奖,2008年吉林省科技进步一等奖,中国商业科技进步二等奖。发表论文20余篇,其中被SCI收录5篇;韩啸,男,1981年生,编辑,博士研究生,主要研究方向为网络协同、软件建模和网络技术;彭君,男,1981年生,讲师,博士,主要研究方向为模型驱动技术、构件技术、软件体系结构。
通讯作者:王晓燕.E-mail:wangxy@jlu.edu.cn

更新日期/Last Update: 2017-10-25
Copyright © 《 智能系统学报》 编辑部
地址:(150001)黑龙江省哈尔滨市南岗区南通大街145-1号楼 电话:0451- 82534001、82518134 邮箱:tis@vip.sina.com