Access Restriction

Author Henzinger, Thomas A. ♦ Kopke, Peter W. ♦ Puri, Anuj ♦ Varaiya, Pravin
Source CiteSeerX
Content type Text
Publisher ACM Press
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Hybrid Automaton Model System ♦ Previous Decidability ♦ Reachability Information ♦ Many Verification Task ♦ Reachability Analysis ♦ Independent Trajectory ♦ Timed Automaton ♦ Undecidability Result ♦ Envelope Change ♦ Positive Side ♦ Reachability Problem ♦ Symbolic Procedure ♦ Piecewise-linear Envelope ♦ Practical Significance ♦ Pspace Reachability Algorithm ♦ Analog Variable ♦ Initialized Rectangular Automaton ♦ Initialized Rectangular Autom ♦ Analog Component ♦ Hybrid Automaton ♦ Control Program
Description . Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular autom...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1995-01-01
Journal Journal of Computer and System Sciences