Abstract
We present a new approach to combine partial order reduction with fairness in the context of LTL model checking. For this purpose, we define several behaviour classes representing typical fairness assumptions and examine how various reduction techniques affect these classes. In particular, we consider both reductions preserving all behaviours and reductions preserving only some behaviours.
This work has been partially supported by the Grant Agency of Czech Republic grant No. GACR 201/06/1338. and by the Academy of Sciences of the Czech Republic grant. No. 1ET408050503.
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.
References
Bosnacki, D.: Partial order reduction in presence of rendez-vous communications with unless constructs and weak fairness. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol. 1680, pp. 40–56. Springer, Heidelberg (1999)
Brim, L., Černá, I., Moravec, P., Šimša, J.: Distributed Partial Order Reduction. Electronic Notes in Theoretical Computer Science 128, 63–74 (2005)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)
Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 438–449. Springer, Heidelberg (1993)
Holzmann, G.J., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis. In: Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Orlando, Fl., June (1992), citeseer.nj.nec.com/holzmann92coverage.html
Latvala, T., Heljanko, K.: Coping with strong fairness. Fundamenta Informaticae, 175–193 (2000)
Peled, D.: All from one, one from all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)
Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the nexttime operator. Information Processing Letters (1997)
Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Brim, L., Černá, I., Moravec, P., Šimša, J. (2007). On Combining Partial Order Reduction with Fairness Assumptions. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds) Formal Methods: Applications and Technology. PDMC 2006. Lecture Notes in Computer Science, vol 4346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70952-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-70952-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70951-0
Online ISBN: 978-3-540-70952-7
eBook Packages: Computer ScienceComputer Science (R0)