---
_id: '4435'
abstract:
- lang: eng
text: 'An important case of hybrid systems are the rectangular automata. First,
rectangular dynamics can naturally and arbitrarily closely approximate more general,
nonlinear dynamics. Second, rectangular automata are the most general type of
hybrid systems for which model checking -in particular, Ltl model checking- is
decidable. However, on one hand, the original proofs of decidability did not suggest
practical algorithms and, on the other hand, practical symbolic model-checking
procedures -such as those implemented in HyTech- were not known to terminate on
rectangular automata. We remedy this unsatisfactory situation: we present a symbolic
method for Ltl model checking which can be performed by HyTech and is guaranteed
to terminate on all rectangular automata. We do so by proving that our method
for symbolic Ltl model checking terminates on an infinite-state transition system
if the trace-equivalence relation of the system has finite index, which is the
case for all rectangular automata.'
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660,
the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Majumdar R. Symbolic model checking for rectangular hybrid systems.
In: Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. Vol 1785. Springer; 2000:142-156.
doi:10.1007/3-540-46419-0_11'
apa: 'Henzinger, T. A., & Majumdar, R. (2000). Symbolic model checking for rectangular
hybrid systems. In Proceedings of the 6th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (Vol. 1785, pp.
142–156). Berlin, Germany: Springer. https://doi.org/10.1007/3-540-46419-0_11'
chicago: Henzinger, Thomas A, and Ritankar Majumdar. “Symbolic Model Checking for
Rectangular Hybrid Systems.” In Proceedings of the 6th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 1785:142–56.
Springer, 2000. https://doi.org/10.1007/3-540-46419-0_11.
ieee: T. A. Henzinger and R. Majumdar, “Symbolic model checking for rectangular
hybrid systems,” in Proceedings of the 6th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, Berlin, Germany,
2000, vol. 1785, pp. 142–156.
ista: 'Henzinger TA, Majumdar R. 2000. Symbolic model checking for rectangular hybrid
systems. Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 1785, 142–156.'
mla: Henzinger, Thomas A., and Ritankar Majumdar. “Symbolic Model Checking for Rectangular
Hybrid Systems.” Proceedings of the 6th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, vol. 1785, Springer,
2000, pp. 142–56, doi:10.1007/3-540-46419-0_11.
short: T.A. Henzinger, R. Majumdar, in:, Proceedings of the 6th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Springer,
2000, pp. 142–156.
conference:
end_date: 2000-04-02
location: Berlin, Germany
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2000-03-25
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:08:09Z
day: '01'
doi: 10.1007/3-540-46419-0_11
extern: '1'
intvolume: ' 1785'
language:
- iso: eng
month: '01'
oa_version: None
page: 142 - 156
publication: Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
publication_identifier:
isbn:
- '9783540672821'
publication_status: published
publisher: Springer
publist_id: '293'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for rectangular hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1785
year: '2000'
...