[1]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]
Copy

PTSL model checking of timed concurrent system

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 12 Number of periods: 2017 5 Page number: 694-701 Column: 学术论文—智能系统 Public date: 2017-10-25
Title:
PTSL model checking of timed concurrent system
Author(s):
WANG Xiaoyan1;  HAN Xiao1; 2;  PENG Jun1;  LIU Shufen1
1. College of Computer Science and Technology, Jilin University, Changchun 130012, China;
2. Editorial Office on Journal, Jilin University, Changchun 130012, China
Keywords:
model checking; probabilistic timed concurrent game structure; probabilistic timed strategy logic; probabilistic timed automata; region graph; timed concurrent system; game model
CLC:
TP311
DOI:
10.11992/tis.201706008
Abstract:
With the increased scale and complexity of real-time concurrent software systems, ensuringtheir correctness and reliability has become a matter of urgency. Current model-checking technology uses an automated demonstration algorithm to judgesystem properties, which must include the traversal in the system model and graph-based analysis techniques as well asextensive numerical computations. In this paper, we consider the timed concurrency model as an extension of the concurrent game model (CGS) and addprobability and time properties to propose a new probabilistic timed concurrent game structure (PTCGS). We also propose a new logic language called probabilistic timed strategy logic (PTSL), which uses strategy as the object in the first-order logic to specify the nonzero-sum attributes in a simple and natural way. Lastly, we give an example usingthe ZeroConf protocol to demonstrate the correctness of the PTSL model checking method.
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.
Similar References:

Memo

-

Last Update: 2017-10-25

Copyright © CAAI Transactions on Intelligent Systems