Time-Bounded Verification of CTMCs against Real-Time Specifications
作者： Taolue Chen , Marco Diciolla , Marta Kwiatkowska , Alexandru Mereacre
DOI: 10.1007/978-3-642-24310-3_4
关键词: Timed automaton 、 Discrete mathematics 、 Pointwise 、 Bounded function 、 Approximation algorithm 、 Metric (mathematics) 、 Interval (mathematics) 、 Markov chain 、 Mathematics 、 Path (graph theory)
摘要: In this paper we study time-bounded verification of a finite continuous-time Markov chain (CTMC) C against real-time specification, provided either as metric temporal logic (MTL) property φ, or timed automaton (TA) A. The key question is: what is the probability set paths that satisfy φ (or are accepted by A) over time interval fixed, bounded length? We provide approximation algorithms to solve these problems. first derive bound N such with at most discrete jumps sufficient approximate desired up e. Then, for each (untimed) path σ length N, generate constraints variables determining residence state along σ, depending on realtime specification under consideration. paths, determined and associated constraints, can thus be formulated multidimensional integral. Summing all probabilities yields result. For MTL, consider both continuous pointwise semantics. differ mainly in generation two types specifications.
springer.com
sci-hub.st 参考文章(45)
Moshe Y. Vardi, Pierre Wolper, An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) logic in computer science. pp. 332- 344 ,(1986)
Gianluigi Zavattaro, Mario Bravetti, Concur 2009 - Concurrency Theory ,(2009)
Joël Ouaknine, James Worrell, Towards a Theory of Time-Bounded Verification Automata, Languages and Programming. pp. 22- 37 ,(2010) , 10.1007/978-3-642-14162-1_3
Wiley‐Interscience Series in Discrete Mathematics and Optimization John Wiley & Sons, Inc.. pp. 335- 336 ,(2011) , 10.1002/9781118032718.SCARD
Joël Ouaknine, Alexander Rabinovich, James Worrell, Time-Bounded Verification international conference on concurrency theory. pp. 496- 510 ,(2009) , 10.1007/978-3-642-04081-8_33
Orna Kupferman, Moshe Y. Vardi, Model Checking of Safety Properties formal methods. ,vol. 19, pp. 291- 314 ,(2001) , 10.1023/A:1011254632723
S. Blum, L., Cucker, F., Shub, M., Smale, Complexity and Real Computation ,(1997)
Jean-Baptiste Hiriart-Urruty, Claude Lemaréchal, Convex analysis and minimization algorithms ,(1993)
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Dejan Ničković, Nir Piterman, From MTL to deterministic timed automata formal modeling and analysis of timed systems. ,vol. 6246, pp. 152- 167 ,(2010) , 10.1007/978-3-642-15297-9_13