Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)

Authors Koko Muroya, Takahiro Sanada, Natsuki Urabe

Thumbnail PDF


  • Filesize: 0.61 MB
  • 5 pages

Document Identifiers

Author Details

Koko Muroya
  • RIMS, Kyoto University, Japan
Takahiro Sanada
  • RIMS, Kyoto University, Japan
Natsuki Urabe
  • National Institute of Informatics, Tokyo, Japan

Cite AsGet BibTex

Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


We describe our ongoing work on generalizing some quantitatively constrained notions of weak simulation up-to that are recently introduced for deterministic systems modeling program execution. We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison between words using a preorder, instead of equality.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • simulation
  • weak simulation
  • up-to technique
  • language inclusion
  • preorder


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


  1. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The machinery of interaction. In PPDP 2020, pages 4:1-4:15. ACM, 2020. Google Scholar
  2. Suguman Bansal, Swarat Chaudhuri, and Moshe Y. Vardi. Comparator automata in quantitative verification. In FoSSaCS 2018, volume 10803 of Lecture Notes in Computer Science, pages 420-437. Springer, 2018. Google Scholar
  3. Milka Hutagalung, Martin Lange, and Étienne Lozes. Buffered simulation games for büchi automata. In Zoltán Ésik and Zoltán Fülöp, editors, AFL 2014, volume 151 of EPTCS, pages 286-300, 2014. Google Scholar
  4. Bart Jacobs and Jesse Hughes. Simulations in coalgebra. Electronic Notes in Theoretical Computer Science, 82(1):128-149, 2003. Google Scholar
  5. Bengt Jonsson and Kim Guldstrand Larsen. Specification and refinement of probabilistic processes. In LICS 1991, pages 266-277. IEEE Computer Society, 1991. Google Scholar
  6. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. Google Scholar
  7. Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations: I. Untimed systems. Inf. Comput., 121(2):214-233, 1995. URL:
  8. A. R. Meyer and L. J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In 13th Annual Symposium on Switching and Automata Theory (swat 1972), pages 125-129, 1972. URL:
  9. Koko Muroya. Hypernet Semantics of Programming Languages. PhD thesis, University of Birmingham, 2020. Google Scholar
  10. Damien Pous. Up-to techniques for weak bisimulation. In Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, ICALP 2005, volume 3580 of Lecture Notes in Computer Science, pages 730-741. Springer, 2005. Google Scholar
  11. Damien Pous. New up-to techniques for weak bisimulation. Theoretical Computer Science, 380(1):164-180, 2007. Automata, Languages and Programming. Google Scholar
  12. Natsuki Urabe and Ichiro Hasuo. Generic forward and backward simulations III: quantitative simulations by matrices. In CONCUR 2014, volume 8704 of Lecture Notes in Computer Science, pages 451-466. Springer, 2014. Google Scholar
  13. Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail