Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Hybrid Automata with Finite Mutual Simulations

Hybrid Automata with Finite Mutual Simulations

File(s)
95-1497.ps (241.9 KB)
95-1497.pdf (193.03 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7155
Collections
Computer Science Technical Reports
Author
Henzinger, Thomas A.
Kopke, Peter W.
Abstract

Many decidability results for hybrid automata rely upon the finite region bisimulation of timed automata [AD94]. Rectangular automata do not have finite bisimulations [Hen95], yet have many decidable verification problems [PV94,HKPV95]. We prove that every two-dimensional rectangular automaton A with positive-slope variables has a finite mutual simulation relation, which is the intersection of the region bisimulations defined by the extremal slopes of the variables of A. While the mutual simulation is infinite for two-dimensional automata with one variable taking both positive and negative slopes, it forms a regular tesselation of the plane, and therefore can be encoded by one counter. As a corollary, we obtain the decidability of model checking linear temporal logic on these automata.

Date Issued
1995-03
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1497
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance