12 Search Results for "Bacci, Giorgio"

Document
DOI: 10.4230/LIPIcs.LICS.2026.6
Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability

Authors: Giorgio Bacci and Rasmus Ejlers Møgelberg

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes. We construct an affine calculus for 1-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach’s fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion, and induction over probability measures and natural numbers. We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.
Cite as

Giorgio Bacci and Rasmus Ejlers Møgelberg. Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.LICS.2026.6,
  author =	{Bacci, Giorgio and M{\o}gelberg, Rasmus Ejlers},
  title =	{{Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{6:1--6:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.6},
  URN =		{urn:nbn:de:0030-drops-267935},
  doi =		{10.4230/LIPIcs.LICS.2026.6},
  annote =	{Keywords: Quantitative Logic, Probabilistic Processes, Affine Logic, Guarded Recursion, Metric Spaces}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.48
Interpreting Lambda Calculus in Domain-Valued Random Variables

Authors: Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.
Cite as

Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott. Interpreting Lambda Calculus in Domain-Valued Random Variables. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{furber_et_al:LIPIcs.CSL.2026.48,
  author =	{Furber, Robert and Mardare, Radu and Panangaden, Prakash and Scott, Dana},
  title =	{{Interpreting Lambda Calculus in Domain-Valued Random Variables}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.48},
  URN =		{urn:nbn:de:0030-drops-254734},
  doi =		{10.4230/LIPIcs.CSL.2026.48},
  annote =	{Keywords: lambda calculus, domain theory, random variables}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.26
ε-Distance via Lévy-Prokhorov Lifting

Authors: Josée Desharnais and Ana Sokolova

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics. Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute. We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.
Cite as

Josée Desharnais and Ana Sokolova. ε-Distance via Lévy-Prokhorov Lifting. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 26:1-26:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.CSL.2026.26,
  author =	{Desharnais, Jos\'{e}e and Sokolova, Ana},
  title =	{{\epsilon-Distance via L\'{e}vy-Prokhorov Lifting}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{26:1--26:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.26},
  URN =		{urn:nbn:de:0030-drops-254506},
  doi =		{10.4230/LIPIcs.CSL.2026.26},
  annote =	{Keywords: L\'{e}vy-Prokhorov metric, behavioural distance, epsilon-bisimulation, reactive probabilistic transition systems, discrete labelled Markov processes, coalgebraic epsilon-(bi)simulation}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CSL.2026.3
Rational Lawvere Logic (Invited Paper)

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

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We study Rational Lawvere logic (RL). This logic is defined over the extended positive reals with an algebraic structure combining the Lawvere quantale (with the reversed order on the extended reals and a sum as tensor) and a multiplicative quantale (with the usual order on the extended reals and a multiplication as tensor); together they provide a semiring structure. The logic is designed for complex quantitative reasoning, including sequents expressing inequalities between rational functions over the extended positive reals. We give a deduction system and demonstrate its expressiveness by deriving a classical result from probability theory relating the Kantorovich and total variation distances. Our deductive system is complete for finitely axiomatizable theories. The proof of completeness relies on the Krivine-Stengle Positivstellensatz. We additionally provide complexity results for both RL and its affine fragment AL. We consider two decision problems: the satisfiability of a set of sequents and whether a sequent follows from a finite set of sequent. We show that both problems lie in PSPACE for RL, and we give sharper complexity bounds for AL: the first problem is NP-complete, while the second is co-NP-complete.
Cite as

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Rational Lawvere Logic (Invited Paper). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CSL.2026.3,
  author =	{Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
  title =	{{Rational Lawvere Logic}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.3},
  URN =		{urn:nbn:de:0030-drops-254277},
  doi =		{10.4230/LIPIcs.CSL.2026.3},
  annote =	{Keywords: Quantitative reasoning, complete deductive system, Lawvere’s quantale}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.36
Explainability is a Game for Probabilistic Bisimilarity Distances

Authors: Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
We revisit a game from the literature that characterizes the probabilistic bisimilarity distances of a labelled Markov chain. We illustrate how an optimal policy of the game can explain these distances. Like the games that characterize bisimilarity and probabilistic bisimilarity, the game is played on pairs of states and matches transitions of those states. To obtain more convincing and interpretable explanations than those provided by generic optimal policies, we restrict to optimal policies that delay reaching observably inequivalent state pairs for as long as possible (called 1-maximal) while quickly reaching equivalent ones (called 0-minimal). We present iterative algorithms that compute 1-maximal and 0-minimal policies and prove an exponential lower bound for the number of iterations of the algorithm that computes 1-maximal policies.
Cite as

Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a Game for Probabilistic Bisimilarity Distances. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vlasman_et_al:LIPIcs.CONCUR.2025.36,
  author =	{Vlasman, Emily and Nanah Ji, Anto and Worrell, James and van Breugel, Franck},
  title =	{{Explainability is a Game for Probabilistic Bisimilarity Distances}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.36},
  URN =		{urn:nbn:de:0030-drops-239861},
  doi =		{10.4230/LIPIcs.CONCUR.2025.36},
  annote =	{Keywords: probabilistic bisimilarity distance, labelled Markov chain, game, policy, explainability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.29
Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach

Authors: Samuel Humeau, Daniela Petrisan, and Jurriaan Rot

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
The Kantorovich distance is a widely used metric between probability distributions. The Kantorovich-Rubinstein duality states that it can be defined in two equivalent ways: as a supremum, based on non-expansive functions into [0,1], and as an infimum, based on probabilistic couplings. Orthogonally, there are categorical generalisations of both presentations proposed in the literature, in the form of codensity liftings and what we refer to as coupling-based liftings. Both lift endofunctors on the category Set of sets and functions to that of pseudometric spaces, and both are parameterised by modalities from coalgebraic modal logic. A generalisation of the Kantorovich-Rubinstein duality has been more nebulous - it is known not to work in some cases. In this paper we propose a compositional approach for obtaining such generalised dualities for a class of functors, which is closed under coproducts and products. Our approach is based on an explicit construction of modalities and also applies to and extends known cases such as that of the powerset functor.
Cite as

Samuel Humeau, Daniela Petrisan, and Jurriaan Rot. Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{humeau_et_al:LIPIcs.CSL.2025.29,
  author =	{Humeau, Samuel and Petrisan, Daniela and Rot, Jurriaan},
  title =	{{Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.29},
  URN =		{urn:nbn:de:0030-drops-227861},
  doi =		{10.4230/LIPIcs.CSL.2025.29},
  annote =	{Keywords: Kantorovich distance, behavioural metrics, Kantorovich-Rubinstein duality, functor liftings}
}
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 Type
  • 12 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 4 2026
  • 2 2025
  • 1 2024
  • 1 2021
  • 1 2020
  • Show More...

  • Refine by Author
  • 6 Bacci, Giorgio
  • 6 Mardare, Radu
  • 3 Bacci, Giovanni
  • 3 Panangaden, Prakash
  • 2 Larsen, Kim G.
  • Show More...

  • Refine by Series/Journal
  • 12 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Categorical semantics
  • 3 Theory of computation → Program verification
  • 2 Mathematics of computing → Probability and statistics
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Probabilistic computation
  • Show More...

  • Refine by Keyword
  • 2 Behavioral distances
  • 2 Metric Spaces
  • 2 Monads
  • 1 Affine Logic
  • 1 Automata Minimization
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact