Abstract
Effective temporal logic model checking algorithms exist that exploit symmetries arising from parallel composition of multiple identical components. These algorithms often employ a function rep from states to representative states under the symmetries exploited. We adapt this idea to the context of refinement checking for the process algebra CSP. In so doing, we must cope with refinement-style specifications. The main challenge, though, is the need for access to sufficient local information about states to enable definition of a useful rep function, since compilation of CSP processes to Labelled Transition Systems (LTSs) renders state information a global property instead of a local one. Using a structured form of implementation transition system, we obtain an efficient symmetry exploiting CSP refinement checking algorithm, generalise it in two directions, and demonstrate all three variants on simple examples.
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
Miller, A., Donaldson, A.F., Calder, M.: Symmetry in Temporal Logic Model Checking. ACM Comput. Surv. 38(3) (2006)
Hoare, C.A.R.: Communicating Sequential Processes. CACM, 21(8) (1978)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Formal Systems (Europe) Ltd: Failures-Divergences Refinement: FDR2 User Manual (1992-2008)
Moffat, N., Goldsmith, M., Roscoe, A.W.: Towards Symmetry Aware Refinement Checking (Extended Abstract). In: Proceedings of International Symmetry Conference, Edinburgh, UK (2007)
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, A.W.: Modelling and Analysis of Security Protocols. Addison-Wesley, Reading (2001)
Park, D.M.: Concurrency on automata and infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104. Springer, Heidelberg (1981)
Milner, R.: Communication and concurrency. Prentice-Hall, Englewood Cliffs (1989)
Clarke, E., Enders, R., Filkhorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. Formal Methods in System Design 9(1/2), 77–104 (1996)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design 9(12), 105–131 (1996)
Lazić, R.S.: A semantic study of data-independence with applications to the mechanical verification of concurrent systems. Ph.D. thesis, Oxford University Computing Laboratory (1999)
Emerson, E.A., Havlicek, J., Trefler, R.: Virtual Symmetry Reduction. In: Proceedings of the 15th IEEE Symposium on Logic in Computer Science (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moffat, N., Goldsmith, M., Roscoe, B. (2008). A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking. In: Liu, S., Maibaum, T., Araki, K. (eds) Formal Methods and Software Engineering. ICFEM 2008. Lecture Notes in Computer Science, vol 5256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88194-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-88194-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88193-3
Online ISBN: 978-3-540-88194-0
eBook Packages: Computer ScienceComputer Science (R0)