8 Search Results for "Bacci, Giorgio"

Document
DOI: 10.4230/LIPIcs.ITP.2024.4
Taming Differentiable Logics with Coq Formalisation

Authors: Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, and Kathrin Stark

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

Abstract
For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to translate propositional or first-order formulae into loss functions deployed for optimisation in machine learning. At the same time, recent attempts to give programming language support for verification of neural networks showed that DLs can be used to compile verification properties to machine-learning backends. This situation is calling for stronger guarantees about the soundness of such compilers, the soundness and compositionality of DLs, and the differentiability and performance of the resulting loss functions. In this paper, we propose an approach to formalise existing DLs using the Mathematical Components library in the Coq proof assistant. Thanks to this formalisation, we are able to give uniform semantics to otherwise disparate DLs, give formal proofs to existing informal arguments, find errors in previous work, and provide formal proofs to missing conjectured properties. This work is meant as a stepping stone for the development of programming language support for verification of machine learning.
Cite as

Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, and Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.4,
  author =	{Affeldt, Reynald and Bruni, Alessandro and Komendantskaya, Ekaterina and \'{S}lusarz, Natalia and Stark, Kathrin},
  title =	{{Taming Differentiable Logics with Coq Formalisation}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{4:1--4:19},
  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.4},
  URN =		{urn:nbn:de:0030-drops-207325},
  doi =		{10.4230/LIPIcs.ITP.2024.4},
  annote =	{Keywords: Machine Learning, Loss Functions, Differentiable Logics, Logic and Semantics, Interactive Theorem Proving}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.20
Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques

Authors: Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild

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

Abstract
Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the category theoretic generalization of the Kantorovich lifting from transportation theory to the case of lifting functors to quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition, we describe how to lift distributive laws in the case where one of the two functors is polynomial (with finite coproducts). These results are essential ingredients for adapting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We illustrate the results of our paper in two case studies.
Cite as

Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild. Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dangelo_et_al:LIPIcs.CONCUR.2024.20,
  author =	{D'Angelo, Keri and Gurke, Sebastian and Kirss, Johanna Maria and K\"{o}nig, Barbara and Najafi, Matina and R\'{o}\.{z}owski, Wojciech and Wild, Paul},
  title =	{{Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{20:1--20:19},
  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.20},
  URN =		{urn:nbn:de:0030-drops-207921},
  doi =		{10.4230/LIPIcs.CONCUR.2024.20},
  annote =	{Keywords: behavioural metrics, coalgebra, Galois connections, quantales, Kantorovich lifting, up-to techniques}
}
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.CALCO.2021.7
Tensor of Quantitative Equational Theories

Authors: Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin

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

Abstract
We develop a theory for the commutative combination of quantitative effects, their tensor, given as a combination of quantitative equational theories that imposes mutual commutation of the operations from each theory. As such, it extends the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We show that under certain assumptions on the quantitative theories the free monad that arises from the tensor of two theories is the categorical tensor of the free monads on the theories. As an application, we provide the first algebraic axiomatizations of labelled Markov processes and Markov decision processes. Apart from the intrinsic interest in the axiomatizations, it is pleasing they are obtained compositionally by means of the sum and tensor of simpler quantitative equational theories.
Cite as

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Tensor of Quantitative Equational Theories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CALCO.2021.7,
  author =	{Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
  title =	{{Tensor of Quantitative Equational Theories}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{7:1--7:17},
  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.7},
  URN =		{urn:nbn:de:0030-drops-153628},
  doi =		{10.4230/LIPIcs.CALCO.2021.7},
  annote =	{Keywords: Quantitative equational theories, Tensor, Monads, Quantitative Effects}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.28
Monads and Quantitative Equational Theories for Nondeterminism and Probability

Authors: Matteo Mio and Valeria Vignudelli

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The monad of convex sets of probability distributions is a well-known tool for modelling the combination of nondeterministic and probabilistic computational effects. In this work we lift this monad from the category of sets to the category of extended metric spaces, by means of the Hausdorff and Kantorovich metric liftings. Our main result is the presentation of this lifted monad in terms of the quantitative equational theory of convex semilattices, using the framework of quantitative algebras recently introduced by Mardare, Panangaden and Plotkin.
Cite as

Matteo Mio and Valeria Vignudelli. Monads and Quantitative Equational Theories for Nondeterminism and Probability. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{mio_et_al:LIPIcs.CONCUR.2020.28,
  author =	{Mio, Matteo and Vignudelli, Valeria},
  title =	{{Monads and Quantitative Equational Theories for Nondeterminism and Probability}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.28},
  URN =		{urn:nbn:de:0030-drops-128407},
  doi =		{10.4230/LIPIcs.CONCUR.2020.28},
  annote =	{Keywords: Computational Effects, Monads, Metric Spaces, Quantitative Algebras}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.9
Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Authors: Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch’s probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon’s simple policy iteration on these games. The correctness of Condon’s approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.
Cite as

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing Probabilistic Bisimilarity Distances for Probabilistic Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CONCUR.2019.9,
  author =	{Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim G. and Mardare, Radu and Tang, Qiyi and van Breugel, Franck},
  title =	{{Computing Probabilistic Bisimilarity Distances for Probabilistic Automata}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.9},
  URN =		{urn:nbn:de:0030-drops-109119},
  doi =		{10.4230/LIPIcs.CONCUR.2019.9},
  annote =	{Keywords: Probabilistic automata, Behavioural metrics, Simple stochastic games, Simple policy iteration algorithm}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.104
On the Metric-Based Approximate Minimization of Markov Chains

Authors: Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We address the behavioral metric-based approximate minimization problem of Markov Chains (MCs), i.e., given a finite MC and a positive integer k, we are interested in finding a k-state MC of minimal distance to the original. By considering as metric the bisimilarity distance of Desharnais at al., we show that optimal approximations always exist; show that the problem can be solved as a bilinear program; and prove that its threshold problem is in PSPACE and NP-hard. Finally, we present an approach inspired by expectation maximization techniques that provides suboptimal solutions. Experiments suggest that our method gives a practical approach that outperforms the bilinear program implementation run on state-of-the-art bilinear solvers.
Cite as

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. On the Metric-Based Approximate Minimization of Markov Chains. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 104:1-104:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.ICALP.2017.104,
  author =	{Bacci, Giovanni and Bacci, Giorgio and Larsen, Kim G. and Mardare, Radu},
  title =	{{On the Metric-Based Approximate Minimization of Markov Chains}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{104:1--104:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian 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.ICALP.2017.104},
  URN =		{urn:nbn:de:0030-drops-73675},
  doi =		{10.4230/LIPIcs.ICALP.2017.104},
  annote =	{Keywords: Behavioral distances, Probabilistic Models, Automata Minimization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.21
Complete Axiomatization for the Bisimilarity Distance on Markov Chains

Authors: Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
In this paper we propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS'16) that uses equality relations t =_e s indexed by rationals, expressing that "t is approximately equal to s up to an error e". Notably, our quantitative deductive system extends in a natural way the equational system for probabilistic bisimilarity given by Stark and Smolka by introducing an axiom for dealing with the Kantorovich distance between probability distributions.
Cite as

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Complete Axiomatization for the Bisimilarity Distance on Markov Chains. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CONCUR.2016.21,
  author =	{Bacci, Giorgio and Bacci, Giovanni and G. Larsen, Kim and Mardare, Radu},
  title =	{{Complete Axiomatization for the Bisimilarity Distance on Markov Chains}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{21:1--21:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.21},
  URN =		{urn:nbn:de:0030-drops-61569},
  doi =		{10.4230/LIPIcs.CONCUR.2016.21},
  annote =	{Keywords: Markov chains, Behavioral distances, Axiomatization}
}
  • Refine by Author
  • 4 Bacci, Giorgio
  • 4 Mardare, Radu
  • 3 Bacci, Giovanni
  • 2 Larsen, Kim G.
  • 2 Różowski, Wojciech
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Models of computation
  • 1 Computing methodologies → Rule learning
  • 1 Mathematics of computing → Probability and statistics
  • 1 Theory of computation → Axiomatic semantics
  • Show More...

  • Refine by Keyword
  • 2 Behavioral distances
  • 2 Monads
  • 1 Automata Minimization
  • 1 Axiomatization
  • 1 Behavioural Distances
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2024
  • 1 2016
  • 1 2017
  • 1 2019
  • 1 2020
  • 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact