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

Nima Roohi, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference 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 ◁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.

Original languageEnglish (US)
Title of host publicationFormal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings
PublisherSpringer
Pages191-205
Number of pages15
ISBN (Print)9783319105116
DOIs
StatePublished - 2014
Event12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014 - Florence, Italy
Duration: Sep 8 2014Sep 10 2014

Publication series

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

Other

Other12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014
Country/TerritoryItaly
CityFlorence
Period9/8/149/10/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints'. Together they form a unique fingerprint.

Cite this