English 
曹子宁

教授 博士生导师

招生学科专业:
计算机科学与技术 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院
软件工程 -- 【招收硕士研究生】 -- 计算机科学与技术学院
电子信息 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院

性别:男

学历:清华大学

学位:工学博士学位

所在单位:计算机科学与技术学院/人工智能学院/软件学院

联系方式:13814535662

电子邮箱:

手机版

访问量:

最后更新时间:..

当前位置: 中文主页 >> 科学研究 >> 论文成果
A Specification with Performance Evaluation for Probabilistic Timed Automata

点击次数:

所属单位:计算机科学与技术学院/人工智能学院/软件学院

发表刊物: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

通讯作者:曹子宁

版权所有©2018- 南京航空航天大学·信息化处(信息化技术中心)