## Files in this item

FilesDescriptionFormat

application/pdf

TBReach.pdf (1MB)
(no description provided)PDF

## Description

 Title: Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints Author(s): Roohi, Nima; Viswanathan, Mahesh Subject(s): Hybrid Automata, Reachability, Time-Bounded Reachability, Safety Verification 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 \lhd_1\dot{x} \lhd_2 cx+d$ (with $\lhd_1,\lhd_2 \in \{<,\leq\}$), 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. Issue Date: 2014-06-23 Publisher: Springer Citation Info: Extended abstract to appear in proceedings of Formal Modeling and Analysis of Timed Systems 2014 Genre: Article Type: Text Language: English URI: http://hdl.handle.net/2142/49952 Publication Status: published or submitted for publication Peer Reviewed: is peer reviewed Date Available in IDEALS: 2014-06-23
﻿