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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)
Arts, T., Earle, C.B., Derrick, J.: Verifying Erlang code: A resource locker case-study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 184–203. Springer, Heidelberg (2002)
Badban, B., Fokkink, W., Groote, J.F., Pang, J., van de Pol, J.: Verification of a sliding window protocol in μCRL and PVS. Formal Aspects of Computing 17(3), 342–388 (2005)
Bezem, M., Groote, J.F.: Invariants in process algebra with data. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 401–416. Springer, Heidelberg (1994)
Blom, S., van de Pol, J.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 596–609. Springer, Heidelberg (2002)
Blom, S., van de Pol, J.: Symbolic reachability for process algebras with recursive data types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81–95. Springer, Heidelberg (2008)
Bozga, M., Fernandez, J.-C., Ghirvu, L.: State space reduction based on live variables analysis. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 164–178. Springer, Heidelberg (1999)
Chandy, K.M., Misra, J.: Parallel program design: a foundation. Addison-Wesley, Reading (1988)
Fokkink, W., Ioustinova, N., Kesseler, E., van de Pol, J., Usenko, Y.S., Yushtein, Y.A.: Refinement and verification applied to an in-flight data acquisition unit. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 1–23. Springer, Heidelberg (2002)
Garavel, H., Serwe, W.: State space reduction for process algebra specifications. Theoretical Computer Science 351(2), 131–145 (2006)
Groote, J.F., Lisser, B.: Computer assisted manipulation of algebraic process specifications. Technical report, SEN-R0117, CWI (2001)
Groote, J.F., Ponse, A.: The syntax and semantics of μCRL. In: Proc. of the 1st Workshop on the Algebra of Communicating Processes (ACP 1994), pp. 26–62. Springer, Heidelberg (1994)
Groote, J.F., Ponse, A., Usenko, Y.S.: Linearization in parallel pCRL. Journal of Logic and Algebraic Programming 48(1-2), 39–72 (2001)
Groote, J.F., van de Pol, J.: State space reduction using partial τ-confluence. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 383–393. Springer, Heidelberg (2000)
Hesselink, W.H.: Invariants for the construction of a handshake register. Information Processing Letters 68(4), 173–177 (1998)
Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), 219–246 (1989)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Pang, J., Fokkink, W., Hofman, R.F.H., Veldema, R.: Model checking a cache coherence protocol of a Java DSM implementation. Journal of Logic and Algebraic Programming 71(1), 1–43 (2007)
Usenko, Y.S.: Linearization in μCRL. PhD thesis, Eindhoven University (2002)
van de Pol, J., Timmer, M.: State space reduction of linear processes using control flow reconstruction (extended version). Technical report, TR-CTIT-09-24, CTIT, University of Twente (2009)
Winters, B.D., Hu, A.J.: Source-level transformations for improved formal verification. In: Proc. of the 18th IEEE Int. Conference on Computer Design (ICCD 2000), pp. 599–602 (2000)
Yorav, K., Grumberg, O.: Static analysis for state-space reductions preserving temporal logics. Formal Methods in System Design 25(1), 67–96 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van de Pol, J., Timmer, M. (2009). State Space Reduction of Linear Processes Using Control Flow Reconstruction. In: Liu, Z., Ravn, A.P. (eds) Automated Technology for Verification and Analysis. ATVA 2009. Lecture Notes in Computer Science, vol 5799. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04761-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-04761-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04760-2
Online ISBN: 978-3-642-04761-9
eBook Packages: Computer ScienceComputer Science (R0)