LIPIcs.CALCO.2021.21.pdf
- Filesize: 0.61 MB
- 5 pages
Document
Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)
Authors
-
Part of:
Volume:
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-11-08
Cite As Get 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)
https://doi.org/10.4230/LIPIcs.CALCO.2021.21
Abstract
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
Keywords
- simulation
- weak simulation
- up-to technique
- language inclusion
- preorder
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The machinery of interaction. In PPDP 2020, pages 4:1-4:15. ACM, 2020.
-
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.
-
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.
-
Bart Jacobs and Jesse Hughes. Simulations in coalgebra. Electronic Notes in Theoretical Computer Science, 82(1):128-149, 2003.
-
Bengt Jonsson and Kim Guldstrand Larsen. Specification and refinement of probabilistic processes. In LICS 1991, pages 266-277. IEEE Computer Society, 1991.
-
Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991.
- Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations: I. Untimed systems. Inf. Comput., 121(2):214-233, 1995. URL: https://doi.org/10.1006/inco.1995.1134.
- 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: https://doi.org/10.1109/SWAT.1972.29.
-
Koko Muroya. Hypernet Semantics of Programming Languages. PhD thesis, University of Birmingham, 2020.
-
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.
-
Damien Pous. New up-to techniques for weak bisimulation. Theoretical Computer Science, 380(1):164-180, 2007. Automata, Languages and Programming.
-
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.
-
Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994.