Abstract
We propose to use bisimulation to quantify dissimilarity between processes: in this case we speak of k-bisimulation. Two processes p and q, whose semantics is given through transition systems, are k-bisimilar if they differ from at most k moves, where k is a natural number. Roughly speaking, the k-bisimulation captures the extension of the dissimilarity between p and q when they are neither strong nor weak equivalent. The importance of the formal concept of k-bisimulation can be seen in several application fields, such as clone detection, process mining, business-IT alignment. We propose several heuristics in order to efficiently check such a bisimulation. The approach can be applied to different specification languages (CCS, LOTOS, CSP) provided that the language semantics is based on the notion of transition system. We have implemented a prototype tool and we have conducted experiments on well-known systems for a proof of concept of our methodology.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
We use iff thereafter.
- 2.
- 3.
References
Van der Aalst, W., Weijters, T., Maruster, L.: Workflow mining: discovering process models from event logs. IEEE Trans. Knowl. Data Eng. 16(9), 1128–1142 (2004)
Alkhammash, E., Fathabadi, A.S., Butler, M.J., Cîrstea, C.: Building traceable Event-B models from requirements. ECEASST 66, 1–16 (2013)
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14(1), 25–59 (1987)
Bruns, G.: A case study in safety-critical design. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 220–233. Springer, Heidelberg (1993)
Černý, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 253–268. Springer, Heidelberg (2010)
Chen, X., Deng, Y.: Game characterizations of process equivalences. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 107–121. Springer, Heidelberg (2008)
Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Conchon, S., Krstic, S.: Strategies for combining decision procedures. Theor. Comput. Sci. 354(2), 187–210 (2006)
Cuomo, A., Santone, A., Villano, U.: CD-Form: a clone detector based on formal methods. Sci. Comput. Program. 95, 390–405 (2014)
De Francesco, N., Santone, A., Tesei, L.: Abstract interpretation and model checking for checking secure information flow in concurrent systems. Fundamenta Informaticae 54(2), 195–211 (2003)
De Ruvo, G., Santone, A.: Equivalence-based selection of best-fit models to support wiki design. In: Reddy, S. (ed.) WETICE 2015, pp. 204–209. IEEE Press, New York (2015)
Delsarte, P., Levenshtein, V.I.: Association schemes and coding theory. IEEE Trans. Inf. Theor. 44(6), 2477–2504 (1998)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)
van Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR ’90 Theories of Concurrency: Unification and Extension. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)
Hamming, R.W.: Error detecting and error correcting codes. Bell Syst. Tech. J. 29(2), 147–160 (1950)
Hoare, C.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
Jacquart, P.: Nouvelles recherches sur la distribution florale. Bull. Soc. Vand. Sci. Nat. 44, 223–270 (1908)
Mazzocca, N., Santone, A., Vaglini, G., Vittorini, V.: Efficient model checking of properties of a distributed application: a multimedia case study. Softw. Test. Verif. Reliab. 12(1), 3–21 (2002)
Milner, R.: Communication and Concurrency. Prentice Hall, London (1989). Prentice Hall International Series in Computer Science
Nguyen, H.N., Poizat, P., Zaïdi, F.: A symbolic framework for the conformance checking of value-passing choreographies. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds.) Service Oriented Computing. LNCS, vol. 7636, pp. 525–532. Springer, Heidelberg (2012)
Palahan, S., Babic, D., Chaudhuri, S., Kifer, D.: Extraction of statistically significant malware behaviors. In: Paynre Jr., C.N. (ed.) ACSAC 2013, pp. 69–78. ACM, New York (2013)
Romero Hernández, D., de Frutos Escrig, D.: Defining distances for all process semantics. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 169–185. Springer, Heidelberg (2012)
Romero-Hernández, D., de Frutos Escrig, D.: Coinductive definition of distances between processes: beyond bisimulation distances. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 249–265. Springer, Heidelberg (2014)
Roy, C., Cordy, J., Koschke, R.: Comparison and evaluation of code clone detection techniques and tools: a qualitative approach. Sci. Comput. Program. 74(7), 470–495 (2009)
Santone, A., Vaglini, G.: Abstract reduction in directed model checking CCS processes. Acta Informatica 49(5), 313–341 (2012)
Santone, A., Vaglini, G., Villani, M.L.: Incremental construction of systems: an efficient characterization of the lacking sub-system. Sci. Comput. Program. 78(9), 1346–1367 (2013)
Ullah, A., Lai, R.: A systematic review of business and information technology alignment. ACM Trans. Manage. Inf. Syst. 4(1), 1–30 (2013)
Zeng, Z., Tung, A.K.H., Wang, J., Feng, J., Zhou, L.: Comparing stars: on approximating graph edit distance. PVLDB 2(1), 25–36 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
De Ruvo, G., Lettieri, G., Martino, D., Santone, A., Vaglini, G. (2016). k-Bisimulation: A Bisimulation for Measuring the Dissimilarity Between Processes. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-28934-2_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-28933-5
Online ISBN: 978-3-319-28934-2
eBook Packages: Computer ScienceComputer Science (R0)