State Space Reduction of Linear Processes Using Control Flow Reconstruction


Share/Save/Bookmark

Pol van de, Jaco and Timmer, Mark (2009) State Space Reduction of Linear Processes Using Control Flow Reconstruction. In: 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, October 14-16, 2009, Macao SAR, China.

[img]
Preview
PDF (Author's version)
221Kb
[img]PDF (Publisher's version)
Restricted to UT campus only
: Request a copy
258Kb
Abstract: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.
Item Type:Conference or Workshop Item
Copyright:© 2009 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/68161
Official URL:http://dx.doi.org/10.1007/978-3-642-04761-9_5
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 264067