教授 博士生导师
招生学科专业:
计算机科学与技术 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院
软件工程 -- 【招收硕士研究生】 -- 计算机科学与技术学院
电子信息 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院
性别:男
学历:清华大学
学位:工学博士学位
所在单位:计算机科学与技术学院/人工智能学院/软件学院
联系方式:13814535662
电子邮箱:
最后更新时间:..
点击次数:
所属单位:计算机科学与技术学院/人工智能学院/软件学院
发表刊物:2017 12TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (IEEE ISKE)
关键字:probabilistic timed automata model checking and stochastic timed logic
摘要:At present, there are various logics used to describe properties of continue-time systems, such as TCTL (timed computation tree logic) and RTCTL (rewards timed computation tree logic), and of continue-time stochastic systems, such as CSL (continuous stochastic logic) and PTCTL (probabilistic timed computation tree logic). When assigned on the systems, these logics are limited to returning only true or false. In order to establish the correctness and the performance of a system one needs a unified framework for expressing the system, and a unified logic for expressing the desired specification. In this word, we propose a new formal specification TCTML (timed computation tree measurement language) to check the correctness and evaluate the performance of a system, which operates on real values to reason over probabilistic continue-time systems. Retaining the conventional semantics of temporal logics, it extends weak until and until with arithmetic operations on real-valued quantities. Moreover, the algorithms of CTML model checking PTAs (probabilistic timed automata) is given and a concrete example is used to demonstrate that it is feasible and effective.
是否译文:否
发表时间:2017-01-01
合写作者:Ma, Yan,Liu, Yang
通讯作者:曹子宁