---
_id: '4608'
abstract:
- lang: eng
text: 'State space explosion is a fundamental obstacle in formal verification of
designs and protocols. Several techniques for combating this problem have emerged
in the past few years, among which two are significant: partial-order reductions
and symbolic state space search. In asynchronous systems, interleavings of independent
concurrent events are equivalent, and only a representative interleaving needs
to be explored to verify local properties. Partial-order methods exploit this
redundancy and visit only a subset of the reachable states. Symbolic techniques,
on the other hand, capture the transition relation of a system and the set of
reachable states as boolean functions. In many cases, these functions can be represented
compactly using binary decision diagrams (BDDs). Traditionally, the two techniques
have been practiced by two different schools—partial-order methods with enumerative
depth-first search for the analysis of asynchronous network protocols, and symbolic
breadth-first search for the analysis of synchronous hardware designs. We combine
both approaches and develop a method for using partial-order reduction techniques
in symbolic BDD-based invariant checking. We present theoretical results to prove
the correctness of the method, and experimental results to demonstrate its efficacy.'
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the Semiconductor Research Corporation contracts DC-324.036
and DC-324.005.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Robert
full_name: Brayton, Robert
last_name: Brayton
- 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: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction
in symbolic state-space exploration. In: 9th International Conference on Computer
Aided Verification. Vol 1254. Springer; 1997:340-351. doi:10.1007/3-540-63166-6_34'
apa: 'Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (1997).
Partial-order reduction in symbolic state-space exploration. In 9th International
Conference on Computer Aided Verification (Vol. 1254, pp. 340–351). Haifa,
Israel: Springer. https://doi.org/10.1007/3-540-63166-6_34'
chicago: Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram
Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” In 9th
International Conference on Computer Aided Verification, 1254:340–51. Springer,
1997. https://doi.org/10.1007/3-540-63166-6_34.
ieee: R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order
reduction in symbolic state-space exploration,” in 9th International Conference
on Computer Aided Verification, Haifa, Israel, 1997, vol. 1254, pp. 340–351.
ista: 'Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 1997. Partial-order
reduction in symbolic state-space exploration. 9th International Conference on
Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1254,
340–351.'
mla: Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.”
9th International Conference on Computer Aided Verification, vol. 1254,
Springer, 1997, pp. 340–51, doi:10.1007/3-540-63166-6_34.
short: R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, in:, 9th International
Conference on Computer Aided Verification, Springer, 1997, pp. 340–351.
conference:
end_date: 1997-06-25
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 1997-06-22
date_created: 2018-12-11T12:09:44Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-16T14:09:54Z
day: '01'
doi: 10.1007/3-540-63166-6_34
extern: '1'
intvolume: ' 1254'
language:
- iso: eng
month: '01'
oa_version: None
page: 340 - 351
publication: 9th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540631668'
publication_status: published
publisher: Springer
publist_id: '99'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Partial-order reduction in symbolic state-space exploration
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1254
year: '1997'
...
---
_id: '4494'
abstract:
- lang: eng
text: A hybrid system consists of a collection of digital programs that interact
with each other and with an analog environment. Examples of hybrid systems include
medical equipment, manufacturing controllers, automotive controllers, and robots.
The formal analysis of the mixed digital-analog nature of these systems requires
a model that incorporates the discrete behavior of computer programs with the
continuous behavior of environment variables, such as temperature and pressure.
Hybrid automata capture both types of behavior by combining finite automata with
differential inclusions (i.e. differential inequalities). HyTech is a symbolic
model checker for linear hybrid automata, an expressive, yet automatically analyzable,
subclass of hybrid automata. A key feature of HyTech is its ability to perform
parametric analysis, i.e. to determine the values of design parameters for which
a linear hybrid automaton satisfies a temporal requirement.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 95-DC-324.036.
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: Pei
full_name: Ho, Pei
last_name: Ho
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems.
In: Vol 1254. Springer; 1997:460-463. doi:10.1007/3-540-63166-6_48'
apa: 'Henzinger, T. A., Ho, P., & Wong Toi, H. (1997). HyTech: A model checker
for hybrid systems (Vol. 1254, pp. 460–463). Presented at the CAV: Computer Aided
Verification, Haifa, Israel: Springer. https://doi.org/10.1007/3-540-63166-6_48'
chicago: 'Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker
for Hybrid Systems,” 1254:460–63. Springer, 1997. https://doi.org/10.1007/3-540-63166-6_48.'
ieee: 'T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid
systems,” presented at the CAV: Computer Aided Verification, Haifa, Israel, 1997,
vol. 1254, pp. 460–463.'
ista: 'Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid
systems. CAV: Computer Aided Verification, LNCS, vol. 1254, 460–463.'
mla: 'Henzinger, Thomas A., et al. HyTech: A Model Checker for Hybrid Systems.
Vol. 1254, Springer, 1997, pp. 460–63, doi:10.1007/3-540-63166-6_48.'
short: T.A. Henzinger, P. Ho, H. Wong Toi, in:, Springer, 1997, pp. 460–463.
conference:
end_date: 1997-06-25
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 1997-06-22
date_created: 2018-12-11T12:09:08Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T11:06:13Z
day: '01'
doi: 10.1007/3-540-63166-6_48
extern: '1'
intvolume: ' 1254'
language:
- iso: eng
month: '01'
oa_version: None
page: 460 - 463
publication_identifier:
isbn:
- '9783540631668'
publication_status: published
publisher: Springer
publist_id: '235'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'HyTech: A model checker for hybrid systems'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1254
year: '1997'
...