Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints

Nima Roohi; Mahesh Viswanathan

doi:10.1007/978-3-319-10512-3_14

Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints

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

Abstract

Initialized hybrid automata with linear differential inclusions and rectangular constraints are hybrid automata where the invariants, guards, resets, and initial values are given by rectangular constraints, the flows are described by linear differential inclusions of the form ax + b ◁₁ x ◁₂ cx + d (with ◁₁, ◁₂ ∈ {<, ≤}), and a variable x is reset on mode change whenever the differential inclusion describing the dynamics for x changes. Such automata strictly subsume initialized rectangular automata. Our main result is that while the control state reachability problem for such automata is undecidable, the time-bounded reachability problem is decidable.

Original language	English (US)
Title of host publication	Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings
Publisher	Springer
Pages	191-205
Number of pages	15
ISBN (Print)	9783319105116
DOIs	https://doi.org/10.1007/978-3-319-10512-3_14
State	Published - 2014
Event	12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014 - Florence, Italy Duration: Sep 8 2014 → Sep 10 2014

Publication series

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

Other

Other	12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014
Country/Territory	Italy
City	Florence
Period	9/8/14 → 9/10/14

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-319-10512-3_14

Library availability

Discover UIUC Full Text

Cite this

Roohi, N., & Viswanathan, M. (2014). Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. In Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings (pp. 191-205). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8711 LNCS). Springer. https://doi.org/10.1007/978-3-319-10512-3_14

Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. / Roohi, Nima; Viswanathan, Mahesh.
Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings. Springer, 2014. p. 191-205 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8711 LNCS).

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

Roohi, N & Viswanathan, M 2014, Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. in Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8711 LNCS, Springer, pp. 191-205, 12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014, Florence, Italy, 9/8/14. https://doi.org/10.1007/978-3-319-10512-3_14

Roohi N, Viswanathan M. Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. In Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings. Springer. 2014. p. 191-205. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-10512-3_14

Roohi, Nima ; Viswanathan, Mahesh. / Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings. Springer, 2014. pp. 191-205 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0814110c8ec749cdbb135353ff8a7192,

title = "Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints",

abstract = "Initialized hybrid automata with linear differential inclusions and rectangular constraints are hybrid automata where the invariants, guards, resets, and initial values are given by rectangular constraints, the flows are described by linear differential inclusions of the form ax + b ◁1 x ◁2 cx + d (with ◁1, ◁2 ∈ {<, ≤}), and a variable x is reset on mode change whenever the differential inclusion describing the dynamics for x changes. Such automata strictly subsume initialized rectangular automata. Our main result is that while the control state reachability problem for such automata is undecidable, the time-bounded reachability problem is decidable.",

author = "Nima Roohi and Mahesh Viswanathan",

year = "2014",

doi = "10.1007/978-3-319-10512-3_14",

language = "English (US)",

isbn = "9783319105116",

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

publisher = "Springer",

pages = "191--205",

booktitle = "Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings",

address = "Germany",

note = "12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014 ; Conference date: 08-09-2014 Through 10-09-2014",

}

TY - GEN

T1 - Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints

AU - Roohi, Nima

AU - Viswanathan, Mahesh

PY - 2014

Y1 - 2014

N2 - Initialized hybrid automata with linear differential inclusions and rectangular constraints are hybrid automata where the invariants, guards, resets, and initial values are given by rectangular constraints, the flows are described by linear differential inclusions of the form ax + b ◁1 x ◁2 cx + d (with ◁1, ◁2 ∈ {<, ≤}), and a variable x is reset on mode change whenever the differential inclusion describing the dynamics for x changes. Such automata strictly subsume initialized rectangular automata. Our main result is that while the control state reachability problem for such automata is undecidable, the time-bounded reachability problem is decidable.

AB - Initialized hybrid automata with linear differential inclusions and rectangular constraints are hybrid automata where the invariants, guards, resets, and initial values are given by rectangular constraints, the flows are described by linear differential inclusions of the form ax + b ◁1 x ◁2 cx + d (with ◁1, ◁2 ∈ {<, ≤}), and a variable x is reset on mode change whenever the differential inclusion describing the dynamics for x changes. Such automata strictly subsume initialized rectangular automata. Our main result is that while the control state reachability problem for such automata is undecidable, the time-bounded reachability problem is decidable.

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

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

U2 - 10.1007/978-3-319-10512-3_14

DO - 10.1007/978-3-319-10512-3_14

M3 - Conference contribution

AN - SCOPUS:84958527386

SN - 9783319105116

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

SP - 191

EP - 205

BT - Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings

PB - Springer

T2 - 12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014

Y2 - 8 September 2014 through 10 September 2014

ER -

Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this