---
_id: '4606'
abstract:
- lang: eng
text: "In formal design verification, successful model checking is typically preceded
by a laborious manual process of constructing design abstractions. We present
a methodology for partially—and in some cases, fully—bypassing the abstraction
process. For this purpose, we provide to the designer abstraction operators which,
if used judiciously in the description of a design, structure the corresponding
state space hierarchically. This structure can then be exploited by verification
tools, and makes possible the automatic and exhaustive exploration of state spaces
that would otherwise be out of scope for existing model checkers.\r\nSpecifically,
we present the following contributions:\r\n- \t A temporal abstraction operator
that aggregates transitions and hides intermediate steps. Mathematically, our
abstraction operator is a function that maps a flat transition system into a two-level
hierarchy where each atomic upper-level transition expands into an entire lower-level
transition system. For example, an arithmetic operation may expand into a sequence
of bit operations.\r\n- \t A BDD-based algorithm for the symbolic exploration
of multi-level hierarchies of transition systems. The algorithm traverses a level-n
transition by expanding the corresponding level-(n − 1) transition system on-the-fly.
The level-n successors of a state are determined by computing a level-(n − 1)
reach set, which is then immediately released from memory. In this fashion, we
can exhaustively explore hierarchically structured state spaces whose flat counterparts
cause memory overflows.\r\n- \t We experimentally demonstrate the efficiency of
our method with three examples—a multiplier, a cache coherence protocol, and a
multiprocessor system. In the first two examples, we obtain significant improvements
in run times and peak BDD sizes over traditional state-space search. The third
example cannot be model checked at all using conventional methods (without manual
abstractions), but can be analyzed fully automatically using transition hierarchies."
acknowledgement: "This research was supported in part by the Office of Naval Research
Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER
award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the
Air Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research
Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant
NAG2-892, and by the Semiconductor Research Corporation contract 95-DC-324.036.\r\n"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- 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: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Alur R, Henzinger TA, Rajamani S. Symbolic exploration of transition hierarchies.
In: Proceedings of the 4th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. Vol 1384. Springer; 1998:330-344.
doi:10.1007/BFb0054181'
apa: 'Alur, R., Henzinger, T. A., & Rajamani, S. (1998). Symbolic exploration
of transition hierarchies. In Proceedings of the 4th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems (Vol.
1384, pp. 330–344). Lisbon, Portugal: Springer. https://doi.org/10.1007/BFb0054181'
chicago: Alur, Rajeev, Thomas A Henzinger, and Sriram Rajamani. “Symbolic Exploration
of Transition Hierarchies.” In Proceedings of the 4th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 1384:330–44.
Springer, 1998. https://doi.org/10.1007/BFb0054181.
ieee: R. Alur, T. A. Henzinger, and S. Rajamani, “Symbolic exploration of transition
hierarchies,” in Proceedings of the 4th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal,
1998, vol. 1384, pp. 330–344.
ista: 'Alur R, Henzinger TA, Rajamani S. 1998. Symbolic exploration of transition
hierarchies. Proceedings of the 4th 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. 1384, 330–344.'
mla: Alur, Rajeev, et al. “Symbolic Exploration of Transition Hierarchies.” Proceedings
of the 4th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 1384, Springer, 1998, pp. 330–44, doi:10.1007/BFb0054181.
short: R. Alur, T.A. Henzinger, S. Rajamani, in:, Proceedings of the 4th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer, 1998, pp. 330–344.
conference:
end_date: 1998-04-04
location: Lisbon, Portugal
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 1998-03-28
date_created: 2018-12-11T12:09:43Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T08:44:36Z
day: '01'
doi: 10.1007/BFb0054181
extern: '1'
intvolume: ' 1384'
language:
- iso: eng
month: '01'
oa_version: None
page: 330 - 344
publication: Proceedings of the 4th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
publication_identifier:
isbn:
- '9783540643562'
publication_status: published
publisher: Springer
publist_id: '102'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic exploration of transition hierarchies
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1384
year: '1998'
...