## Research team

- Diego Vaggione (Head of the group and Full Professor)
- Hector Gramaglia (Associate Professor)
- Miguel Campercholi (Adjunct Professor and Conicet Researcher)
- Pedro Sánchez Terraf (Adjunct Professor and Conicet Researcher)
- Mariana Badano (Assistant Professor and Postdoctoral fellow)

## Current graduate students

- Pablo Celayes
- Martín Moroni
- Mauricio Tellechea (Assistant Professor)
- Mariana Vargas Vieyra
- Pablo Ventura

## Recent Papers

### In journals (and latest manuscripts)

- P. Sánchez Terraf, “Bisimilarity is not Borel,” Mathematical Structures in Computer Science FirstView (2015).

[ $e$-edition | Download PDF | Abstract | BibTeX ]

We prove that the relation of bisimilarity between countable labelled transition systems is $\Sigma_1^1$-complete (hence not Borel), by reducing the set of non-wellorders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and nondeterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on the unique structure theorem for analytic spaces) require a countable logic whose formulas have measurable semantics. Our reduction shows that such a logic does not exist in the case of image-infinite processes.

`@article{2012arXiv1211.0967S, author = {S{\'a}nchez Terraf, Pedro}, title = {Bisimilarity is not {B}orel}, abstract = {We prove that the relation of bisimilarity between countable labelled transition systems is $\Sigma_1^1$-complete (hence not Borel), by reducing the set of non-wellorders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and nondeterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on the unique structure theorem for analytic spaces) require a countable logic whose formulas have measurable semantics. Our reduction shows that such a logic does not exist in the case of image-infinite processes.}, ee = {http://arxiv.org/abs/1211.0967}, keywords = {Mathematics - Logic, Computer Science - Logic in Computer Science, 03B70, 03E15, 28A05, F.4.1, F.1.2}, journal = {Mathematical Structures in Computer Science}, issn = {1469-8072}, doi = {10.1017/S0960129515000535}, url = {http://journals.cambridge.org/article_S0960129515000535}, month = {12}, year = {2015}, volume = {FirstView} }`

- M. Campercholi, M. M. Stronkowski, and D. Vaggione, “On structural completeness versus almost structural completeness problem: A discriminator varieties case study,” Logic Journal of IGPL 23 (2): 235-246 (2015).

[ Preprint | Download PDF | Abstract | BibTeX ]

We study the following problem: determine which almost structurally complete quasivarieties are structurally complete. We propose a general solution to this problem and then a solution in the semisimple case. As a consequence, we obtain a characterization of structurally complete discriminator varieties. An interesting corollary in logic follows: Let L be a propositional logic/deductive system in the language with formulas for verum, which is a theorem, and falsum, which is not a theorem. Assume also that L has an adequate semantics given by a discriminator variety. Then L is structurally complete if and only if it is maximal. All such logics/deductive systems are almost structurally complete.

`@article{StrucVsAlmost, author = {Campercholi, Miguel and Stronkowski, Michał M. and Vaggione, Diego}, title = {On structural completeness versus almost structural completeness problem: A discriminator varieties case study}, volume = {23}, number = {2}, pages = {235-246}, year = {2015}, doi = {10.1093/jigpal/jzu032}, abstract = {We study the following problem: determine which almost structurally complete quasivarieties are structurally complete. We propose a general solution to this problem and then a solution in the semisimple case. As a consequence, we obtain a characterization of structurally complete discriminator varieties. An interesting corollary in logic follows: Let L be a propositional logic/deductive system in the language with formulas for verum, which is a theorem, and falsum, which is not a theorem. Assume also that L has an adequate semantics given by a discriminator variety. Then L is structurally complete if and only if it is maximal. All such logics/deductive systems are almost structurally complete.}, url = {http://jigpal.oxfordjournals.org/content/23/2/235.abstract}, eprint = {http://jigpal.oxfordjournals.org/content/23/2/235.full.pdf+html}, journal = {Logic Journal of IGPL} }`

- E. Doberkat and P. Sánchez Terraf, “Stochastic Nondeterminism and Effectivity Functions,” Journal of Logic and Computation (2015).

[ Abstract | BibTeX ]

This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernels used for defining two different models: Nondeterministic labelled Markov processes and stochastic game models, respectively. We show that an effectivity function that maps into principal filters is given by an image-countable nondeterministic kernel, and that image-finite kernels give rise to effectivity functions. We define state bisimilarity for the latter, considering its connection to morphisms. We provide a logical characterization of bisimilarity in the finitary case. A generalization of congruences (event bisimulations) to effectivity functions and its relation to the categorical presentation of bisimulation are also studied.

`@article{2014arXiv1405.7141D, author = {Doberkat, Ernst-Erich and S{\'a}nchez Terraf, Pedro}, title = {Stochastic Nondeterminism and Effectivity Functions}, journal = {Journal of Logic and Computation}, archiveprefix = {arXiv}, eprint = {1405.7141}, primaryclass = {cs.LO}, keywords = {stochastic effectivity function, non-deterministic labelled Markov process, state bisimilarity, coalgebra}, year = 2015, doi = {10.1093/logcom/exv049}, abstract = {This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernels used for defining two different models: Nondeterministic labelled Markov processes and stochastic game models, respectively. We show that an effectivity function that maps into principal filters is given by an image-countable nondeterministic kernel, and that image-finite kernels give rise to effectivity functions. We define state bisimilarity for the latter, considering its connection to morphisms. We provide a logical characterization of bisimilarity in the finitary case. A generalization of congruences (event bisimulations) to effectivity functions and its relation to the categorical presentation of bisimulation are also studied.} }`

- C. Areces, M. Campercholi, D. Penazzi, and P. Sánchez Terraf, “The Lattice of Congruences of a Finite Linear Frame,” arXiv:1504.01789 (2015).

[ arXiv | Abstract | BibTeX ]

Let $\mathbf{F}=\left\langle F,R\right\rangle $ be a finite Kripke frame. A congruence of $\mathbf{F}$ is a bisimulation of $\mathbf{F}$ that is also an equivalence relation on F. The set of all congruences of $\mathbf{F}$ is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that $\mathbf{F}$ is a finite linear frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence $\rho$, the interval $[\mathrm{Id_{F},\rho]}$ embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute.

`@article{2015arXiv150401789A, author = {Areces, Carlos and Campercholi, Miguel and Penazzi, Daniel and S{\'a}nchez Terraf, Pedro}, title = {{The Lattice of Congruences of a Finite Linear Frame}}, journal = {ArXiv e-prints}, archiveprefix = {arXiv}, eprint = {1504.01789}, primaryclass = {math.LO}, keywords = {Mathematics - Logic, Computer Science - Logic in Computer Science, 03B45 (Primary), 06B10, 06E25, 03B70 (Secondary), F.4.1, F.1.2}, abstract = {Let $\mathbf{F}=\left\langle F,R\right\rangle $ be a finite Kripke frame. A congruence of $\mathbf{F}$ is a bisimulation of $\mathbf{F}$ that is also an equivalence relation on F. The set of all congruences of $\mathbf{F}$ is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that $\mathbf{F}$ is a finite linear frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence $\rho$, the interval $[\mathrm{Id_{F},\rho]}$ embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute.}, year = 2015, month = apr, adsurl = {http://adsabs.harvard.edu/abs/2015arXiv150401789A}, adsnote = {Provided by the SAO/NASA Astrophysics Data System} }`

### In peer-reviewed conferences

- C. E. Budde, P. R. D’Argenio, P. Sánchez Terraf, and N. Wolovick, “A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems,” in Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, A. Remke and M. Stoelinga, Eds., Springer Berlin Heidelberg (2014) 8453, pp. 67-86.

[ Download PDF | Abstract | BibTeX ]

The description of complex systems involving physical or biological components usually requires to model involved continuous behavior induced by variables such as time, distances, speed, temperature, alkalinity of a solution, etc. Often, such variables can be quantified probabilistically to better understand the behavior of the complex systems. For example, the arrival time of events may be considered a Poisson process or the weight of an individual may be assumed to be distributed according to a log-normal distribution. However, it is also common that the uncertainty on how these variables behave make us prefer to leave out the choice of a particular probability and rather model it as a purely non-deterministic decision, as it is the case when a system is intended to be deployed in a variety of very different computer or network architectures. Therefore, the semantics of these systems needs to be represented by a variant of probabilistic automata that involves continuous domains on the state space and the transition relation. In this paper, we provide a survey to the theory of such kind of models. We present the theory of the so called labeled Markov processes (LMP) and its extension with internal non-determinism (NLMP). We show that in these complex domains, the bisimulation relation can be understood in different manners. We show the relation among these different definitions and try to understand the boundaries among them through examples. We also study variants of Hennessy-Milner logic that provides logical characterizations of some of these bisimulations.

`@incollection{ROCKS, year = 2014, isbn = {978-3-662-45488-6}, booktitle = {Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems}, volume = 8453, series = {Lecture Notes in Computer Science}, editor = {Remke, Anne and Stoelinga, Mariëlle}, doi = {10.1007/978-3-662-45489-3_3}, title = {A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems}, url = {http://dx.doi.org/10.1007/978-3-662-45489-3_3}, publisher = {Springer Berlin Heidelberg}, pages = {67-86}, language = {English}, author = { Budde, Carlos E. and D'Argenio, Pedro R. and S{\'a}nchez Terraf, Pedro and Wolovick, Nicol\'as}, abstract = {The description of complex systems involving physical or biological components usually requires to model involved continuous behavior induced by variables such as time, distances, speed, temperature, alkalinity of a solution, etc. Often, such variables can be quantified probabilistically to better understand the behavior of the complex systems. For example, the arrival time of events may be considered a Poisson process or the weight of an individual may be assumed to be distributed according to a log-normal distribution. However, it is also common that the uncertainty on how these variables behave make us prefer to leave out the choice of a particular probability and rather model it as a purely non-deterministic decision, as it is the case when a system is intended to be deployed in a variety of very different computer or network architectures. Therefore, the semantics of these systems needs to be represented by a variant of probabilistic automata that involves continuous domains on the state space and the transition relation. In this paper, we provide a survey to the theory of such kind of models. We present the theory of the so called labeled Markov processes (LMP) and its extension with internal non-determinism (NLMP). We show that in these complex domains, the bisimulation relation can be understood in different manners. We show the relation among these different definitions and try to understand the boundaries among them through examples. We also study variants of Hennessy-Milner logic that provides logical characterizations of some of these bisimulations.} }`