To Appear (Accepted for publication)

Active Learning of Markov Decision Processes using Baum-Welch algorithm

Giovanni Bacci, Anna Ingólfsdóttir, Kim G. Larsen, and Raphaël Reynouard. in 20th IEEE International Conference on Machine Learning and Applications, (ICMLA 2021), 2021.
Extended Version: icmla21

Conference and Journal Papers

Optimal and Robust Controller Synthesis using Energy Timed Automata with Uncertainty

Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey Pierre-Alain Reynier. in Formal Aspects of Compututing (FAOC), Vol. 33(1), 2021.

L*-Based Learning of Markov Decision Processes (extended version)

Martin Tappler, Bernhard K. Aichernig Giovanni Bacci, Kim G. Larsen, and Maria Eichlseder. in Formal Aspects of Compututing (FAOC), Vol. 33(4), 2021.

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. in Logical Methods in Computer Science (LMCS), Vol. 17(1), 2021.

Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Mirco Tribastone, Max Tschaikowski, Andrea Vandin. in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), IEEE, 2021.

Approximating Euclidean by Imprecise Markov Decision Processes

Manfred Jaeger, Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Peter Gjøl Jensen. in Tiziana Margaria and Bernhard Steffen editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA 2020), LNCS, 2020.

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. in Wan J. Fokkink and Rob van Glabbeek editors, Proceedings of the 30th International Conference on Concurrency Theory (CONCUR 2019), LIPIcs, 2019.

Model Checking Constrained Markov Reward Models with Uncertainties

Giovanni Bacci, Mikkel Hansen, and Kim G. Larsen. in David Parker, Verena Wolf editors, Proceedings of the 16th International Conference on Quantitative Evaluation of Systems, (QEST 2019), LNCS, 2019.

L*-Based Learning of Markov Decision Processes

Martin Tappler, Bernhard K. Aichernig Giovanni Bacci, Kim G. Larsen, and Maria Eichlseder. in Maurice H. ter Beek, Annabelle McIver, José N. Oliveira editors, Proceedings of the 3rd World Congress on Formal Methods (FM 2019), LNCS, 2019.

Converging from Branching to Linear Metrics on Markov chains

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. in M. Leucker, C. Rueda, F. D. Valencia editors, Selected papers of the 27th International Colloquium of Theoretical Aspects of Computing (ICTAC 2015), MSCS, 2019.
doi: 10.1017/S0960129517000160 | Preprint: branching-to-linear-mscs

Optimal and Robust Controller Synthesis using Energy Timed Automata with Uncertainty

Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey Pierre-Alain Reynier. in Lecture Notes in Computer Science volume 10951, Bill W. Roscoe and Jan Peleska (Eds.), Proceedings of 22nd International Symposium on Formal Methods (FM 2018), pages 203-221, 2018.
Best Paper Award at Formal Methods - FLoC 2018 | doi: 10.1007/978-3-319-95582-7\_12 | Slides: fm18_slides | Extended: fm18 | Extras: see tools page

On the Verification of Weighted Kripke Structures Under Uncertainty

Giovanni Bacci, Mikkel Hansen, Kim G. Larsen. in A. Horvath and A. McIver editors, Proceedings of 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), 2018.
doi: 10.1007/978-3-319-99154-2\_5 | Extended: fm18 | Extras: see tools page

On the Metric-based Approximate Minimization of Markov Chains

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. in Journal of Logical and Algebraic Methods in Programming (JLAMP), Special Issue of the 28th Nordic Workshop on Programming Theory (NWPT'16)

Complete Axiomatization for the Total Variation Distance of Markov chains

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. in A. Silva editor, Proceedings of Mathematical Foundations of Programming Semantics XXXIII (MFPS XXXIII), 2017.

On the Metric-based Approximate Minimization of Markov Chains

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. in Proceedings of 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), I. Chatzigiannakis, P. Indyk, F. Kuhn, and A. Muscholl editors. Leibniz International Proceedings in Informatics, Article No. 104, 2017.
doi: 10.4230/LIPIcs.ICALP.2017.104 | Slides: slides-icalp17 | Extended: extended-icalp2016 Paper: paper-icalp2016 | Extras: see tools page

On-the-Fly Computation of Bisimilarity Distances

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. in Logical Methods in Computer Science, Volume 13, Issue 2, Nir Piterman and Scott A. Smolka (Eds.), (June 30, 2017).
doi: arXiv:1702.08306[cs.LO] | Paper: paper-lmcs2017 | Extras: see tools page

Complete Axiomatization for the Bisimilarity Distance on Markov Chains

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. 27th International Conference on Concurrency Theory (CONCUR 2016), Leibniz International Proceedings in Informatics,, Article No. 21, J. Desharnais and R. Jagadeesan (Eds.), 2016.

Converging from Branching to Linear Metrics on Markov Chains

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Lecture Notes in Computer Science volume 9399, M. Leucker, C. Rueda, F. Valencia (Eds.), pages 349-367, 2015.
Best Scored Paper | doi: 10.1007/978-3-319-25150-9_21 | Slides: tvsmc_slides | Paper: tvsmc

On the Total Variation Distance of Semi-Markov Chains

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Foundations of Software Science and Computation Structures (FoSSaCS 2015), Lecture Notes in Computer Science volume 9034, A. Pitts (Ed.), pages 185-199, 2015.
doi: 10.1007/978-3-662-46678-0_12 | Slides: tvsmc_slides | Extended: tvsmc_ext | Paper: tvsmc

Bisimulation on Markov Processes over Arbitrary Measurable Spaces

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, F. van Breugel, E. Kashefi, C. Palamidessi, J. Rutten (Eds.), pages 76-95, 2014.
doi: 10.1007/978-3-319-06880-0_4 | Extended: equibisim

Computing Behavioral Distances, Compositionally

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. in Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS 2013), volume 8087 of Lecture Notes in Computer Science, K. Chatterjee and J. Sgall (Eds.), pages 74–85. Springer Berlin Heidelberg, 2013.
doi: 10.1007/978-3-642-40313-2_9 | Extras: see tools page | Slides: mfcs13 slides | Extended: compmdpdist

The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. in Proceedings of the 10th International Conference on Quantitative Evaluation of SysTems (QEST 2013), volume 8054 of Lecture Notes in Computer Science, K. Joshi, M. Siegle, M. Stoelinga, P. R. D’Argenio (Eds.) pages 278-281, Springer Berlin Heidelberg, 2013.

On-the-Fly Exact Computation of Bisimilarity Distances

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of Lecture Notes in Computer Science, pages 1-15. Springer Berlin Heidelberg, 2013.
Nominated for the Best Paper Award at ETAPS 2013 | doi:10.1007/978-3-642-36742-7_1 | Tool: prototype | Slides: tacas13 slides | Extended: tacas13

Automatic Synthesis of Specifications for First Order Curry Programs

Giovanni Bacci, Marco Comini, Marco A. Feliu, and Alicia Villanueva. In Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP '12), pages 25-34, New York, NY, USA, 2012. ACM.
doi:10.1145/2370776.2370781 | Tool: prototype | Paper: ppdp12

The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages

Giovanni Bacci, Marco Comini, Marco A. Feliu, and Alicia Villanueva. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12), volume 17 of Leibniz International Proceedings in Informatics (LIPIcs), pages 144-153, Dagstuhl, Germany, 2012.

Abstract Diagnosis of First Order Functional Logic Programs

Giovanni Bacci and Marco Comini. In Logic-Based Program Synthesis and Transformation (LOPSTR'11), volume 6564 of Lecture Notes in Computer Science, pages 215-233. Springer Berlin Heidelberg, 2011.
doi:10.1007/978-3-642-20551-4_14 | Slides: lopstr11_slides | Paper: lopstr11

Talks and Dissemination

On the Metric-based Approximate Minimization of Markov Chains

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. Workshop on Learning and Automata (LearnAut 2017).
Extended Abstract: abstract-learnaut2016

Minimizing Markov Chains Beyond Bisimilarity

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. 28th Nordic Workshop on Programming Theory (NWPT 2016).
Slides: slides-nwpt16 | Extended Abstract: abstract-nwpt2016

On-the-Fly Exact Computation of Bisimilarity Distances

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. In Quantitative Models: Expressiveness, Analysis, and New Applications, Dagstuhl Seminar 14041, 2014.

doi:10.4230/DagRep.4.1.104 | Slides: Dagstuhl14 slides | Related Papers: tacas13

Ph.D. Thesis

An Abstract Interpretation Framework for Semantics and Diagnosis of Lazy Functional-Logic Languages

Giovanni Bacci. PhD thesis, Dipartimento di Matematica e Informatica, Università di Udine, 2011.
Slides: bacci_phd_slides | Thesis: bacci_phd

Technical Reports

A Compact Goal-Independent Bottom-Up Fixpoint Modeling of the Behaviour of First Order Curry

Giovanni Bacci and Marco Comini. Technical Report DIMI-UD/06/2010/RR, Dipartimento di Matematica e Informatica, Università di Udine, 2010.
Paper: lopstr11

Disclaimer: this material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All people copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.