DROPS

Volume

LIPIcs, Volume 35

6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands

Editors: Lawrence S. Moss and Pawel Sobocinski

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2024.41

Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)

Authors: Sam Ezeh

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

We present Untangle, a Lean4 extension for Visual Studio Code that displays string diagrams for morphisms inside monoidal categories, allowing users to rewrite expressions by clicking on natural transformations and morphisms in the string diagram. When the the user manipulates the string diagram by clicking on natural transformations in the Graphical User Interface, it attempts to generate relevant tactics to apply which it then inserts into the editor, allowing the user to prove equalities visually by diagram rewriting.

Cite as

Sam Ezeh. Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 41:1-41:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ezeh:LIPIcs.ITP.2024.41,
  author =	{Ezeh, Sam},
  title =	{{Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{41:1--41:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41},
  URN =		{urn:nbn:de:0030-drops-207690},
  doi =		{10.4230/LIPIcs.ITP.2024.41},
  annote =	{Keywords: Interactive theorem proving, Lean4, Graphical User Interface}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.11

Left-Linear Rewriting in Adhesive Categories

Authors: Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of many formalisms. We investigate the issue in the context of the double pushout approach to rewriting in the general setting of adhesive categories. While a consolidated theory exists for linear rules, which can consume, preserve and generate entities, this paper focuses on left-linear rules which may also "merge" parts of the state. This is an apparently minimal, yet technically hard enhancement, since a standard characterisation of independence that - in the linear case - allows one to derive a number of properties, essential in the development of a theory of concurrency, no longer holds. The paper performs an in-depth study of the notion of independence for left-linear rules: it introduces a novel characterisation of independence, identifies well-behaved classes of left-linear rewriting systems, and provides some fundamental results including a Church-Rosser property and the existence of canonical equivalence proofs for concurrent computations. These results properly extends the class of formalisms that can be modelled in the adhesive framework.

Cite as

Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci. Left-Linear Rewriting in Adhesive Categories. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CONCUR.2024.11,
  author =	{Baldan, Paolo and Castelnovo, Davide and Corradini, Andrea and Gadducci, Fabio},
  title =	{{Left-Linear Rewriting in Adhesive Categories}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{11:1--11:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.11},
  URN =		{urn:nbn:de:0030-drops-207835},
  doi =		{10.4230/LIPIcs.CONCUR.2024.11},
  annote =	{Keywords: Adhesive categories, double-pushout rewriting, left-linear rules, switch equivalence, local Church-Rosser property}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.12

History-Determinism vs Fair Simulation

Authors: Udi Boker, Thomas A. Henzinger, Karoliina Lehtinen, and Aditya Prakash

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

An automaton 𝒜 is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton 𝒜 is guidable with respect to a class C of automata if it can fairly simulate every automaton in C, whose language is contained in that of 𝒜. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking. We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes. We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are ω-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata. We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.

Cite as

Udi Boker, Thomas A. Henzinger, Karoliina Lehtinen, and Aditya Prakash. History-Determinism vs Fair Simulation. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.CONCUR.2024.12,
  author =	{Boker, Udi and Henzinger, Thomas A. and Lehtinen, Karoliina and Prakash, Aditya},
  title =	{{History-Determinism vs Fair Simulation}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.12},
  URN =		{urn:nbn:de:0030-drops-207841},
  doi =		{10.4230/LIPIcs.CONCUR.2024.12},
  annote =	{Keywords: History-Determinism}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.29

Strategic Dominance: A New Preorder for Nondeterministic Processes

Authors: Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.

Cite as

Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Strategic Dominance: A New Preorder for Nondeterministic Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2024.29,
  author =	{Henzinger, Thomas A. and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Strategic Dominance: A New Preorder for Nondeterministic Processes}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.29},
  URN =		{urn:nbn:de:0030-drops-208011},
  doi =		{10.4230/LIPIcs.CONCUR.2024.29},
  annote =	{Keywords: quantitative automata, refinement relation, resolver, strategy, history-determinism}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.34

On Continuous Pushdown VASS in One Dimension

Authors: Guillermo A. Pérez and Shrisha Rao

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer variables. Unfortunately, reachability analysis, even for one-dimensional PVASS is not known to be decidable. So, we relax the model of one-dimensional PVASS to make the counter updates continuous and show that in this case reachability, coverability, and boundedness are decidable in polynomial time. In addition, for the extension of the model with lower-bound guards on the states, we show that coverability and reachability are NP-complete, and boundedness is coNP-complete.

Cite as

Guillermo A. Pérez and Shrisha Rao. On Continuous Pushdown VASS in One Dimension. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CONCUR.2024.34,
  author =	{P\'{e}rez, Guillermo A. and Rao, Shrisha},
  title =	{{On Continuous Pushdown VASS in One Dimension}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{34:1--34:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.34},
  URN =		{urn:nbn:de:0030-drops-208065},
  doi =		{10.4230/LIPIcs.CONCUR.2024.34},
  annote =	{Keywords: Vector addition systems, Pushdown automata, Reachability}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.39

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

Authors: Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.

Cite as

Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas. Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{stoltenow_et_al:LIPIcs.CONCUR.2024.39,
  author =	{Stoltenow, Lara and K\"{o}nig, Barbara and Schneider, Sven and Corradini, Andrea and Lambers, Leen and Orejas, Fernando},
  title =	{{Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.39},
  URN =		{urn:nbn:de:0030-drops-208113},
  doi =		{10.4230/LIPIcs.CONCUR.2024.39},
  annote =	{Keywords: satisfiability, graph conditions, coinductive techniques, category theory}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2024.23

Minimizing Cost Register Automata over a Field

Authors: Yahia Idriss Benalioua, Nathan Lhote, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract

Weighted automata (WA) are an extension of finite automata that define functions from words to values in a given semiring. An alternative deterministic model, called Cost Register Automata (CRA), was introduced by Alur et al. It enriches deterministic finite automata with a finite number of registers, which store values, updated at each transition using the operations of the semiring. It is known that CRA with register updates defined by linear maps have the same expressiveness as WA. Previous works have studied the register minimization problem: given a function computable by a WA and an integer k, is it possible to realize it using a CRA with at most k registers? In this paper, we solve this problem for CRA over a field with linear register updates, using the notion of linear hull, an algebraic invariant of WA introduced recently by Bell and Smertnig. We then generalise the approach to solve a more challenging problem, that consists in minimizing simultaneously the number of states and that of registers. In addition, we also lift our results to the setting of CRA with affine updates. Last, while the linear hull was recently shown to be computable by Bell and Smertnig, no complexity bounds were given. To fill this gap, we provide two new algorithms to compute invariants of WA. This allows us to show that the register (resp. state-register) minimization problem can be solved in 2-ExpTime (resp. in NExpTime).

Cite as

Yahia Idriss Benalioua, Nathan Lhote, and Pierre-Alain Reynier. Minimizing Cost Register Automata over a Field. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{benalioua_et_al:LIPIcs.MFCS.2024.23,
  author =	{Benalioua, Yahia Idriss and Lhote, Nathan and Reynier, Pierre-Alain},
  title =	{{Minimizing Cost Register Automata over a Field}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.23},
  URN =		{urn:nbn:de:0030-drops-205798},
  doi =		{10.4230/LIPIcs.MFCS.2024.23},
  annote =	{Keywords: Weighted automata, Cost Register automata, Zariski topology}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2024.30

When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines

Authors: Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract

Fo-bicategories are a categorification of Peirce’s calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere’s hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.

Cite as

Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.MFCS.2024.30,
  author =	{Bonchi, Filippo and Di Giorgio, Alessandro and Trotta, Davide},
  title =	{{When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.30},
  URN =		{urn:nbn:de:0030-drops-205867},
  doi =		{10.4230/LIPIcs.MFCS.2024.30},
  annote =	{Keywords: relational algebra, hyperdoctrines, cartesian bicategories, string diagrams}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2024.5

The Flower Calculus

Authors: Pablo Donato

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.

Cite as

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{donato:LIPIcs.FSCD.2024.5,
  author =	{Donato, Pablo},
  title =	{{The Flower Calculus}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.5},
  URN =		{urn:nbn:de:0030-drops-203343},
  doi =		{10.4230/LIPIcs.FSCD.2024.5},
  annote =	{Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2024.17

A Categorical Approach to DIBI Models

Authors: Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

The logic of Dependence and Independence Bunched Implications (DIBI) is a logic to reason about conditional independence (CI); for instance, DIBI formulas can characterise CI in discrete probability distributions and in relational databases, using a probabilistic DIBI model and a similarly-constructed relational model. Despite the similarity of the two models, there lacks a uniform account. As a result, the laborious case-by-case verification of the frame conditions required for constructing new models hinders them from generalising the results to CI in other useful models such that continuous distribution. In this paper, we develop an abstract framework for systematically constructing DIBI models, using category theory as the unifying mathematical language. We show that DIBI models arise from arbitrary symmetric monoidal categories with copy-discard structure. In particular, we use string diagrams - a graphical presentation of monoidal categories - to give a uniform definition of the parallel composition and subkernel relation in DIBI models. Our approach not only generalises known models, but also yields new models of interest and reduces properties of DIBI models to structures in the underlying categories. Furthermore, our categorical framework enables a comparison between string diagrammatic approaches to CI in the literature and a logical notion of CI, defined in terms of the satisfaction of specific DIBI formulas. We show that the logical notion is an extension of string diagrammatic CI under reasonable conditions.

Cite as

Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi. A Categorical Approach to DIBI Models. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gu_et_al:LIPIcs.FSCD.2024.17,
  author =	{Gu, Tao and Bao, Jialu and Hsu, Justin and Silva, Alexandra and Zanasi, Fabio},
  title =	{{A Categorical Approach to DIBI Models}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.17},
  URN =		{urn:nbn:de:0030-drops-203469},
  doi =		{10.4230/LIPIcs.FSCD.2024.17},
  annote =	{Keywords: Conditional Independence, Dependence Independence Bunched Implications, String Diagrams, Markov Categories}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2024.30

homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories

Authors: Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.

Cite as

Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{corbyn_et_al:LIPIcs.FSCD.2024.30,
  author =	{Corbyn, Nathan and Heidemann, Lukas and Hu, Nick and Sarti, Chiara and Tataru, Calin and Vicary, Jamie},
  title =	{{homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{30:1--30:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.30},
  URN =		{urn:nbn:de:0030-drops-203594},
  doi =		{10.4230/LIPIcs.FSCD.2024.30},
  annote =	{Keywords: Higher category theory, proof assistant, string diagrams}
}

Document

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

DOI: 10.4230/LIPIcs.ICALP.2024.149

A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions

Authors: Wojciech Różowski

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract

Deterministic automata have been traditionally studied through the point of view of language equivalence, but another perspective is given by the canonical notion of shortest-distinguishing-word distance quantifying the of states. Intuitively, the longer the word needed to observe a difference between two states, then the closer their behaviour is. In this paper, we give a sound and complete axiomatisation of shortest-distinguishing-word distance between regular languages. Our axiomatisation relies on a recently developed quantitative analogue of equational logic, allowing to manipulate rational-indexed judgements of the form e ≡_ε f meaning term e is approximately equivalent to term f within the error margin of ε. The technical core of the paper is dedicated to the completeness argument that draws techniques from order theory and Banach spaces to simplify the calculation of the behavioural distance to the point it can be then mimicked by axiomatic reasoning.

Cite as

Wojciech Różowski. A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 149:1-149:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{rozowski:LIPIcs.ICALP.2024.149,
  author =	{R\'{o}\.{z}owski, Wojciech},
  title =	{{A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{149:1--149:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.149},
  URN =		{urn:nbn:de:0030-drops-202920},
  doi =		{10.4230/LIPIcs.ICALP.2024.149},
  annote =	{Keywords: Regular Expressions, Behavioural Distances, Quantitative Equational Theories}
}

Document

DOI: 10.4230/LIPIcs.CSL.2024.25

The Produoidal Algebra of Process Decomposition

Authors: Matt Earnshaw, James Hefford, and Mario Román

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

We characterize a universal normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. In particular, symmetric monoidal contexts coincide with monoidal lenses and endow them with a novel universal property. We apply this algebraic structure to the analysis of multi-party protocols in arbitrary theories of processes.

Cite as

Matt Earnshaw, James Hefford, and Mario Román. The Produoidal Algebra of Process Decomposition. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.CSL.2024.25,
  author =	{Earnshaw, Matt and Hefford, James and Rom\'{a}n, Mario},
  title =	{{The Produoidal Algebra of Process Decomposition}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello 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.CSL.2024.25},
  URN =		{urn:nbn:de:0030-drops-196688},
  doi =		{10.4230/LIPIcs.CSL.2024.25},
  annote =	{Keywords: monoidal categories, profunctors, lenses, duoidal categories}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2023.43

String Diagrammatic Trace Theory

Authors: Matthew Earnshaw and Paweł Sobociński

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract

We extend the theory of formal languages in monoidal categories to the multi-sorted, symmetric case, and show how this theory permits a graphical treatment of topics in concurrency. In particular, we show that Mazurkiewicz trace languages are precisely symmetric monoidal languages over monoidal distributed alphabets. We introduce symmetric monoidal automata, which define the class of regular symmetric monoidal languages. Furthermore, we prove that Zielonka’s asynchronous automata coincide with symmetric monoidal automata over monoidal distributed alphabets. Finally, we apply the string diagrams for symmetric premonoidal categories to derive serializations of traces.

Cite as

Matthew Earnshaw and Paweł Sobociński. String Diagrammatic Trace Theory. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 43:1-43:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.MFCS.2023.43,
  author =	{Earnshaw, Matthew and Soboci\'{n}ski, Pawe{\l}},
  title =	{{String Diagrammatic Trace Theory}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{43:1--43:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.43},
  URN =		{urn:nbn:de:0030-drops-185770},
  doi =		{10.4230/LIPIcs.MFCS.2023.43},
  annote =	{Keywords: symmetric monoidal categories, Mazurkiewicz traces, asynchronous automata}
}

50 Search Results for "Sobocinski, Pawel"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as