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

DOI10.1145/2461328.2461370MaRDI QIDQ2986932zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Vinayak S. Prabhu

Publication date 16 May 2017

Published in Proceedings of the 16th international conference on Hybrid systems: computation and control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1212.6556

zbMATH Keywords

approximation theoriesgraph gamesquantitative simulation relationsrobustnesstimed automata

Mathematics Subject Classification ID

Distributed systems (68M14) Formal languages and automata (68Q45) Games involving graphs (91A43) Applications of game theory (91A80)

Abstract: We introduce quantatitive timed refinement and timed simulation (directed) metrics, incorporating zenoness check s, for timed systems. These metrics assign positive real numbers between zero and infinity which quantify the emph{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 emph{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.

Recommendations

• Quantitative Temporal Simulation and Refinement Distances for Timed Systems
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Parametric timing analysis for real-time systems
• Analysis and verification of real-time systems using quantitative symbolic algorithms
• Timing parameter characterization of real-time systems
• Specification and timing analysis of real-time systems

Cites work

• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A note on two problems in connexion with graphs
• Controlling a Class of Nonlinear Systems on Rectangles
• Diagnostic Information for Realizability
• Enhancing model checking in verification by AI techniques
• scientific article; zbMATH DE number 5595151 (Why is no real title available?)
• scientific article; zbMATH DE number 2080065 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Markov decision processes and regular events
• Model repair for probabilistic systems
• Receding horizon control for temporal logic specifications

Cited in

(5)

• Average-energy games
• Average-energy games
• Theoretical Aspects of Computing – ICTAC 2005
• Formal Modeling and Analysis of Timed Systems
• Numerical coverage estimation for the symbolic simulation of real-time systems

This page was built for publication: Quantitative timed simulation functions and refinement metrics for real-time systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2986932)