NDLI: Relaxed Decidability and the Robust Semantics of Metric Temporal Logic

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

Forward Inner-Approximated Reachability of Non-Linear Continuous Systems

Forward Stochastic Reachability Analysis for Uncontrolled Linear Systems using Fourier Transforms

Optimal Data Rate for State Estimation of Switched Nonlinear Systems

Robust Abstractions for Control Synthesis: Completeness via Robustness for Linear-Time Properties

Convex and Combinatorial Optimization for Dynamic Robots in the Real World

Coupling Policy Iterations with Piecewise Quadratic Lyapunov Functions

Dynamic Periodic Event-Triggered Control for Linear Systems

A Small Gain Theorem for Parametric Assume-Guarantee Contracts

Piecewise - Differentiable Trajectory Outcomes in Mechanical Systems Subject to Unilateral Constraints

On the Polytope Escape Problem for Continuous Linear Dynamical Systems

Controller Synthesis for Reward Collecting Markov Processes in Continuous Space

Path-Complete Graphs and Common Lyapunov Functions

Formal Synthesis of Stabilizing Controllers for Switched Systems

Robust Model Checking of Timed Automata under Clock Drifts

On a Class of Maximal Invariance Inducing Control Strategies for Large Collections of Switched Systems

Relaxed Decidability and the Robust Semantics of Metric Temporal Logic

Structural Analysis of Multi-Mode DAE Systems

SMC: Satisfiability Modulo Convex Optimization

Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision

Invariance Feedback Entropy of Nondeterministic Control Systems

Convex Interpolation Control with Formal Guarantees for Disturbed and Constrained Nonlinear Systems

Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Sampling-based Approximate Optimal Control Under Temporal Logic Constraints

Bipedal Robotic Running with DURUS-2D: Bridging the Gap between Theory and Experiment

Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems

Statistical Verification of the Toyota Powertrain Control Verification Benchmark

Scheduling of Embedded Controllers Under Timing Contracts

HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems

Abnormal Data Classification Using Time-Frequency Temporal Logic

Relaxed Decidability and the Robust Semantics of Metric Temporal Logic

Content Provider	ACM Digital Library
Author	Mangharam, Rahul Abbas, Houssam O'Kelly, Matthew
Abstract	Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and delta-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a slight restriction on the class of problems we verify, then it is possible to obtain practically useful answers. This paper explores the connections between relaxed decidability and the robust semantics of Metric Temporal Logic formulas. It establishes a formal equivalence between the robustness degree of MTL specifications, and the imprecision parameter delta used in delta-decidability when it is used to verify MTL properties. We present an application of this result in the form of an algorithm that generates new constraints to the delta-decision procedure from falsification runs, which can speed up the verification run. We then establish new conditions under which robust testing, based on the robust semantics of MTL, is in fact a quasi-semidecision procedure. These results allow us to delimit what is possible with fast, robustness-based methods, accelerate (near-)exhaustive verification, and further bridge the gap between verification and simulation.
Starting Page	217
Ending Page	225
Page Count	9
File Format	PDF
ISBN	9781450345903
DOI	10.1145/3049797.3049813
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2017-04-13
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Metric temporal logic Robust semantics Delta-decidability Quasi-decidability Hybrid systems Falsification
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

Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems

Partially Punctual Metric Temporal Logic is Decidable

A New Metric Temporal Logic for Hybrid Systems

Falsification of temporal properties of hybrid systems using the cross-entropy method

Ant colonies for temporal logic falsification of hybrid systems.

Probabilistic Temporal Logic Falsification of Cyber-Physical Systems

The Temporal Description Logic TL-SI and its Decidability Algorithm

On the decidability of metric temporal logic

On the Decidability and Complexity of Some Fragments of Metric Temporal Logic

Relaxed Decidability and the Robust Semantics of Metric Temporal Logic

Similar Documents

Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems

Partially Punctual Metric Temporal Logic is Decidable

A New Metric Temporal Logic for Hybrid Systems

Falsification of temporal properties of hybrid systems using the cross-entropy method

Ant colonies for temporal logic falsification of hybrid systems.

Probabilistic Temporal Logic Falsification of Cyber-Physical Systems

The Temporal Description Logic TL-SI and its Decidability Algorithm

On the decidability of metric temporal logic

On the Decidability and Complexity of Some Fragments of Metric Temporal Logic

Relaxed Decidability and the Robust Semantics of Metric Temporal Logic