Document Open Access Logo

Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable

Authors Jan Martens , Jan Friso Groote

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2023.32.pdf
  • Filesize: 0.94 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Distinguishing behaviour
  • Hennessy-Milner logic
  • NP-hardness

Metrics

Abstract

We study the problem of computing minimal distinguishing formulas for non-bisimilar states in finite LTSs. We show that this is NP-hard if the size of the formula must be minimal. Similarly, the existence of a short distinguishing trace is NP-complete. However, we can provide polynomial algorithms, if minimality is formulated as the minimal number of nested modalities, and it can even be extended by recursively requiring a minimal number of nested negations. A prototype implementation shows that the generated formulas are much smaller than those generated by the method introduced by Cleaveland.

Cite As Get BibTex

Jan Martens and Jan Friso Groote. Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.32

Author Details

Jan Martens
  • Eindhoven University of Technology, The Netherlands
Jan Friso Groote
  • Eindhoven University of Technology, The Netherlands

Funding

AVVA project NWO 612.001.751/TOP1.17.002.

Supplementary Materials

References

  1. Manuel Baclet and Claire Pagetti. Around Hopcroft’s algorithm. In Implementation and Application of Automata: 11th International Conference, CIAA 2006, Taipei, Taiwan, August 21-23, 2006. Proceedings 11, pages 114-125. Springer, 2006. Google Scholar
  2. Christoph Berkholz, Paul Bonsma, and Martin Grohe. Tight lower and upper bounds for the complexity of canonical colour refinement. Theory of Computing Systems, 60(4):581-614, 2017. Google Scholar
  3. Benjamin Bisping, David N. Jansen, and Uwe Nestmann. Deciding all behavioral equivalences at once: A game for linear-time-branching-time spectroscopy. Logical Methods in Computer Science, 18(3), August 2022. URL: https://doi.org/10.46298/lmcs-18(3:19)2022.
  4. Michael C. Browne, Edmund M. Clarke, and Orna Grümberg. Characterizing finite kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1):115-131, 1988. URL: https://doi.org/10.1016/0304-3975(88)90098-9.
  5. Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mCRL2 toolset for analysing concurrent systems. In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS `19), pages 21-39. Springer International Publishing, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_2.
  6. Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Edmund M. Clarke and Robert P. Kurshan, editors, Proc. Computer-Aided Verification (CAV 1990), pages 364-372, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0023750.
  7. Keith Ellul, Bryan Krawetz, Jeffrey Shallit, and Ming-Wei Wang. Regular expressions: New results and open problems. J. Autom. Lang. Comb., 10(4):407-437, 2005. Google Scholar
  8. Santiago Figueira and Daniel Gorín. On the size of shortest modal descriptions. In Advances in Modal Logic, volume 8, pages 114-132, 2010. Google Scholar
  9. Herman Geuvers. Apartness and distinguishing formulas in Hennessy-Milner logic. In Nils Jansen, Mariëlle Stoelinga, and Petra van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning, pages 266-282. Springer Nature Switzerland, 2022. URL: https://doi.org/10.1007/978-3-031-15629-8_14.
  10. Jan Friso Groote and Frits Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, 1992. URL: https://doi.org/10.1016/0890-5401(92)90013-6.
  11. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jaco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming (ICALP `1980), pages 299-309, Berlin, Heidelberg, 1980. Springer-Verlag. URL: https://doi.org/10.5555/646234.758793.
  12. John Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Zvi Kohavi and Azaria Paz, editors, Theory of Machines and Computations, pages 189-196. Academic Press, 1971. URL: https://doi.org/10.1016/B978-0-12-417750-5.50022-1.
  13. Harry B. Hunt III. On the Time and Tape Complexity of Languages. PhD thesis, Cornell University, 1973. Google Scholar
  14. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86(1):43-68, 1990. URL: https://doi.org/10.1016/0890-5401(90)90025-D.
  15. Barbara König, Christina Mika-Michalski, and Lutz Schröder. Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In Daniela Petrişan and Jurriaan Rot, editors, Coalgebraic Methods in Computer Science (CMCS 2022), pages 133-154. Springer, 2020. Google Scholar
  16. Henri Korver. Computing distinguishing formulas for branching bisimulation. In Kim G. Larsen and Arne Skou, editors, Computer Aided Verification (CAV 1991), pages 13-23. Springer, 1992. Google Scholar
  17. David Lee and Mihalis Yannakakis. Testing finite-state machines: State identification and verification. IEEE Transactions on computers, 43(3):306-320, 1994. URL: https://doi.org/10.1109/12.272431.
  18. Bas Luttik. Description and formal specification of the Link Layer of P1394. CWI report. SEN-R : software engineering. Centrum voor Wiskunde en Informatica, 1997. Google Scholar
  19. Robin Milner. A calculus of communicating systems. Springer, 1980. Google Scholar
  20. Edward F. Moore. Gedanken-experiments on sequential machines. In Claude Shannon and John McCarthy, editors, Automata Studies, pages 129-153. Princeton University Press, Princeton, NJ, 1956. Google Scholar
  21. Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, 1987. URL: https://doi.org/10.1137/0216062.
  22. David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science, pages 167-183. Springer Berlin Heidelberg, 1981. Google Scholar
  23. Rick Smetsers, Joshua Moerman, and David N Jansen. Minimal separating sequences for all pairs of states. In Adrian-Horia Dediu, Jan Janoušek, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications (LATA 2016), pages 181-193. Springer, 2016. Google Scholar
  24. Antti Valmari. Bisimilarity minimization in o(m logn) time. In Giuliana Franceschinis and Karsten Wolf, editors, Applications and Theory of Petri Nets, pages 123-142, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  25. Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Quasilinear-time computation of generic modal witnesses for behavioural inequivalence. Logical Methods in Computer Science, 18(4), November 2022. URL: https://doi.org/10.46298/lmcs-18(4:6)2022.
  26. Jacob K. Wortmann, Simon R. Olesen, and Søren Enevoldsen. Caal 2.0. recursive HML, distinguishing formulae, equivalence collapses and parallel fixed-point computations. Master’s thesis, Aalborg University, 2015. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact