Hits:

Affiliation of Author(s):计算机科学与技术学院/人工智能学院/软件学院

Title of Paper:A Specification with Performance Evaluation for Probabilistic Timed Automata

Journal:2017 12TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (IEEE ISKE)

Key Words:probabilistic timed automata model checking and stochastic timed logic

Abstract: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.

Translation or Not:no

Date of Publication:2017-01-01

Co-author:Ma, Yan,Liu, Yang

Correspondence Author:Cao Zi Ning