DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2018.26

Relating Syntactic and Semantic Perturbations of Hybrid Automata

Authors: Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

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 epsilon-simulation 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 non-strict 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 counter-example validation in a CEGAR framework, namely, when a counter-example is spurious, then we have a complete procedure for deducing the same.

Cite as

Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Relating Syntactic and Semantic Perturbations of Hybrid Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{roohi_et_al:LIPIcs.CONCUR.2018.26,
  author =	{Roohi, Nima and Prabhakar, Pavithra and Viswanathan, Mahesh},
  title =	{{Relating Syntactic and Semantic Perturbations of Hybrid Automata}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{26:1--26:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.26},
  URN =		{urn:nbn:de:0030-drops-95644},
  doi =		{10.4230/LIPIcs.CONCUR.2018.26},
  annote =	{Keywords: Model Checking, Hybrid Automata, Approximation, Perturbation}
}

Document

DOI: 10.4230/DagRep.4.3.85

Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122)

Authors: Rupak Majumdar, Richard M. Murray, and Pavithra Prabhakar

Published in: Dagstuhl Reports, Volume 4, Issue 3 (2014)

Abstract

Cyber-physical systems refer to a new genre of engineered systems consisting of a tight coupling between computation, communication and physical entities. The main focus of the seminar was to discuss issues related to the reliable development of cyber-physical systems by using formal verification. This is a multi-disciplinary area requiring collaboration between areas focusing discrete systems analysis and continuous systems analysis. To this end, the seminar brought together researchers working in the fields of formal methods, control theory and hybrid systems to identify and discuss potential issues and research questions which require collaboration between the communities. This report documents the program and the outcomes of Dagstuhl Seminar 14122 "Verification of Cyber-Physical Systems".

Cite as

Rupak Majumdar, Richard M. Murray, and Pavithra Prabhakar. Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122). In Dagstuhl Reports, Volume 4, Issue 3, pp. 85-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{majumdar_et_al:DagRep.4.3.85,
  author =	{Majumdar, Rupak and Murray, Richard M. and Prabhakar, Pavithra},
  title =	{{Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122)}},
  pages =	{85--102},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{3},
  editor =	{Majumdar, Rupak and Murray, Richard M. and Prabhakar, Pavithra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.3.85},
  URN =		{urn:nbn:de:0030-drops-45937},
  doi =		{10.4230/DagRep.4.3.85},
  annote =	{Keywords: Formal Verification, Cyber-Physical Systems, Hybrid Systems}
}

Search Results

Documents authored by Prabhakar, Pavithra

Relating Syntactic and Semantic Perturbations of Hybrid Automata

Abstract

Cite as

Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122)

Abstract

Cite as

Thanks for your feedback!

Could not send message