Quantitative timed simulation functions and refinement metrics for real-time systems Conference Paper

Author(s): Chatterjee, Krishnendu; Prabhu, Vinayak S
Title: Quantitative timed simulation functions and refinement metrics for real-time systems
Affiliation IST Austria
Abstract: We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the "steady-state" maximum 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 functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, 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 for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions.
Keywords: robustness; Graph games; Approximation theories; Quantitative simulation relations; Timed automata
Conference Title: HSCC: Hybrid Systems - Computation and Control
Conference Dates: April 8-11, 2013
Conference Location: Philadelphia, PA, USA
Publisher: Springer  
Location: New York, NY, USA
Date Published: 2012-04-01
Start Page: 273
End Page: 282
DOI: 10.1145/2461328.2461370
Notes: This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOP-TILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008 (Modeling and control of Networked vehicle systems in persistent autonomous operations); by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start grant (279307: Graph Games); and the Microsoft faculty fellows award
Open access: yes (repository)
IST Austria Authors
Related IST Austria Work