Abstract
| Original language | English |
|---|---|
| Title of host publication | Automated Technology for Verification and Analysis |
| Subtitle of host publication | 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings |
| Editors | Zhiming Liu, Anders P. Ravn |
| Place of Publication | Berlin |
| Publisher | Springer |
| Pages | 54-68 |
| Number of pages | 15 |
| ISBN (Electronic) | 978-3-642-04761-9 |
| ISBN (Print) | 978-3-642-04760-2 |
| DOIs | |
| Publication status | Published - 13 Oct 2009 |
| Event | 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 - Macao, China Duration: 14 Oct 2009 → 16 Oct 2009 Conference number: 7 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Verlag |
| Volume | 5799 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 |
|---|---|
| Abbreviated title | ATVA |
| Country | China |
| City | Macao |
| Period | 14/10/09 → 16/10/09 |
Fingerprint
Keywords
- IR-68161
- METIS-264067
- Dead variable analysis
- EWI-16155
- Process Algebra
- Control flow reconstruction
- State space reduction
Cite this
}
State Space Reduction of Linear Processes Using Control Flow Reconstruction. / van de Pol, Jan Cornelis; Timmer, Mark.
Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. ed. / Zhiming Liu; Anders P. Ravn. Berlin : Springer, 2009. p. 54-68 (Lecture Notes in Computer Science; Vol. 5799).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - State Space Reduction of Linear Processes Using Control Flow Reconstruction
AU - van de Pol, Jan Cornelis
AU - Timmer, Mark
N1 - 10.1007/978-3-642-04761-9_5
PY - 2009/10/13
Y1 - 2009/10/13
N2 - We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear process equations (LPEs). Our method consists of two steps: (1) we reconstruct the LPE's control flow, detecting control flow parameters that were introduced by linearisation as well as those already encoded in the original specification; (2) we reset parameters found to be irrelevant based on data flow analysis techniques similar to traditional liveness analysis, modified to take into account the parallel nature of the specifications. Our transformation is correct with respect to strong bisimilarity, and never increases the state space. Case studies show that impressive reductions occur in practice, which could not be obtained automatically without reconstructing the control flow.
AB - We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear process equations (LPEs). Our method consists of two steps: (1) we reconstruct the LPE's control flow, detecting control flow parameters that were introduced by linearisation as well as those already encoded in the original specification; (2) we reset parameters found to be irrelevant based on data flow analysis techniques similar to traditional liveness analysis, modified to take into account the parallel nature of the specifications. Our transformation is correct with respect to strong bisimilarity, and never increases the state space. Case studies show that impressive reductions occur in practice, which could not be obtained automatically without reconstructing the control flow.
KW - IR-68161
KW - METIS-264067
KW - Dead variable analysis
KW - EWI-16155
KW - Process Algebra
KW - Control flow reconstruction
KW - State space reduction
U2 - 10.1007/978-3-642-04761-9_5
DO - 10.1007/978-3-642-04761-9_5
M3 - Conference contribution
SN - 978-3-642-04760-2
T3 - Lecture Notes in Computer Science
SP - 54
EP - 68
BT - Automated Technology for Verification and Analysis
A2 - Liu, Zhiming
A2 - Ravn, Anders P.
PB - Springer
CY - Berlin
ER -