Abstract
We investigate how the semantics of a hybrid automaton deviates with respect to syntactic perturbations on the hybrid automaton. We consider syntactic perturbations of a hybrid automaton, wherein the syntactic representations of its elements, namely, initial sets, invariants, guards, and flows, in some logic are perturbed. Our main result establishes a continuity like property that states that small perturbations in the syntax lead to small perturbations in the semantics. More precisely, we show that for every real number epsilon>0 and natural number k, there is a real number delta>0 such that H^delta, the delta syntactic perturbation of a hybrid automaton H, is epsilonsimulation equivalent to H up to k transition steps. As a byproduct, we obtain a proof that a bounded safety verification tool such as dReach will eventually prove the safety of a safe hybrid automaton design (when only nonstrict inequalities are used in all constraints) if dReach iteratively reduces the syntactic parameter delta that is used in checking approximate satisfiability. This has an immediate application in counterexample validation in a CEGAR framework, namely, when a counterexample is spurious, then we have a complete procedure for deducing the same.
BibTeX  Entry
@InProceedings{roohi_et_al:LIPIcs:2018:9564,
author = {Nima Roohi and Pavithra Prabhakar and Mahesh Viswanathan},
title = {{Relating Syntactic and Semantic Perturbations of Hybrid Automata}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {26:126:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770873},
ISSN = {18688969},
year = {2018},
volume = {118},
editor = {Sven Schewe and Lijun Zhang},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9564},
URN = {urn:nbn:de:0030drops95644},
doi = {10.4230/LIPIcs.CONCUR.2018.26},
annote = {Keywords: Model Checking, Hybrid Automata, Approximation, Perturbation}
}
Keywords: 

Model Checking, Hybrid Automata, Approximation, Perturbation 
Seminar: 

29th International Conference on Concurrency Theory (CONCUR 2018) 
Issue Date: 

2018 
Date of publication: 

13.08.2018 