Found 2 Possible Name Variants:

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

The powerset monad on the category of sets does not distribute over itself. Nevertheless a weaker form of distributive law of the powerset monad over itself exists and it essentially stems from the canonical Egli-Milner extension of the powerset to the category of relations. On the other hand, any regular category yields a category of relations, and some regular categories also possess a powerset-like monad, as is the Vietoris monad on compact Hausdorff spaces. We derive the Egli-Milner extension in three different frameworks : sets, toposes, and compact Hausdorff spaces. We prove that it corresponds to a monotone weak distributive law in each case by showing that the multiplication extends to relations but the unit does not. We provide an application to coalgebraic determinization of alternating automata.

Alexandre Goy, Daniela Petrişan, and Marc Aiguier. Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 132:1-132:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{goy_et_al:LIPIcs.ICALP.2021.132, author = {Goy, Alexandre and Petri\c{s}an, Daniela and Aiguier, Marc}, title = {{Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces}}, booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)}, pages = {132:1--132:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-195-5}, ISSN = {1868-8969}, year = {2021}, volume = {198}, editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.132}, URN = {urn:nbn:de:0030-drops-142016}, doi = {10.4230/LIPIcs.ICALP.2021.132}, annote = {Keywords: Egli-Milner relation, weak extension, weak distributive law, weak lifting, powerset monad, Vietoris monad, topos, alternating automaton, generalized determinization} }

Document

**Published in:** LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

In this paper, we present a categorical approach to learning automata over words, in the sense of the L*-algorithm of Angluin. This yields a new generic L*-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a "computation category". We establish that the sufficient properties for yielding the existence of minimal automata (that were disclosed in a previous paper), in combination with some additional hypotheses relative to termination, ensure the correctness of our generic algorithm.

Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. Learning Automata and Transducers: A Categorical Approach. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CSL.2021.15, author = {Colcombet, Thomas and Petri\c{s}an, Daniela and Stabile, Riccardo}, title = {{Learning Automata and Transducers: A Categorical Approach}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.15}, URN = {urn:nbn:de:0030-drops-134498}, doi = {10.4230/LIPIcs.CSL.2021.15}, annote = {Keywords: Automata, transducer, learning, category} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way.
In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.

Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2018.17, author = {Bonchi, Filippo and K\"{o}nig, Barbara and Petrisan, Daniela}, title = {{Up-To Techniques for Behavioural Metrics via Fibrations}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {17:1--17:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17}, URN = {urn:nbn:de:0030-drops-95552}, doi = {10.4230/LIPIcs.CONCUR.2018.17}, annote = {Keywords: behavioural metrics, bisimilarity, up-to techniques, coalgebras, fibrations} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

In this paper we adopt a category-theoretic approach to the conception of automata classes enjoying minimization by design. The main instantiation of our construction is a new class of automata that are hybrid between deterministic automata and automata weighted over a field.

Thomas Colcombet and Daniela Petrisan. Automata in the Category of Glued Vector Spaces. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.MFCS.2017.52, author = {Colcombet, Thomas and Petrisan, Daniela}, title = {{Automata in the Category of Glued Vector Spaces}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {52:1--52:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.52}, URN = {urn:nbn:de:0030-drops-81324}, doi = {10.4230/LIPIcs.MFCS.2017.52}, annote = {Keywords: hybrid set-vector automata, automata minimization in a category} }

Document

**Published in:** LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as
functors from input categories that specify the type of the
languages and of the machines to categories that specify the type of
outputs.
Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be applied to several phenomena in automata theory, starting with determinization and
minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to
Choffrut's minimization algorithm for subsequential transducers and revisit Brzozowski's minimization algorithm.

Thomas Colcombet and Daniela Petrisan. Automata Minimization: a Functorial Approach. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CALCO.2017.8, author = {Colcombet, Thomas and Petrisan, Daniela}, title = {{Automata Minimization: a Functorial Approach}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.8}, URN = {urn:nbn:de:0030-drops-80484}, doi = {10.4230/LIPIcs.CALCO.2017.8}, annote = {Keywords: functor automata, minimization, Choffrut's minimization algorithm, subsequential transducers, Brzozowski's minimization algorithm} }

Document

**Published in:** LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Starting from Boolean algebras of languages closed under quotients and using duality theoretic insights, we derive the notion of Boolean spaces with internal monoids as recognisers for arbitrary formal languages of finite words over finite alphabets. This leads to recognisers and syntactic spaces in a setting that is well-suited for applying tools from Stone duality as applied in semantics.
The main focus of the paper is the development of topo-algebraic constructions pertinent to the treatment of languages given by logic formulas. In particular, using the standard semantic view of quantification as projection, we derive a notion of Schützenberger product for Boolean spaces with internal monoids. This makes heavy use of the Vietoris construction - and its dual functor - which is central to the coalgebraic treatment of classical modal logic.
We show that the unary Schützenberger product for spaces yields a recogniser for the language of all models of the formula EXISTS x.phi(x), when applied to a recogniser for the language of all models of phi(x). Further, we generalise global and local versions of the theorems of Schützenberger and Reutenauer characterising the languages recognised by the binary Schützenberger product.
Finally, we provide an equational characterisation of Boolean algebras obtained by local Schützenberger product with the one element space based on an Egli-Milner type condition on generalised factorisations of ultrafilters on words.

Mai Gehrke, Daniela Petrisan, and Luca Reggio. The Schützenberger Product for Syntactic Spaces. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 112:1-112:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{gehrke_et_al:LIPIcs.ICALP.2016.112, author = {Gehrke, Mai and Petrisan, Daniela and Reggio, Luca}, title = {{The Sch\"{u}tzenberger Product for Syntactic Spaces}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {112:1--112:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.112}, URN = {urn:nbn:de:0030-drops-62474}, doi = {10.4230/LIPIcs.ICALP.2016.112}, annote = {Keywords: Stone duality and Stone-Cech compactification, Vietoris hyperspace construction, logic on words, algebraic language theory beyond the regular setting} }

Document

**Published in:** LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.

Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 205-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kurz_et_al:LIPIcs.CALCO.2015.205, author = {Kurz, Alexander and Pardo, Alberto and Petrisan, Daniela and Severi, Paula and de Vries, Fer-Jan}, title = {{Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes}}, booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)}, pages = {205--220}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-84-2}, ISSN = {1868-8969}, year = {2015}, volume = {35}, editor = {Moss, Lawrence S. and Sobocinski, Pawel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.205}, URN = {urn:nbn:de:0030-drops-55351}, doi = {10.4230/LIPIcs.CALCO.2015.205}, annote = {Keywords: coalgebra, Bekic lemma, infinite data, functional programming, type theory} }

Document

**Published in:** LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.

Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gabbay_et_al:LIPIcs.CSL.2015.374, author = {Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela}, title = {{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {374--389}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374}, URN = {urn:nbn:de:0030-drops-54262}, doi = {10.4230/LIPIcs.CSL.2015.374}, annote = {Keywords: nominal sets, scope, alpha equivalence, dynamic sequences} }

Document

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

Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered setting.

Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 240-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2015.240, author = {Bonchi, Filippo and Petrisan, Daniela and Pous, Damien and Rot, Jurriaan}, title = {{Lax Bialgebras and Up-To Techniques for Weak Bisimulations}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {240--253}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.240}, URN = {urn:nbn:de:0030-drops-53709}, doi = {10.4230/LIPIcs.CONCUR.2015.240}, annote = {Keywords: Up-to techniques, weak bisimulation, (lax) bialgebras} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

The powerset monad on the category of sets does not distribute over itself. Nevertheless a weaker form of distributive law of the powerset monad over itself exists and it essentially stems from the canonical Egli-Milner extension of the powerset to the category of relations. On the other hand, any regular category yields a category of relations, and some regular categories also possess a powerset-like monad, as is the Vietoris monad on compact Hausdorff spaces. We derive the Egli-Milner extension in three different frameworks : sets, toposes, and compact Hausdorff spaces. We prove that it corresponds to a monotone weak distributive law in each case by showing that the multiplication extends to relations but the unit does not. We provide an application to coalgebraic determinization of alternating automata.

Alexandre Goy, Daniela Petrişan, and Marc Aiguier. Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 132:1-132:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{goy_et_al:LIPIcs.ICALP.2021.132, author = {Goy, Alexandre and Petri\c{s}an, Daniela and Aiguier, Marc}, title = {{Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces}}, booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)}, pages = {132:1--132:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-195-5}, ISSN = {1868-8969}, year = {2021}, volume = {198}, editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.132}, URN = {urn:nbn:de:0030-drops-142016}, doi = {10.4230/LIPIcs.ICALP.2021.132}, annote = {Keywords: Egli-Milner relation, weak extension, weak distributive law, weak lifting, powerset monad, Vietoris monad, topos, alternating automaton, generalized determinization} }

Document

**Published in:** LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

In this paper, we present a categorical approach to learning automata over words, in the sense of the L*-algorithm of Angluin. This yields a new generic L*-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a "computation category". We establish that the sufficient properties for yielding the existence of minimal automata (that were disclosed in a previous paper), in combination with some additional hypotheses relative to termination, ensure the correctness of our generic algorithm.

Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. Learning Automata and Transducers: A Categorical Approach. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CSL.2021.15, author = {Colcombet, Thomas and Petri\c{s}an, Daniela and Stabile, Riccardo}, title = {{Learning Automata and Transducers: A Categorical Approach}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.15}, URN = {urn:nbn:de:0030-drops-134498}, doi = {10.4230/LIPIcs.CSL.2021.15}, annote = {Keywords: Automata, transducer, learning, category} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way.
In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.

Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2018.17, author = {Bonchi, Filippo and K\"{o}nig, Barbara and Petrisan, Daniela}, title = {{Up-To Techniques for Behavioural Metrics via Fibrations}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {17:1--17:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17}, URN = {urn:nbn:de:0030-drops-95552}, doi = {10.4230/LIPIcs.CONCUR.2018.17}, annote = {Keywords: behavioural metrics, bisimilarity, up-to techniques, coalgebras, fibrations} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

In this paper we adopt a category-theoretic approach to the conception of automata classes enjoying minimization by design. The main instantiation of our construction is a new class of automata that are hybrid between deterministic automata and automata weighted over a field.

Thomas Colcombet and Daniela Petrisan. Automata in the Category of Glued Vector Spaces. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.MFCS.2017.52, author = {Colcombet, Thomas and Petrisan, Daniela}, title = {{Automata in the Category of Glued Vector Spaces}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {52:1--52:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.52}, URN = {urn:nbn:de:0030-drops-81324}, doi = {10.4230/LIPIcs.MFCS.2017.52}, annote = {Keywords: hybrid set-vector automata, automata minimization in a category} }

Document

**Published in:** LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as
functors from input categories that specify the type of the
languages and of the machines to categories that specify the type of
outputs.
Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be applied to several phenomena in automata theory, starting with determinization and
minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to
Choffrut's minimization algorithm for subsequential transducers and revisit Brzozowski's minimization algorithm.

Thomas Colcombet and Daniela Petrisan. Automata Minimization: a Functorial Approach. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CALCO.2017.8, author = {Colcombet, Thomas and Petrisan, Daniela}, title = {{Automata Minimization: a Functorial Approach}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.8}, URN = {urn:nbn:de:0030-drops-80484}, doi = {10.4230/LIPIcs.CALCO.2017.8}, annote = {Keywords: functor automata, minimization, Choffrut's minimization algorithm, subsequential transducers, Brzozowski's minimization algorithm} }

Document

**Published in:** LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Starting from Boolean algebras of languages closed under quotients and using duality theoretic insights, we derive the notion of Boolean spaces with internal monoids as recognisers for arbitrary formal languages of finite words over finite alphabets. This leads to recognisers and syntactic spaces in a setting that is well-suited for applying tools from Stone duality as applied in semantics.
The main focus of the paper is the development of topo-algebraic constructions pertinent to the treatment of languages given by logic formulas. In particular, using the standard semantic view of quantification as projection, we derive a notion of Schützenberger product for Boolean spaces with internal monoids. This makes heavy use of the Vietoris construction - and its dual functor - which is central to the coalgebraic treatment of classical modal logic.
We show that the unary Schützenberger product for spaces yields a recogniser for the language of all models of the formula EXISTS x.phi(x), when applied to a recogniser for the language of all models of phi(x). Further, we generalise global and local versions of the theorems of Schützenberger and Reutenauer characterising the languages recognised by the binary Schützenberger product.
Finally, we provide an equational characterisation of Boolean algebras obtained by local Schützenberger product with the one element space based on an Egli-Milner type condition on generalised factorisations of ultrafilters on words.

Mai Gehrke, Daniela Petrisan, and Luca Reggio. The Schützenberger Product for Syntactic Spaces. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 112:1-112:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{gehrke_et_al:LIPIcs.ICALP.2016.112, author = {Gehrke, Mai and Petrisan, Daniela and Reggio, Luca}, title = {{The Sch\"{u}tzenberger Product for Syntactic Spaces}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {112:1--112:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.112}, URN = {urn:nbn:de:0030-drops-62474}, doi = {10.4230/LIPIcs.ICALP.2016.112}, annote = {Keywords: Stone duality and Stone-Cech compactification, Vietoris hyperspace construction, logic on words, algebraic language theory beyond the regular setting} }

Document

**Published in:** LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.

Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 205-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kurz_et_al:LIPIcs.CALCO.2015.205, author = {Kurz, Alexander and Pardo, Alberto and Petrisan, Daniela and Severi, Paula and de Vries, Fer-Jan}, title = {{Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes}}, booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)}, pages = {205--220}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-84-2}, ISSN = {1868-8969}, year = {2015}, volume = {35}, editor = {Moss, Lawrence S. and Sobocinski, Pawel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.205}, URN = {urn:nbn:de:0030-drops-55351}, doi = {10.4230/LIPIcs.CALCO.2015.205}, annote = {Keywords: coalgebra, Bekic lemma, infinite data, functional programming, type theory} }

Document

**Published in:** LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.

Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gabbay_et_al:LIPIcs.CSL.2015.374, author = {Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela}, title = {{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {374--389}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374}, URN = {urn:nbn:de:0030-drops-54262}, doi = {10.4230/LIPIcs.CSL.2015.374}, annote = {Keywords: nominal sets, scope, alpha equivalence, dynamic sequences} }

Document

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

Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered setting.

Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 240-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2015.240, author = {Bonchi, Filippo and Petrisan, Daniela and Pous, Damien and Rot, Jurriaan}, title = {{Lax Bialgebras and Up-To Techniques for Weak Bisimulations}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {240--253}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.240}, URN = {urn:nbn:de:0030-drops-53709}, doi = {10.4230/LIPIcs.CONCUR.2015.240}, annote = {Keywords: Up-to techniques, weak bisimulation, (lax) bialgebras} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail