Quantitative temporal simulation and refinement distances for timed systems Journal Article

Author(s): Chatterjee, Krishnendu; Prabhu, Vinayak S
Article Title: Quantitative temporal simulation and refinement distances for timed systems
Affiliation IST Austria
Abstract: We introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.
Keywords: Algorithms; Game theory; Automata theory; Two-player games; Time sharing systems; Approximate timed simulation; Degree of accuracy; Limit energy; Quantitative simulation; Temporal simulation; timed simulation metrics; Timed systems
Journal Title: IEEE Transactions on Automatic Control
Volume: 60
Issue 9
ISSN: 0018-9286
Publisher: IEEE  
Date Published: 2015-02-24
Start Page: 2291
End Page: 2306
DOI: 10.1109/TAC.2015.2404612
Notes: This work was supported in part by Austrian Science Fund (FWF) under Grant P23499-N23, FWF NFN under Grant S11407-N23 (RiSE), ERC Start under Grant (279307: Graph Games), FCT under Grant SFRHBPD902672012 and Microsoft faculty fellows award.
Open access: no
IST Austria Authors
Related IST Austria Work