30 Search Results for "Sokolova, Ana"

Volume

LIPIcs, Volume 139

8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

CALCO 2019, June 3-6, 2019, London, United Kingdom

Editors: Markus Roggenbach and Ana Sokolova

Document
DOI: 10.4230/DagRep.12.12.27
Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492)

Authors: Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova

Published in: Dagstuhl Reports, Volume 12, Issue 12 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22492 "Formal Methods and Distributed Computing: Stronger Together", held in December 2022.
Cite as

Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova. Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492). In Dagstuhl Reports, Volume 12, Issue 12, pp. 27-53, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{attiya_et_al:DagRep.12.12.27,
  author =	{Attiya, Hagit and Enea, Constantin and Rajsbaum, Sergio and Sokolova, Ana},
  title =	{{Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492)}},
  pages =	{27--53},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{12},
  editor =	{Attiya, Hagit and Enea, Constantin and Rajsbaum, Sergio and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.12.27},
  URN =		{urn:nbn:de:0030-drops-178452},
  doi =		{10.4230/DagRep.12.12.27},
  annote =	{Keywords: automated verification and reasoning, concurrent data structures and transactions, distributed algorithms, large-scale replication}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2022.1
CONCUR Test-Of-Time Award 2022 (Invited Paper)

Authors: Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.
Cite as

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi. CONCUR Test-Of-Time Award 2022 (Invited Paper). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1:1-1:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{castellani_et_al:LIPIcs.CONCUR.2022.1,
  author =	{Castellani, Ilaria and Gastin, Paul and Kupferman, Orna and Randour, Mickael and Sangiorgi, Davide},
  title =	{{CONCUR Test-Of-Time Award 2022}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{1:1--1:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.1},
  URN =		{urn:nbn:de:0030-drops-170644},
  doi =		{10.4230/LIPIcs.CONCUR.2022.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.11
Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls)

Authors: Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We prove that every finitely generated convex set of finitely supported probability distributions has a unique base. We apply this result to provide an alternative proof of a recent result: the algebraic theory of convex semilattices presents the monad of convex sets of probability distributions.
Cite as

Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 11:1-11:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.11,
  author =	{Bonchi, Filippo and Sokolova, Ana and Vignudelli, Valeria},
  title =	{{Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11},
  URN =		{urn:nbn:de:0030-drops-153666},
  doi =		{10.4230/LIPIcs.CALCO.2021.11},
  annote =	{Keywords: Convex sets of distributions monad, Convex semilattices, Unique base}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.23
Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls)

Authors: Ana Sokolova and Harald Woracek

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We reprove the countable splitting lemma by adapting Nawrotzki’s algorithm which produces a sequence that converges to a solution. Our algorithm combines Nawrotzki’s approach with taking finite cuts. It is constructive in the sense that each term of the iteratively built approximating sequence as well as the error between the approximants and the solution is computable with finitely many algebraic operations.
Cite as

Ana Sokolova and Harald Woracek. Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 23:1-23:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{sokolova_et_al:LIPIcs.CALCO.2021.23,
  author =	{Sokolova, Ana and Woracek, Harald},
  title =	{{Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.23},
  URN =		{urn:nbn:de:0030-drops-153781},
  doi =		{10.4230/LIPIcs.CALCO.2021.23},
  annote =	{Keywords: countable splitting lemma, distributions with given marginals, couplings}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CALCO.2019
LIPIcs, Volume 139, CALCO'19, Complete Volume

Authors: Markus Roggenbach and Ana Sokolova

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
LIPIcs, Volume 139, CALCO'19, Complete Volume
Cite as

Markus Roggenbach and Ana Sokolova. LIPIcs, Volume 139, CALCO'19, Complete Volume. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{roggenbach_et_al:LIPIcs.CALCO.2019,
  title =	{{LIPIcs, Volume 139, CALCO'19, Complete Volume}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019},
  URN =		{urn:nbn:de:0030-drops-115619},
  doi =		{10.4230/LIPIcs.CALCO.2019},
  annote =	{Keywords: Theory of computation, Models of computation; Modal and temporal logics; Algebraic semantics; Categorical semantics, Quantum computation theory; Software and its engineering, Specification languages}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CALCO.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Markus Roggenbach and Ana Sokolova

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Markus Roggenbach and Ana Sokolova. Front Matter, Table of Contents, Preface, Conference Organization. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 0:i-0:x, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{roggenbach_et_al:LIPIcs.CALCO.2019.0,
  author =	{Roggenbach, Markus and Sokolova, Ana},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.0},
  URN =		{urn:nbn:de:0030-drops-114282},
  doi =		{10.4230/LIPIcs.CALCO.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.1
Matching mu-Logic: Foundation of K Framework (Invited Paper)

Authors: Xiaohong Chen and Grigore Roşu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.
Cite as

Xiaohong Chen and Grigore Roşu. Matching mu-Logic: Foundation of K Framework (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 1:1-1:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CALCO.2019.1,
  author =	{Chen, Xiaohong and Ro\c{s}u, Grigore},
  title =	{{Matching mu-Logic: Foundation of K Framework}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.1},
  URN =		{urn:nbn:de:0030-drops-114296},
  doi =		{10.4230/LIPIcs.CALCO.2019.1},
  annote =	{Keywords: Matching mu-logic, Program verification, Reachability logic}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.2
From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper)

Authors: Stefan Milius

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
This extended abstract first presents a new category theoretic approach to equationally axiomatizable classes of algebras. This approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. We present a generic HSP theorem and a sound and complete equational logic, which encompass numerous flavors of equational axiomizations studied in the literature. In addition, we use the generic HSP theorem as a key ingredient to obtain Eilenberg-type correspondences yielding algebraic characterizations of properties of regular machine behaviours. When instantiated for orbit-finite nominal monoids, the generic HSP theorem yields a crucial step for the proof of the first Eilenberg-type variety theorem for data languages.
Cite as

Stefan Milius. From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 2:1-2:5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{milius:LIPIcs.CALCO.2019.2,
  author =	{Milius, Stefan},
  title =	{{From Equational Specifications of Algebras with Structure to Varieties of Data Languages}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{2:1--2:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.2},
  URN =		{urn:nbn:de:0030-drops-114309},
  doi =		{10.4230/LIPIcs.CALCO.2019.2},
  annote =	{Keywords: Birkhoff theorem, Equational logic, Eilenberg theorem, Data languages}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.3
Principles of Natural Language, Logic, and Tensor Semantics (Invited Paper)

Authors: Mehrnoosh Sadrzadeh

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
Residuated monoids model the structure of sentences. Vectors provide meaning representations for words. A functorial mapping between the two is obtained by lifting the vectors to tensors. The resulting sentence representations solve similarity, disambiguation and entailment tasks.
Cite as

Mehrnoosh Sadrzadeh. Principles of Natural Language, Logic, and Tensor Semantics (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 3:1-3:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sadrzadeh:LIPIcs.CALCO.2019.3,
  author =	{Sadrzadeh, Mehrnoosh},
  title =	{{Principles of Natural Language, Logic, and Tensor Semantics}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{3:1--3:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.3},
  URN =		{urn:nbn:de:0030-drops-114312},
  doi =		{10.4230/LIPIcs.CALCO.2019.3},
  annote =	{Keywords: Residuated Monoids, Vector Space Semantics, Corpora of Textual Data, Sentence Similarity and Disambiguation}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.4
Coinduction: Automata, Formal Proof, Companions (Invited Paper)

Authors: Damien Pous

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
Coinduction is a mathematical tool that is used pervasively in computer science: to program and reason about infinite data-structures, to give semantics to concurrent systems, to obtain automata algorithms. We present some of these applications in automata theory and in formalised mathematics. Then we discuss recent developments on the abstract theory of coinduction and its enhancements.
Cite as

Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 4:1-4:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{pous:LIPIcs.CALCO.2019.4,
  author =	{Pous, Damien},
  title =	{{Coinduction: Automata, Formal Proof, Companions}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{4:1--4:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.4},
  URN =		{urn:nbn:de:0030-drops-114323},
  doi =		{10.4230/LIPIcs.CALCO.2019.4},
  annote =	{Keywords: Coinduction, Automata, Coalgebra, Formal proofs}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.5
Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages

Authors: Vincenzo Ciancia and Yde Venema

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
In this work, we provide a simple coalgebraic characterisation of regular omega-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Omega-automata. In earlier work we introduced Omega-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Omega-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Omega-automata are expressively complete for the regular omega-languages. We show that, due to their coalgebraic nature, Omega-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Omega-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular omega-languages.
Cite as

Vincenzo Ciancia and Yde Venema. Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 5:1-5:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ciancia_et_al:LIPIcs.CALCO.2019.5,
  author =	{Ciancia, Vincenzo and Venema, Yde},
  title =	{{Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.5},
  URN =		{urn:nbn:de:0030-drops-114338},
  doi =		{10.4230/LIPIcs.CALCO.2019.5},
  annote =	{Keywords: omega-automata, regular omega-languages, coalgebra, streams, bisimilarity}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.6
Tree Automata as Algebras: Minimisation and Determinisation

Authors: Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We study a categorical generalisation of tree automata, as algebras for a fixed endofunctor endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.
Cite as

Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva. Tree Automata as Algebras: Minimisation and Determinisation. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 6:1-6:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{vanheerdt_et_al:LIPIcs.CALCO.2019.6,
  author =	{van Heerdt, Gerco and Kapp\'{e}, Tobias and Rot, Jurriaan and Sammartino, Matteo and Silva, Alexandra},
  title =	{{Tree Automata as Algebras: Minimisation and Determinisation}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.6},
  URN =		{urn:nbn:de:0030-drops-114341},
  doi =		{10.4230/LIPIcs.CALCO.2019.6},
  annote =	{Keywords: tree automata, algebras, minimisation, determinisation, Nerode equivalence}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.7
Coalgebraic Geometric Logic

Authors: Nick Bezhanishvili, Jim de Groot, and Yde Venema

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
Using the theory of coalgebra, we introduce a uniform framework for adding modalities to the language of propositional geometric logic. Models for this logic are based on coalgebras for an endofunctor T on some full subcategory of the category Top of topological spaces and continuous functions. We compare the notions of modal equivalence, behavioural equivalence and bisimulation on the resulting class of models, and we provide a final object for the corresponding category. Furthermore, we specify a method of lifting an endofunctor on Set, accompanied by a collection of predicate liftings, to an endofunctor on the category of topological spaces.
Cite as

Nick Bezhanishvili, Jim de Groot, and Yde Venema. Coalgebraic Geometric Logic. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 7:1-7:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bezhanishvili_et_al:LIPIcs.CALCO.2019.7,
  author =	{Bezhanishvili, Nick and de Groot, Jim and Venema, Yde},
  title =	{{Coalgebraic Geometric Logic}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.7},
  URN =		{urn:nbn:de:0030-drops-114354},
  doi =		{10.4230/LIPIcs.CALCO.2019.7},
  annote =	{Keywords: Coalgebra, Geometric Logic, Modal Logic, Topology}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.8
Coinduction in Flow: The Later Modality in Fibrations

Authors: Henning Basold

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This enables easily understandable coinductive proofs and programs, and fosters automatic proof search. Part of the framework are also various results that enable a wide range of applications: transportation of (co)limits, exponentials, fibred adjunctions and first-order connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any first-order logic with the later modality. Moreover, we obtain soundness and completeness results, and can use up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal mu-calculus. Finally, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results.
Cite as

Henning Basold. Coinduction in Flow: The Later Modality in Fibrations. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 8:1-8:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{basold:LIPIcs.CALCO.2019.8,
  author =	{Basold, Henning},
  title =	{{Coinduction in Flow: The Later Modality in Fibrations}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{8:1--8:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.8},
  URN =		{urn:nbn:de:0030-drops-114369},
  doi =		{10.4230/LIPIcs.CALCO.2019.8},
  annote =	{Keywords: Coinduction, Fibrations, Later Modality, Recursive Proofs, Up-to techniques, Probabilistic Logic, Probabilistic Programming}
}
  • Refine by Author
  • 8 Sokolova, Ana
  • 3 Bonchi, Filippo
  • 2 Roggenbach, Markus
  • 2 Silva, Alexandra
  • 2 Sobociński, Paweł
  • Show More...

  • Refine by Classification
  • 9 Theory of computation → Categorical semantics
  • 7 Theory of computation → Logic
  • 3 Software and its engineering → Specification languages
  • 3 Theory of computation → Algebraic semantics
  • 3 Theory of computation → Formal languages and automata theory
  • Show More...

  • Refine by Keyword
  • 2 Coalgebra
  • 2 Coinduction
  • 2 coalgebra
  • 2 convex algebra
  • 2 convex powerset monad
  • Show More...

  • Refine by Type
  • 29 document
  • 1 volume

  • Refine by Publication Year
  • 23 2019
  • 2 2017
  • 2 2021
  • 1 2016
  • 1 2022
  • Show More...

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact