×

zbMATH — the first resource for mathematics

Next-preserving branching bisimulation. (English) Zbl 1328.68141
Summary: Bisimulations are equivalence relations between transition systems which assure that certain aspects of the behaviour of the systems are the same in a related pair. For many applications it is not possible to maintain such an equivalence unless non-observable (stuttering) behaviour is ignored. However, existing bisimulation relations which permit the removal of non-observable behaviour are unable to preserve temporal logic formulas referring to the next step operator. In this paper we propose a family of next-preserving branching bisimulations to overcome this limitation.
Next-preserving branching bisimulations are parameterised with a natural number, indicating the nesting depth of the \(\mathbf X\) operators that the bisimulation preserves, while still allowing non-observable behaviour to be reduced. Based on R. J. van Glabbeek and W. P. Weijland’s notion of branching bisimulation with explicit divergence [J. ACM 43, No. 3, 555–600 (1996; Zbl 0882.68085)], we define the novel parameterised relation for which we prove the preservation of \(\mathrm{CTL}^\ast\) formulas with an \(\mathbf X\) operator-nesting depth that is not greater than the specified parameter. It can be shown that the family of next-preserving bisimulations constitutes a hierarchy that fills the gap between branching bisimulation and strong bisimulation.
As an example for its application we show how this definition gives rise to an advanced slicing procedure that creates a formula-specific slice, which constitutes a reduced model of the system that can be used as a substitute when verifying this formula. The result is a novel procedure for generating slices that are next-preserving branching bisimilar to the original model for any formula. We can assure that each slice preserves the formula it corresponds to, which renders the overall verification process sound.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
CESAR; SIGREF; SPIN
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Park, D., Concurrency and automata on infinite sequences, (GI Conference on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 104, (1981)), 167-183
[2] Milner, R., Communication and concurrency, (1989), Prentice Hall · Zbl 0683.68008
[3] Emerson, E. A., Temporal and modal logic, (van Leeuwen, J., Handbook of Theoretical Computer Science, vol. B, (1990), Elsevier Science Publishers), 995-1072 · Zbl 0900.03030
[4] Weiser, M., Program slicing, (Proc. of Int. Conf. on Software Engineering, ICSE’81, (1981)), 439-449
[5] van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600, (1996) · Zbl 0882.68085
[6] Ranganath, V. P.; Amtoft, T.; Banerjee, A.; Hatcliff, J.; Dwyer, M. B., A new foundation for control dependence and slicing for modern program structures, ACM Trans. Program. Lang. Syst., 29, 5, 1-43, (2007), (Article 27)
[7] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (2000), MIT Press
[8] Clarke, E.; Emerson, E., Design and synthesis of synchronization skeletons using branching time temporal logic, (Logics of Programs, Lecture Notes in Computer Science, vol. 131, (1982), Springer-Verlag), 52-71 · Zbl 0546.68014
[9] Queille, J.; Sifakis, J., Specification and verification of concurrent systems in CESAR, (International Symposium on Programming, Lecture Notes in Computer Science, vol. 137, (1982), Springer-Verlag), 337-351 · Zbl 0482.68028
[10] Grunske, L.; Lindsay, P. A.; Yatapanage, N.; Winter, K., An automated failure mode and effect analysis based on high-level design specification with behavior trees, (Romijn, J.; Smith, G.; van de Pol, J., Proc. of Int. Conf. on Integrated Formal Methods, IFM 2005, Lecture Notes in Computer Science, vol. 3771, (2005), Springer), 129-149
[11] Grunske, L.; Winter, K.; Yatapanage, N.; Zafar, S.; Lindsay, P. A., Experience with fault injection experiments for FMEA, Softw. Pract. Exp., 41, 11, 1233-1258, (2011)
[12] Lindsay, P.; Yatapanage, N.; Winter, K., Cut set analysis using behavior trees and model checking, Form. Asp. Comput., 24, 2, 249-266, (2012)
[13] Dromey, R. G., Genetic design: amplifying our ability to deal with requirements complexity, (Scenarios: Models, Transformations and Tools, Lecture Notes in Computer Science, vol. 3466, (2005), Springer), 95-108
[14] Colvin, R. J.; Hayes, I. J., A semantics for behavior trees using CSP with specification commands, Sci. Comput. Program., 76, 10, 891-914, (2011) · Zbl 1220.68050
[15] Yatapanage, N.; Winter, K.; Zafar, S., Slicing behavior tree models for verification, (Theoretical Computer Science, IFIP Adv. Inf. Commun. Technol., vol. 323, (2010), Springer-Verlag), 125-139 · Zbl 1202.68258
[16] de Nicola, R.; Vaandrager, F., Three logics for branching bisimulation, J. ACM, 42, 2, 458-487, (1995) · Zbl 0886.68064
[17] Emerson, E. A.; Halpern, J. Y., “sometimes“ and “not never” revisited: on branching versus linear time temporal logic, J. ACM, 33, 1, 151-178, (1986) · Zbl 0629.68020
[18] van Glabbeek, R. J.; Luttik, B.; Trčka, N., Branching bisimilarity with explicit divergence, Fund. Inform., 93, 4, 371-392, (2009) · Zbl 1183.68404
[19] van Glabbeek, R. J.; Luttik, B.; Trčka, N., Computation tree logic with deadlock detection, Log. Methods Comput. Sci., 5, 4:5, 1-24, (2009) · Zbl 1200.68166
[20] Lamport, L., What good is temporal logic?, (IFIP Congress on Information Processing, (1983)), 657-668
[21] Antonik, A.; Huth, M., Efficient patterns for model checking partial state spaces in CTL intersection LTL, Electron. Notes Theor. Comput. Sci., 158, 41-57, (2006) · Zbl 1273.68218
[22] Kučera, A.; Strejček, J., The stuttering principle revisited, Acta Inform., 41, 7-8, 415-434, (2005) · Zbl 1079.03008
[23] Tip, F., A survey of program slicing techniques, J. Program. Lang., 3, 3, 121-189, (1995)
[24] Xu, B.; Qian, J.; Zhang, X.; Wu, Z.; Chen, L., A brief survey of program slicing, ACM SIGSOFT Softw. Eng. Notes, 30, 2, 1-36, (2005)
[25] Oda, T.; Araki, K., Specification slicing in formal methods of software development, (Proc. of Computer Software and Applications Conference, COMSAC 93, (1993), IEEE), 313-319
[26] Heimdahl, M.; Whalen, M., Reduction and slicing of hierarchical state machines, (Jazayeri, M.; Schauer, H., Proc. of European Software Engineering Conference, ESEC ’97/FSE-5, Lecture Notes in Computer Science, vol. 1301, (1997), Springer-Verlag), 450-467
[27] Millett, L. I.; Teitelbaum, T., Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation, Int. J. Softw. Tools Technol. Transf., 2, 4, 343-349, (2000) · Zbl 1059.68590
[28] Ganesh, V.; Saidi, H.; Shankar, N., Slicing SAL, (1999), Computer Science Laboratory, Tech. rep.
[29] Korel, B.; Singh, I.; Tahat, L.; Vaysburg, B., Slicing of state-based models, (Proc. of Int. Conf. on Software Maintenance, ICSM 2003, (2003), IEEE), 34-43
[30] Wu, F.; Yi, T., Slicing Z specifications, ACM SIGPLAN Not., 39, 8, 39-48, (2004)
[31] Brückner, I.; Wehrheim, H., Slicing an integrated formal method for verification, (Lau, K.-K.; Banach, R., Proc. of Int. Conf. on Formal Methods and Software Engineering, ICFEM’05, Lecture Notes in Computer Science, vol. 3785, (2005), Springer), 360-374
[32] Labbe, S.; Gallois, J.-P.; Pouzet, M., Slicing communicating automata specifications for efficient model reduction, (Grundy, J.; Han, J., Proc. of Australian Software Engineering Conference, ASWEC 2007, (2007), IEEE Computer Society Press), 191-200
[33] Thrane, C., Slicing for UPPAAL, (Ann. IEEE Conf. (Student Paper), (2008), IEEE), 1-5
[34] Odenbrett, M.; Nguyen, V. Y.; Noll, T., Slicing AADL specifications for model checking, (Muñoz, C., NASA Formal Methods, NASA Conference Proceedings, vol. NASA/CP-2010-216215, (2010)), 217-221
[35] Dromey, R. G., From requirements to design: formalizing the key steps, (Proc. of Software Engineering and Formal Methods, SEFM 2003, (2003), IEEE Computer Society), 2-11
[36] Colvin, R.; Hayes, I. J., CSP with hierarchical state, (Leuschel, M.; Wehrheim, H., Proc. of Int. Conf. on Integrated Formal Methods, IFM’09, Lecture Notes in Computer Science, vol. 5423, (2009), Springer), 118-135 · Zbl 1211.68266
[37] Winter, K.; Hayes, I. J.; Colvin, R., Integrating requirements: the behavior tree philosophy, (Proc. of Int. Conf. on Software Engineering and Formal Methods, SEFM 2010, (2010), IEEE Computer Society Press), 41-50
[38] Grunske, L.; Winter, K.; Yatapanage, N., Defining the abstract syntax of visual languages with advanced graph grammars—a case study based on behavior trees, J. Vis. Lang. Comput., 19, 3, 343-379, (2008)
[39] Ottenstein, K. J.; Ottenstein, L. M., The program dependence graph in a software development environment, ACM SIGSOFT Softw. Eng. Notes, 9, 3, 177-184, (1984)
[40] Ferrante, J.; Ottenstein, K. J.; Warren, J. D., The program dependence graph and its use in optimization, ACM Trans. Program. Lang. Syst., 9, 3, 319-349, (1987) · Zbl 0623.68012
[41] Yatapanage, N., Slicing behavior trees for verification of large systems, (2012), Institute for Integrated and Intelligent Systems, Griffith University, Ph.D. thesis
[42] Bergstra, J. A.; Ponse, A.; van der Zwaag, M. B., Branching time and orthogonal bisimulation equivalence, Theoret. Comput. Sci., 309, 1-3, 313-355, (2003) · Zbl 1070.68100
[43] Brückner, I.; Wehrheim, H., Slicing object-Z specifications for verification, (Treharne, H.; King, S.; Henson, M. C.; Schneider, S. A., Proc. of Int. Conf. on Formal Specification and Development in Z and B, ZB’05, Lecture Notes in Computer Science, vol. 3455, (2005), Springer), 414-433 · Zbl 1118.68541
[44] Brückner, I., Slicing concurrent real-time system specifications for verification, (Davies, J.; Gibbons, J., Proc. of Integrated Formal Methods, IFM’07, Lecture Notes in Computer Science, vol. 4591, (2007), Springer), 54-74 · Zbl 1213.68366
[45] Rakow, A., Slicing Petri nets with an application to workflow verification, (Geffert, V.; Karhumäki, J.; Bertoni, A.; Preneel, B.; Návrat, P.; Bieliková, M., Proc. of Conf. on Current Trends in Theory and Practice of Computer Science, SOFSEM’08, Lecture Notes in Computer Science, vol. 4910, (2008), Springer), 436-447 · Zbl 1133.68060
[46] Bordini, R. H.; Fisher, M.; Wooldridge, M.; Visser, W., Property-based slicing for agent verification, J. Logic Comput., 19, 6, 1385-1425, (2009) · Zbl 1185.68751
[47] Hatcliff, J.; Dwyer, M. B.; Zheng, H., Slicing software for model construction, High.-Order Symb. Comput., 13, 4, 315-353, (2000) · Zbl 0972.68021
[48] Holzmann, G. J., The model checker SPIN, IEEE Trans. Softw. Eng., 23, 5, 279-295, (1997)
[49] Schäfer, I.; Poetzsch-Heffter, A., Slicing for model reduction in adaptive embedded systems development, (Proc. of Int. Workshop on Software Engineering for Adaptive and Self-Managing Systems, SEAMS’08, (2008), ACM New York, NY, USA), 25-32
[50] van Langenhove, S.; Hoogewijs, A., \(\operatorname{SV}_t \operatorname{L}\): system verification through logic tool support for verifying sliced hierarchical statecharts, (Fiadeiro, J. L.; Schobbens, P.-Y., Proc. on Int. Workshop on Recent Trends in Algebraic Development Techniques, WADT’06, Lecture Notes in Computer Science, vol. 4409, (2006), Springer), 142-155 · Zbl 1196.68144
[51] Wimmer, R.; Herbstritt, M.; Hermanns, H.; Strampp, K.; Becker, B., Sigref - a symbolic bisimulation tool box, (Graf, S.; Zhang, W., Automated Technology for Verification and Analysis, ATVA 2006, Lecture Notes in Computer Science, vol. 4218, (2006)), 477-492 · Zbl 1161.68631
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.