Hybrid automata-based CEGAR for rectangular hybrid systems

Pavithra Prabhakar; Parasara Sridhar Duggirala; Sayan Mitra; Mahesh Viswanathan

doi:10.1007/978-3-642-35873-9_6

Hybrid automata-based CEGAR for rectangular hybrid systems

Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called Hare, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate the usefulness of the approach.

Original language	English (US)
Title of host publication	Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings
Publisher	Springer
Pages	48-67
Number of pages	20
ISBN (Print)	9783642358722
DOIs	https://doi.org/10.1007/978-3-642-35873-9_6
State	Published - 2013
Event	14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013 - Rome, Italy Duration: Jan 20 2013 → Jan 22 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7737 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013
Country/Territory	Italy
City	Rome
Period	1/20/13 → 1/22/13

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-642-35873-9_6

Library availability

Discover UIUC Full Text

Cite this

Prabhakar, P., Duggirala, P. S., Mitra, S., & Viswanathan, M. (2013). Hybrid automata-based CEGAR for rectangular hybrid systems. In Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings (pp. 48-67). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7737 LNCS). Springer. https://doi.org/10.1007/978-3-642-35873-9_6

Hybrid automata-based CEGAR for rectangular hybrid systems. / Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan et al.
Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Springer, 2013. p. 48-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7737 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Prabhakar, P, Duggirala, PS, Mitra, S & Viswanathan, M 2013, Hybrid automata-based CEGAR for rectangular hybrid systems. in Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7737 LNCS, Springer, pp. 48-67, 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, Rome, Italy, 1/20/13. https://doi.org/10.1007/978-3-642-35873-9_6

Prabhakar P, Duggirala PS, Mitra S , Viswanathan M. Hybrid automata-based CEGAR for rectangular hybrid systems. In Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Springer. 2013. p. 48-67. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-35873-9_6

Prabhakar, Pavithra ; Duggirala, Parasara Sridhar ; Mitra, Sayan et al. / Hybrid automata-based CEGAR for rectangular hybrid systems. Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Springer, 2013. pp. 48-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d2e6870393544b9d96fbd2589ee0566a,

title = "Hybrid automata-based CEGAR for rectangular hybrid systems",

abstract = "In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called Hare, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate the usefulness of the approach.",

author = "Pavithra Prabhakar and Duggirala, {Parasara Sridhar} and Sayan Mitra and Mahesh Viswanathan",

year = "2013",

doi = "10.1007/978-3-642-35873-9_6",

language = "English (US)",

isbn = "9783642358722",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "48--67",

booktitle = "Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings",

address = "Germany",

note = "14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013 ; Conference date: 20-01-2013 Through 22-01-2013",

}

TY - GEN

T1 - Hybrid automata-based CEGAR for rectangular hybrid systems

AU - Prabhakar, Pavithra

AU - Duggirala, Parasara Sridhar

AU - Mitra, Sayan

AU - Viswanathan, Mahesh

PY - 2013

Y1 - 2013

N2 - In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called Hare, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate the usefulness of the approach.

AB - In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called Hare, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate the usefulness of the approach.

UR - http://www.scopus.com/inward/record.url?scp=84881132663&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84881132663&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-35873-9_6

DO - 10.1007/978-3-642-35873-9_6

M3 - Conference contribution

AN - SCOPUS:84881132663

SN - 9783642358722

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 48

EP - 67

BT - Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings

PB - Springer

T2 - 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013

Y2 - 20 January 2013 through 22 January 2013

ER -

Hybrid automata-based CEGAR for rectangular hybrid systems

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this