Abstract
We present the implementation of trace theory in a new model checking tool framework, POEM, that has a strong emphasis on Partial Order Methods. A tree structure is used to store trace systems, which allows sharing common prefixes among traces and therefore reduces memory cost. This structure is easy to extend to incorporate additional features. Two applications are shown in the paper: An extended structure to support a new adequate order for Local First Search, and an acceleration of event zone based state space search for timed automata.
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
Behrmann, G., David, A., Larsen, K.G., Moeller, O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. of 40th IEEE Conference on Decision and Control, IEEE Computer Society Press, Los Alamitos (2001)
Bornot, S., Morin, R., Niebert, P., Zennou, S.: Black box unfolding with local first search. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 386–400. Springer, Heidelberg (2002)
Bozga, M., Graf, S., Mounier, L.: If-2.0: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 343–348. Springer, Heidelberg (2002)
Diekert, V., Rozemberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Esparza, J., Römer, S.: An unfolding algorithm for synchronous products of transition systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 2–20. Springer, Heidelberg (1999)
Esparza, J., Römer, S., Vogler, W.: An improvement of mcmillan’s unfolding algorithm. Formal Methods in System Design 20(3), 285–310 (2002)
Godefroid, P., Wolper, P.: A partial approach to model checking. In: Logic in Computer Science, pp. 406–415 (1991)
Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design 2, 149–164 (1993)
Holzmann, G.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Holzmann, G., Peled, D.: Partial order reduction of the state space. In: First SPIN Workshop, Montrèal, Quebec (1995)
Kurbán, M.E., Niebert, P., Qu, H., Vogler, W.: Stronger reduction criteria for local first search. Technical report (2006) (submitted to ICTAC 2006)
Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theoretical Computer Science 345(1), 27–59 (2005)
McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1), 45–65 (1995)
Niebert, P., Huhn, M., Zennou, S., Lugiez, D.: Local first search: a new paradigm in partial order reductions. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 396–410. Springer, Heidelberg (2001)
Niebert, P., Qu, H.: Adding invariants to event zone automata. Technical report (2006) (submitted to FORMATS 2006)
Parikh, R.J.: On context-free languages. Journal of the ACM 13(4), 570–581 (1966)
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Penczek, W., Kuiper, R.: Traces and logic. In: Diekert and Rozemberg, cite[4]
Valmari, A.: Stubborn sets for reduced state space generation. In: Applications and Theory of Petri Nets, pp. 491–515 (1989)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Niebert, P., Qu, H. (2006). The Implementation of Mazurkiewicz Traces in POEM. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_37
Download citation
DOI: https://doi.org/10.1007/11901914_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47237-7
Online ISBN: 978-3-540-47238-4
eBook Packages: Computer ScienceComputer Science (R0)