Computing Bisimulation-Based Comparisons

• Autorzy: Nguyen L. A.

Identyfikatory

DOI

10.3233/FI-2018-1634

• Języki publikacji: EN

Abstrakty

EN

We provide the first algorithm with a polynomial time complexity, O((m + n)²n²), for computing the largest bisimulation-based auto-comparison of a labeled graph in the setting with counting successors, where m is the number of edges and n is the number of vertices. This setting is like the case with graded modalities in modal logics and qualified number restrictions in description logics. Furthermore, by using the idea of Henzinger et al. for computing simulations, we give an efficient algorithm, with complexity O((m + n)n), for computing the largest bisimulation-based auto-comparison and the directed similarity relation of a labeled graph in the setting without counting successors. We also adapt our former algorithm for computing the simulation pre-order of a labeled graph in the setting with counting successors.

Słowa kluczowe

EN

bisimulation; polynomials; vertices; computer algorithms; KRIPKE semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 157, nr 4
• Strony: 385--401
• Opis fizyczny: Bibliogr. 19 poz., rys.

Twórcy

autor

Nguyen L. A.

• Division of Knowledge and System Engineering for ICT, Faculty of Information Technology, Ton Duc Thang University, Ho Chi Minh City, Vietnam
• Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland

Bibliografia

• [1] Hennessy M, Milner R. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM, 1985;32(1):137-161. doi:10.1145/2455.2460.
• [2] van Benthem J. Modal Correspondence Theory. Ph.D. thesis, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, University of Amsterdam, 1976.
• [3] Blackburn P, de Rijke M, Venema Y. Modal Logic. Number 53 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. ISBN: 10:0521527147, 13:978-0521527149.
• [4] Kurtonina N, de Rijke M. Simulating Without Negation. J. Log. Comput., 1997;7(4):501-522. URL https://doi.org/10.1093/logcom/7.4.501.
• [5] Divroodi A, Nguyen L. Bisimulation-Based Comparisons for Interpretations in Description Logics. In: Proceedings of Description Logics’2013, volume 1014 of CEUR Workshop Proceedings. CEUR-WS.org, 2013 pp. 652-669. arXiv:1304.5602 [cs.LO].
• [6] Divroodi A. Bisimulation Equivalence in Description Logics and Its Applications. Ph.D. thesis, University of Warsaw, 2015.
• [7] Paige R, Tarjan R. Three Partition Refinement Algorithms. SIAM J. Comput., 1987;16(6):973-989. doi:10.1137/0216062.
• [8] Hopcroft J. An n log n algorithm for minimizing states in a finite automaton. 1971. URL ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/71/190/CS-TR-71-190.pdf.
• [9] Bloom B, Paige R. Transformational Design and Implementation of a New Efficient Solution to the Ready Simulation Problem. Sci. Comput. Program., 1995;24(3):189-220. URL https://doi.org/10.1016/0167-6423(95)00003-B.
• [10] Henzinger M, Henzinger T, Kopke P. Computing Simulations on Finite and Infinite Graphs. In: Proceedings of FOCS’1995. IEEE Computer Society, 1995 pp. 453-462. doi:10.1109/SFCS.1995.492576.
• [11] Sangiorgi D. On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst.. Volume 31 Issue 4, May 2009. Article No. 15. doi:10.1145/1516507.1516510.
• [12] Bustan D, Grumberg O. Simulation-based minimazation. ACM Trans. Comput. Log., 2003;4(2):181-206. doi:10.1145/635499.635502.
• [13] Gentilini R, Piazza C, Policriti A. From Bisimulation to Simulation: Coarsest Partition Problems. J. Autom. Reasoning, 2003;31(1):73-103. URL https://doi.org/10.1023/A:1027328830731.
• [14] Ranzato F, Tapparo F. An efficient simulation algorithm based on abstract interpretation. Inf. Comput., 2010;208(1):1-22. URL https://doi.org/10.1016/j.ic.2009.06.002.
• [15] Cairo M, Rizzi R. The Complexity of Simulation and Matrix Multiplication. In: Proceedings of SODA 2017. SIAM, 2017 pp. 2203-2214. URL http://dl.acm.org/citation.cfm?id=3039686.3039830.
• [16] Nguyen L. A long version of the current paper. 2017. URL http://www.mimuw.edu.pl/~nguyen/CompBSDLP-long.pdf.
• [17] Nguyen L, Nguyen THK, Nguyen NT, Ha QT. Bisimilarity for paraconsistent description logics. Journal of Intelligent and Fuzzy Systems, 2017;32(2):1203-1215. doi:10.3233/JIFS-169120.
• [18] Nguyen L. Computing Bisimulation-Based Comparisons. In: Proceedings of CS&P’2016, volume 1698 of CEUR Workshop Proceedings. CEUR-WS.org, 2016 pp. 245-256. URL http://ceur-ws.org/Vol-1698/CS&P2016_23_Nguyen_Computing-Bisimulation-Based-Comparisons.pdf.
• [19] Nguyen L. An implementation of Algorithms 1, 4 and 5 given in the current paper. 2017. URL http://www.mimuw.edu.pl/~nguyen/CompBSDLP-prog.zip.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).