Document Open Access Logo

Explaining Behavioural Inequivalence Generically in Quasilinear Time

Authors Thorsten Wißmann , Stefan Milius , Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.32.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Author Details

Thorsten Wißmann
  • Radboud University, Nijmegen, The Netherlands
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Wißmann, Thorsten: Work forms part of the NWO TOP project 612.001.852 and the DFG-funded project COAX (MI 717/5-2).
  • Milius, Stefan: Work forms part of the DFG-funded project CoMoC (MI 717/7-1).
  • Schröder, Lutz: Work forms part of the DFG-funded project CoMoC (SCHR 1118/15-1).

Cite AsGet BibTex

Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining Behavioural Inequivalence Generically in Quasilinear Time. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.32

Abstract

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time 𝒪((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was 𝒪(m n).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Program analysis
Keywords
  • bisimulation
  • partition refinement
  • modal logic
  • distinguishing formulae
  • coalgebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Peter Aczel and Nax Mendler. A final coalgebra theorem. In Proc. Category Theory and Computer Science (CTCS), volume 389 of LNCS, pages 357-365. Springer, 1989. Google Scholar
  2. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial algebras, terminal coalgebras, and the theory of fixed points of functors. draft book, available online at https://www8.cs.fau.de/ext/milius/publications/files/CoalgebraBook.pdf, 2021.
  3. Micah Adler and Neil Immerman. An n! lower bound on formula size. In LICS 2001, pages 197-206. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/LICS.2001.932497.
  4. Micah Adler and Neil Immerman. An n! lower bound on formula size. ACM Trans. Comput. Log., 4(3):296-314, 2003. URL: https://doi.org/10.1145/772062.772064.
  5. Abel Armas-Cervantes, Paolo Baldan, Marlon Dumas, and Luciano García-Bañuelos. Behavioral comparison of process models based on canonically reduced event structures. In Business Process Management, pages 267-282. Springer, 2014. Google Scholar
  6. Abel Armas-Cervantes, Luciano García-Bañuelos, and Marlon Dumas. Event structures as a foundation for process model differencing, part 1: Acyclic processes. In Web Services and Formal Methods, pages 69-86. Springer, 2013. Google Scholar
  7. Falk Bartels, Ana Sokolova, and Erik de Vink. A hierarchy of probabilistic system types. Theoret. Comput. Sci., 327:3-22, 2004. Google Scholar
  8. Marco Bernardo. TwoTowers 5.1 user manual, 2004. Google Scholar
  9. Marco Bernardo, Rance Cleaveland, Steve Sims, and W. Stewart. TwoTowers: A tool integrating functional and performance analysis of concurrent systems. In Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE / PSTV 1998, volume 135 of IFIP Conference Proceedings, pages 457-467. Kluwer, 1998. Google Scholar
  10. Marco Bernardo and Marino Miculan. Constructive logical characterizations of bisimilarity for reactive probabilistic systems. Theoretical Computer Science, 764:80-99, 2019. Selected papers of ICTCS 2016. Google Scholar
  11. Johanna Björklund and Loek Cleophas. Aggregation-based minimization of finite state automata. Acta Informatica, 2020. Google Scholar
  12. Ufuk Celikkan and Rance Cleaveland. Generating diagnostic information for behavioral preorders. Distributed Computing, 9(2):61-75, 1995. Google Scholar
  13. Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Computer-Aided Verification, pages 364-372. Springer, 1991. Google Scholar
  14. Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), volume 41 of LIPIcs, pages 78-93. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.78.
  15. Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic partition refinement and weighted tree automata. In Formal Methods - The Next 30 Years, Proc. 3rd World Congress on Formal Methods (FM 2019), volume 11800 of LNCS, pages 280-297. Springer, October 2019. Google Scholar
  16. J. Desharnais, A. Edalat, and P. Panangaden. A logical characterization of bisimulation for labeled markov processes. In Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pages 478-487, 1998. Google Scholar
  17. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled markov processes. Information and Computation, 179(2):163-193, 2002. Google Scholar
  18. Remco Dijkman. Diagnosing differences between business process models. In Business Process Management, pages 261-277, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  19. Ernst-Erich Doberkat. Stochastic Coalgebraic Logic. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02995-0.
  20. Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient coalgebraic partition refinement. In Proc. 28th International Conference on Concurrency Theory (CONCUR 2017), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.32.
  21. Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Predicate liftings and functor presentations in coalgebraic expression languages. In Coalgebraic Methods in Computer Science, CMCS 2018, volume 11202 of LNCS, pages 56-77. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00389-0_5.
  22. Santiago Figueira and Daniel Gorín. On the size of shortest modal descriptions. In Advances in Modal Logic 8, papers from the eighth conference on "Advances in Modal Logic," held in Moscow, Russia, 24-27 August 2010, pages 120-139. College Publications, 2010. URL: http://www.aiml.net/volumes/volume8/Figueira-Gorin.pdf.
  23. Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. On the succinctness of some modal logics. Artificial Intelligence, 197:56-85, 2013. Google Scholar
  24. Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_19.
  25. H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Coalgebraic Methods in Computer Science, CMCS 2001, volume 44(1) of ENTCS, pages 185-204. Elsevier, 2001. URL: https://doi.org/10.1016/S1571-0661(04)80908-3.
  26. H.Peter Gumm. From T-coalgebras to filter structures and transition systems. In Algebra and Coalgebra in Computer Science, volume 3629 of LNCS, pages 194-212. Springer, 2005. Google Scholar
  27. John Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Theory of Machines and Computations, pages 189-196. Academic Press, 1971. Google Scholar
  28. Paris C. Kanellakis and Scott A. Smolka. Ccs expressions, finite state processes, and three problems of equivalence. In Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, PODC '83, pages 228-240. ACM, 1983. Google Scholar
  29. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput., 86(1):43-68, 1990. URL: https://doi.org/10.1016/0890-5401(90)90025-D.
  30. Bartek Klin. The least fibred lifting and the expressivity of coalgebraic modal logic. In Algebra and Coalgebra in Computer Science, CALCO 2005, volume 3629 of LNCS, pages 247-262. Springer, 2005. URL: https://doi.org/10.1007/11548133_16.
  31. Timo Knuutila. Re-describing an algorithm by Hopcroft. Theor. Comput. Sci., 250:333-363, 2001. Google Scholar
  32. Barbara König, Christina Mika-Michalski, and Lutz Schröder. Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In Coalgebraic Methods in Computer Science, pages 133-154. Springer, 2020. Google Scholar
  33. Kim Guldstrand Larsen and Arne Arne Skou. Bisimulation through probabilistic testing. Inform. Comput., 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  34. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81(5):880-900, 2015. URL: https://doi.org/10.1016/j.jcss.2014.12.006.
  35. R. Milner. Communication and Concurrency. International series in computer science. Prentice-Hall, 1989. Google Scholar
  36. Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM J. Comput., 16(6):973-989, 1987. Google Scholar
  37. D. Park. Concurrency and automata on infinite sequences. In Proceedings of 5th GI-Conference on Theoretical Computer Science, volume 104 of LNCS, pages 167-183, 1981. Google Scholar
  38. Dirk Pattinson. Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1):177-193, 2003. Google Scholar
  39. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19-33, 2004. URL: https://doi.org/10.1305/ndjfl/1094155277.
  40. Jan Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  41. Jan Rutten and Erik de Vink. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoret. Comput. Sci., 221:271-293, 1999. Google Scholar
  42. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390(2-3):230-247, 2008. URL: https://doi.org/10.1016/j.tcs.2007.09.023.
  43. Věra Trnková. On a descriptive classification of set functors I. Commentationes Mathematicae Universitatis Carolinae, 12(1):143-174, 1971. Google Scholar
  44. Antti Valmari and Giuliana Franceschinis. Simple 𝒪(mlog n) time Markov chain lumping. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, volume 6015 of LNCS, pages 38-52. Springer, 2010. Google Scholar
  45. Antti Valmari and Petri Lehtinen. Efficient minimization of dfas with partial transition. In Theoretical Aspects of Computer Science, STACS 2008, volume 1 of LIPIcs, pages 645-656. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2008. URL: https://doi.org/10.4230/LIPIcs.STACS.2008.1328.
  46. Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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