Document

**Published in:** LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

We introduce ω^ ̅-NED, an edit distance between infinite words, that is a natural extension of NED, the normalized edit distance between finite words. We show it is a metric on (equivalence classes of) infinite words. We provide a polynomial time algorithm to compute the distance between two ultimately periodic words, and a polynomial time algorithm to compute the distance between two regular ω-languages given by non-deterministic Büchi automata.

Dana Fisman, Joshua Grogin, and Gera Weiss. A Normalized Edit Distance on Infinite Words. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{fisman_et_al:LIPIcs.CSL.2023.20, author = {Fisman, Dana and Grogin, Joshua and Weiss, Gera}, title = {{A Normalized Edit Distance on Infinite Words}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.20}, URN = {urn:nbn:de:0030-drops-174818}, doi = {10.4230/LIPIcs.CSL.2023.20}, annote = {Keywords: Edit Distance, Infinite Words, Robustness} }

Document

**Published in:** LIPIcs, Volume 223, 33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022)

We prove that the normalized edit distance proposed in [Marzal and Vidal 1993] is a metric when the cost of all the edit operations are the same. This closes a long standing gap in the literature where several authors noted that this distance does not satisfy the triangle inequality in the general case, and that it was not known whether it is satisfied in the uniform case - where all the edit costs are equal. We compare this metric to two normalized metrics proposed as alternatives in the literature, when people thought that Marzal’s and Vidal’s distance is not a metric, and identify key properties that explain why the original distance, now known to also be a metric, is better for some applications. Our examination is from a point of view of formal verification, but the properties and their significance are stated in an application agnostic way.

Dana Fisman, Joshua Grogin, Oded Margalit, and Gera Weiss. The Normalized Edit Distance with Uniform Operation Costs Is a Metric. In 33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 223, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fisman_et_al:LIPIcs.CPM.2022.17, author = {Fisman, Dana and Grogin, Joshua and Margalit, Oded and Weiss, Gera}, title = {{The Normalized Edit Distance with Uniform Operation Costs Is a Metric}}, booktitle = {33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022)}, pages = {17:1--17:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-234-1}, ISSN = {1868-8969}, year = {2022}, volume = {223}, editor = {Bannai, Hideo and Holub, Jan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2022.17}, URN = {urn:nbn:de:0030-drops-161446}, doi = {10.4230/LIPIcs.CPM.2022.17}, annote = {Keywords: edit distance, normalized distance, triangle inequality, metric} }

Document

**Published in:** LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

We study the learnability of symbolic finite state automata, a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all obtained results are positive. We provide a necessary condition for efficient learnability of SFAs in this paradigm, from which we obtain the first negative result. The main focus of our work lies in the learnability of SFAs under the paradigm of identification in the limit using polynomial time and data. We provide a necessary condition and a sufficient condition for efficient learnability of SFAs in this paradigm, from which we derive a positive and a negative result.

Dana Fisman, Hadar Frenkel, and Sandra Zilles. Inferring Symbolic Automata. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fisman_et_al:LIPIcs.CSL.2022.21, author = {Fisman, Dana and Frenkel, Hadar and Zilles, Sandra}, title = {{Inferring Symbolic Automata}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {21:1--21:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.21}, URN = {urn:nbn:de:0030-drops-157412}, doi = {10.4230/LIPIcs.CSL.2022.21}, annote = {Keywords: Symbolic Finite State Automata, Query Learning, Characteristic Sets} }

Document

**Published in:** LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

A Büchi automaton is strongly unambiguous if every word w ∈ Σ^ω has at most one final path. Many properties of strongly unambiguous Büchi automata (SUBAs) are known. They are fully expressive: every regular ω-language can be represented by a SUBA. Equivalence and containment of SUBAs can be decided in polynomial time. SUBAs may be exponentially smaller than deterministic Muller automata and may be exponentially bigger than deterministic Büchi automata. In this work we show that SUBAs can be learned in polynomial time using membership and certain non-proper equivalence queries, which implies that they are polynomially predictable with membership queries. In contrast, under plausible cryptographic assumptions, non-deterministic Büchi automata are not polynomially predictable with membership queries.

Dana Angluin, Timos Antonopoulos, and Dana Fisman. Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{angluin_et_al:LIPIcs.CSL.2020.8, author = {Angluin, Dana and Antonopoulos, Timos and Fisman, Dana}, title = {{Strongly Unambiguous B\"{u}chi Automata Are Polynomially Predictable With Membership Queries}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {8:1--8:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.8}, URN = {urn:nbn:de:0030-drops-116519}, doi = {10.4230/LIPIcs.CSL.2020.8}, annote = {Keywords: Polynomially predictable languages, Automata learning, Strongly unambiguous B\"{u}chi automata, Automata succinctness, Regular \omega-languages, Grammatical inference} }

Document

**Published in:** LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of omega-tree languages derived from weak regular omega-word languages in polynomial time. The method is a general polynomial time reduction
of learning a class of derived omega-tree languages to learning the underlying class of omega-word languages, for any class of omega-word languages recognized by a deterministic Büchi acceptor.
Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli [Maler and Pneuli, Inform. Comput., 1995]
for the class of weak regular omega-word languages yields the main result. We also show that subset queries that return counterexamples
can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or non-deterministic finite word acceptors, and deterministic or non-deterministic Büchi
omega-word acceptors.
A previous claim of an algorithm to learn regular omega-trees
due to Jayasrirani, Begam and Thomas [Jayasrirani et al., ICGI, 2008] is unfortunately incorrect, as shown in [Angluin, YALEU/DCS/TR-1528, 2016].

Dana Angluin, Timos Antonopoulos, and Dana Fisman. Query Learning of Derived Omega-Tree Languages in Polynomial Time. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{angluin_et_al:LIPIcs.CSL.2017.10, author = {Angluin, Dana and Antonopoulos, Timos and Fisman, Dana}, title = {{Query Learning of Derived Omega-Tree Languages in Polynomial Time}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {10:1--10:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.10}, URN = {urn:nbn:de:0030-drops-77022}, doi = {10.4230/LIPIcs.CSL.2017.10}, annote = {Keywords: Learning, queries, infinite trees, derived tree languages, reactive systems} }

Document

**Published in:** LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Families of DFAs (FDFAs) provide an alternative formalism for recognizing omega-regular languages. The motivation for introducing them was a desired correlation between the automaton states and right congruence relations, in a manner similar to the Myhill-Nerode theorem for regular languages. This correlation is beneficial for learning algorithms, and indeed it was recently shown that omega-regular languages can be learned from membership and equivalence queries, using FDFAs as the acceptors.
In this paper, we look into the question of how suitable FDFAs are for defining omega-regular languages. Specifically, we look into the complexity of performing Boolean operations, such as complementation and intersection, on FDFAs, the complexity of solving decision problems, such as emptiness and language containment, and the succinctness of FDFAs compared to standard deterministic and nondeterministic omega-automata.
We show that FDFAs enjoy the benefits of deterministic automata with respect to Boolean operations and decision problems. Namely, they can all be performed in nondeterministic logarithmic space.
We provide polynomial translations of deterministic Buchi and coBuchi automata to FDFAs and of FDFAs to nondeterministic Buchi automata (NBAs). We show that translation of an NBA to an FDFA may involve an exponential blowup. Last, we show that FDFAs are more succinct than deterministic parity automata (DPAs) in the sense that translating a DPA to an FDFA can always be done with only a polynomial increase, yet the other direction involves an inevitable exponential blowup in the worst case.

Dana Angluin, Udi Boker, and Dana Fisman. Families of DFAs as Acceptors of omega-Regular Languages. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{angluin_et_al:LIPIcs.MFCS.2016.11, author = {Angluin, Dana and Boker, Udi and Fisman, Dana}, title = {{Families of DFAs as Acceptors of omega-Regular Languages}}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)}, pages = {11:1--11:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-016-3}, ISSN = {1868-8969}, year = {2016}, volume = {58}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.11}, URN = {urn:nbn:de:0030-drops-64274}, doi = {10.4230/LIPIcs.MFCS.2016.11}, annote = {Keywords: finite automata, omega regular languages} }

Document

**Published in:** LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

The problem of Büchi determinization is a fundamental problem with important applications in reactive synthesis, multi-agent systems and probabilistic verification. The first asymptotically optimal Büchi determinization (a.k.a the Safra construction), was published in 1988. While asymptotically optimal, the Safra construction is notorious for its technical complexity and opaqueness in terms of intuition. While some improvements were published since the Safra construction, notably Kähler and Wilke’s construction, understanding the constructions remains a non-trivial task.
In this paper we present a modular approach to Büchi determinization, where the difficulties are addressed one at a time, rather than simultaneously, making the solutions natural and easy to understand. We build on the notion of the skeleton trees of Kähler and Wilke. We first show how to construct a deterministic automaton in the case the skeleton's width is one. Then we show how to construct a deterministic automaton in the case the skeleton's width is k (for any given k). The overall construction is obtained by running in parallel the automata for all widths.

Dana Fisman and Yoad Lustig. A Modular Approach for Büchi Determinization. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 368-382, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fisman_et_al:LIPIcs.CONCUR.2015.368, author = {Fisman, Dana and Lustig, Yoad}, title = {{A Modular Approach for B\"{u}chi Determinization}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {368--382}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-91-0}, ISSN = {1868-8969}, year = {2015}, volume = {42}, editor = {Aceto, Luca and de Frutos Escrig, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.368}, URN = {urn:nbn:de:0030-drops-53899}, doi = {10.4230/LIPIcs.CONCUR.2015.368}, annote = {Keywords: B\"{u}chi automata, Determinization, Verification, Games, Synthesis} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail