Undecidability Results for Hybrid Systems
Permanent Link(s)
Collections
Author
Henzinger, Thomas A.
Kopke, Peter W.
Abstract
We illuminate the boundary between decidability and undecidability for hybrid systems. Adding any of the following decorations to a timed automaton makes the reachability problem undecidable: 1. a single stopwatch with weak (less than or equal to, greater than or equal to) edge guards 2. a single skewed clock with variable equality tests 3. a single two-slope clock with weak edge guards 4. a single memory cell with weak edge guards As a corollary, we obtain undecidability for linear hybrid systems with triangular differential inclusions, which have invariants of the form x' less than or equal to y'.
Date Issued
1995-02
Publisher
Cornell University
Keywords
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1483
Type
technical report