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

Please wait, while we are loading the content...

Least-violating control strategy synthesis with safety rules

Human-inspired control of bipedal robots via control lyapunov functions and quadratic programs

Learning nonlinear hybrid systems: from sparse optimization to support vector regression

On the decidability of stability of hybrid systems

CoSyMA: a tool for controller synthesis using multi-scale abstractions

State estimation for polyhedral hybrid systems and applications to the Godunov scheme

Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets

Pipelining for cyclic control systems

Compositional heterogeneous abstraction

Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems

Specification-guided controller synthesis for linear systems and safe linear-time temporal logic

Limited-information control of hybrid systems via reachable set propagation

Mining requirements from closed-loop control models

Lyapunov analysis of rigid body systems with impacts and friction via sums-of-squares

An aircraft electric power testbed for validating automatically synthesized reactive control protocols

Observer design for a class of piecewise affine hybrid systems

One-shot computation of reachable sets for differential games

Optimal CPU allocation to a set of control tasks with soft real--time execution constraints

Certifying the safe design of a virtual fixture control algorithm for a surgical robot

Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems

Temporal logic model predictive control for discrete-time systems

Resilient synchronization in robust networked multi-agent systems

Hybrid control lyapunov functions for the stabilization of hybridsystems

Towards sensitivity analysis of hybrid systems using simulink

Automated analysis of real-time scheduling using graph games

Tracking differentiable trajectories across polyhedra boundaries

Safe schedulability of bounded-rate multi-mode systems

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

Control design for specifications on stochastic hybrid systems

Iterative temporal motion planning for hybrid systems in partially unknown environments

A toolbox for simulation of hybrid systems in matlab/simulink: hybrid equations (HyEQ) toolbox

Flowpipe approximation and clustering in space-time

Rewarding probabilistic hybrid automata

Stabhyli: a tool for automatic stability verification of non-linear hybrid systems

Bounded model-checking of discrete duration calculus

Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata

Zélus: a synchronous language with ODEs

A stochastic hybrid system model of collective transport in the desert ant aphaenogaster cockerelli

Formal verification of distributed aircraft controllers

A simulink hybrid heart model for quantitative verification of cardiac pacemakers

A partially observable hybrid system model for bipedal locomotion for adapting to terrain variations

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

Content Provider	ACM Digital Library
Author	Chatterjee, Krishnendu Prabhu, Vinayak S.
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.
Starting Page	273
Ending Page	282
Page Count	10
File Format	PDF
ISBN	9781450315678
DOI	10.1145/2461328.2461370
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-04-08
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Graph games Timed automata Quantitative simulation relations Approximation theories Robustness
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

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

Quantitative Temporal Simulation and Refinement Distances for Timed Systems

Robust Synthesis for Real Time Systems

Timed I/O automata: a complete specification theory for real-time systems

Compositional Refinement for Real-Time Systems with Priorities

Quantitative Timed Simulation Functions and Refinement Metrics for Timed Systems (Full Version)

Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems

Robustness evaluation of real-Time Protocols

A Conservative Approximation Method for the Verification of Preemptive Scheduling Using Timed Automata

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

Similar Documents

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

Quantitative Temporal Simulation and Refinement Distances for Timed Systems

Robust Synthesis for Real Time Systems

Timed I/O automata: a complete specification theory for real-time systems

Compositional Refinement for Real-Time Systems with Priorities

Quantitative Timed Simulation Functions and Refinement Metrics for Timed Systems (Full Version)

Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems

Robustness evaluation of real-Time Protocols

A Conservative Approximation Method for the Verification of Preemptive Scheduling Using Timed Automata

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